Decisiveness of Stochastic Systems and its Application to Hybrid Models

Patricia Bouyer
(LSV, CNRS and ENS Paris-Saclay, Université Paris-Saclay, France)
Thomas Brihaye
(UMONS - Université de Mons, Belgium)
Mickael Randour
(F.R.S.-FNRS and UMONS - Université de Mons, Belgium)
Cédric Rivière
(UMONS - Université de Mons, Belgium)
Pierre Vandenhove
(F.R.S.-FNRS, UMONS - Université de Mons, Belgium and LSV, CNRS and ENS Paris-Saclay, Université Paris-Saclay, France)

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).

In Jean-Francois Raskin and Davide Bresolin: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2020), Brussels, Belgium, September 21-22, 2020, Electronic Proceedings in Theoretical Computer Science 326, pp. 149–165.
Published: 20th September 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.326.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org