Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games (2015)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/15:00080610 |
|---|---|
| Název v anglickém jazyce | Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2015 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 2 |
| Počet tvůrců celkem | 6 |
| Počet domácích tvůrců | 2 |
| Výčet všech uvedených jednotlivých tvůrců | Mária Svoreňová (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 3734994) Jan Křetínský (státní příslušnost: CZ - Česká republika, vedidk: 3503054) Martin Chmelík (státní příslušnost: CZ - Česká republika, vedidk: 7692005) Krishnendu Chatterjee (státní příslušnost: AT - Rakouská republika) Ivana Černá (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2361132) Calin Belta (státní příslušnost: US - Spojené státy americké) |
| Popis výsledku v anglickém jazyce | We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement,and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study. |
| Klíčová slova oddělená středníkem | control; linear temporal logic (LTL); linear stochastic system; games |
| Stránka www, na které se nachází výsledek | - |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Proceedings of ACM international conference on Hybrid Systems: Computation and Control |
|---|---|
| ISBN | 9781450334334 |
| ISSN | - |
| Počet stran výsledku | 10 |
| Strana od-do | 259-268 |
| Název nakladatele | Association for Computing Machinery (ACM) |
| Místo vydání | Seattle, Washington, USA |
| Místo konání akce | Seattle, Washington, USA |
| Datum konání akce | 2015 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2016 |
| Specifikace | RIV/00216224:14330/15:00080610!RIV16-MSM-14330___ |
| Datum poslední aktualizace výsledku | 24.05.2016 |
| Kontrolní číslo | 191635681 |
Informace o dalších výskytech výsledku dodaného stejným předkladatelem
| Dodáno GA ČR v roce 2016 | RIV/00216224:14330/15:00080610 v dodávce dat RIV16-GA0-14330___/01:1 |
|---|
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Projekt podporovaný GA ČR v programu GA | GA15-17564S - Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů (2015 - 2017) |
|---|---|
| Projekt podporovaný MŠMT v programu LH | LH11065 - Řízení a ověřování vlastností komplexních hybridních systémů (2011 - 2014) |
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |