---
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 all satisfying initial states. Moreover, for any (partial)
solution our algorithm synthesizes witness control strategies to ensure almost-sure
satisfaction of the temporal logic specification. While the proposed algorithm
guarantees progress and soundness in every iteration, it is computationally demanding.
We offer an alternative, more efficient solution for the reachability properties
that decomposes the problem into a series of smaller problems of the same type.
All algorithms are demonstrated 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.1016/j.nahs.2016.04.006
bibo_issue: '2'
bibo_volume: 23
dct_date: 2017^xs_gYear
dct_language: eng
dct_publisher: Elsevier@
dct_title: Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games@
...