16 octobre 2023
Lina Ye (LMF)Decisiveness of infinite Markov chains is a key property that allows to compute reachability probabilities up to an arbitrary precision. However such a generic method suffers from two limitations: (1) decisiveness is somewhat related to recurrence of Markov chains and so does not cover transient models and (2) most of the applicable cases of decisiveness require that the transition weights are independent of the current state which forbids a relevant fraction of probabilistic modelings requiring dynamic weights (i.e., also depending on the current state). In this work, we extend this approach in two directions. First we introduce a new property called divergence that somehow complements decisiveness and also leads to a similar computation. Then we study the decidability of these two properties for dynamic probabilistic versions of counter machines, pushdown automata, and Petri nets. Finally, we exhibit some divergent or decisive subclasses of channel systems and Petri nets.
This presentation is based on two papers accepted by CONCUR’23 and by RP’23, and are joint work with Alain Finkel (LMF) and Serge Haddad (LMF).