Decisiveness of stochastic systems and its application to hybrid models

In 2007, 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 f...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2022-11, Vol.289, p.104861, Article 104861
Main Authors: Bouyer, Patricia, Brihaye, Thomas, Randour, Mickael, Rivière, Cédric, Vandenhove, Pierre
Format: Article
Language:English
Subjects:
Computer Science
Hybrid systems
Logic in Computer Science
Model checking
o-minimality
Reachability
Stochastic systems
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In 2007, 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 the 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.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2021.104861