2014/10/20 by Mária Svoreňová, Svorenova, Maria, Jan Křetínský +9
Computer Science · #Bayesian Modeling and Causal Inference #FOS: Electrical engineering #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1410.5387
openalex publication_date 2014/10/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
We consider the problem of computing the set of initial states of a dynamical\nsystem such that there exists a control strategy to ensure that the\ntrajectories satisfy a temporal logic specification with probability 1\n(almost-surely). We focus on discrete-time, stochastic linear dynamics and\nspecifications given as formulas of the Generalized Reactivity(1) fragment of\nLinear Temporal Logic over linear predicates in the states of the system. We\npropose a solution based on iterative abstraction-refinement, and turn-based\n2-player probabilistic games. While the theoretical guarantee of our algorithm\nafter any finite number of iterations is only a partial solution, we show that\nif our algorithm terminates, then the result is the set of satisfying initial\nstates. Moreover, for any (partial) solution our algorithm synthesizes witness\ncontrol strategies to ensure almost-sure satisfaction of the temporal logic\nspecification. We demonstrate our approach on an illustrative case study.\n