---
_id: '1689'
abstract:
- lang: eng
text: 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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Mária
full_name: Svoreňová, Mária
last_name: Svoreňová
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Ivana
full_name: Cěrná, Ivana
last_name: Cěrná
- first_name: Cǎlin
full_name: Belta, Cǎlin
last_name: Belta
citation:
ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
logic control for stochastic linear systems using abstraction refinement of probabilistic
games. In: Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608'
apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &
Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction
refinement of probabilistic games. In Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control (pp. 259–268). Seattle,
WA, United States: ACM. https://doi.org/10.1145/2728606.2728608'
chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” In Proceedings of the
18th International Conference on Hybrid Systems: Computation and Control,
259–68. ACM, 2015. https://doi.org/10.1145/2728606.2728608.'
ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
“Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games,” in Proceedings of the 18th International Conference
on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015,
pp. 259–268.'
ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015.
Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games. Proceedings of the 18th International Conference on Hybrid
Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control,
259–268.'
mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
Using Abstraction Refinement of Probabilistic Games.” Proceedings of the 18th
International Conference on Hybrid Systems: Computation and Control, ACM,
2015, pp. 259–68, doi:10.1145/2728606.2728608.'
short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control, ACM, 2015, pp. 259–268.'
conference:
end_date: 2015-04-16
location: Seattle, WA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2015-04-14
date_created: 2018-12-11T11:53:29Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2025-06-11T06:33:00Z
day: '14'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1145/2728606.2728608
ec_funded: 1
external_id:
arxiv:
- '1410.5387'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1410.5387
month: '04'
oa: 1
oa_version: Preprint
page: 259 - 268
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
Computation and Control'
publication_status: published
publisher: ACM
publist_id: '5456'
related_material:
record:
- id: '1407'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
of probabilistic games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...