We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Electrical Engineering and Systems Science > Systems and Control

Title: Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems

Abstract: We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a B\"uchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the B\"uchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the B\"uchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. In contrast with finite-state models, we show that such a computation only gives a lower bound on the maximal probability where the gap can be non-zero.
In this paper we focus on approximating the qualitative winning set, while pointing out that the existing approaches for unbounded reachability computation can solve the second step. We provide an abstraction-based technique to approximate the qualitative winning set by simultaneously using an over- and under-approximation of the probabilistic transition relation. Since we are interested in qualitative properties, the abstraction is non-probabilistic; instead, the probabilistic transitions are assumed to be under the control of a (fair) adversary. Thus, we reduce the original policy synthesis problem to a B\"uchi game under a fairness assumption and characterize upper and lower bounds on winning sets as nested fixed point expressions in the $\mu$-calculus. This characterization immediately provides a symbolic algorithm scheme. Further, a winning strategy computed on the abstract game can be refined to a policy on the controlled Markov process.
We describe a concrete abstraction procedure and demonstrate our algorithm on two case studies.
Subjects: Systems and Control (eess.SY)
Journal reference: 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC '20), April 22--24, 2020, Sydney, NSW, Australia
DOI: 10.1145/3365365.3382214
Cite as: arXiv:1910.12137 [eess.SY]
  (or arXiv:1910.12137v2 [eess.SY] for this version)

Submission history

From: Kaushik Mallik [view email]
[v1] Sat, 26 Oct 2019 20:37:15 GMT (471kb,D)
[v2] Fri, 14 Feb 2020 14:30:41 GMT (298kb,D)

Link back to: arXiv, form interface, contact.