---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Mária
foaf_name: Svoreňová, Mária
foaf_surname: Svoreňová
- foaf_Person:
foaf_givenName: Jan
foaf_name: Kretinsky, Jan
foaf_surname: Kretinsky
foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-8122-2881
- foaf_Person:
foaf_givenName: Martin
foaf_name: Chmelik, Martin
foaf_surname: Chmelik
foaf_workInfoHomepage: http://www.librecat.org/personId=3624234E-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Ivana
foaf_name: Cěrná, Ivana
foaf_surname: Cěrná
- foaf_Person:
foaf_givenName: Cǎlin
foaf_name: Belta, Cǎlin
foaf_surname: Belta
bibo_doi: 10.1145/2728606.2728608
dct_date: 2015^xs_gYear
dct_language: eng
dct_publisher: ACM@
dct_title: Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games@
...