Model Checking Markov Chains as Distribution Transformers

Rajab AghamovRajab Aghamov, Christel BaierChristel Baier, Toghrul KarimovToghrul Karimov, Joris NieuwveldJoris Nieuwveld, Joël OuaknineJoël Ouaknine, Jakob PiribauerJakob Piribauer, Mihir VahanwalaMihir Vahanwala

DOI Link

Rajab Aghamov, Christel Baier, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Jakob Piribauer, Mihir Vahanwala
Model Checking Markov Chains as Distribution Transformers
In Nils Jansen and Sebastian Junges and Benjamin Lucien Kaminski and Christoph Matheja and Thomas Noll and Tim Quatmann and Mariëlle Stoelinga and Matthias Volk, eds., Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part II, volume 15261 of Lecture Notes in Computer Science, 293--313, 2024. Springer

Details
Bibtex

KurzfassungAbstract
The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However, consider the following query made of a stochastic system modelling the weather: given the conditions today, will there be a day with less than 50% chance of rain? The conventional perspective is ill-equipped to decide such problems regarding the evolution of the initial distribution. The alternate perspective we consider views Markov chains as distribution transformers: the focus is on the sequence of distributions on states at each step, where the evolution is driven by the underlying stochastic transition matrix. More precisely, given an initial distribution vector μ, a stochastic update transition matrix M, we ask whether the ensuing sequence of distributions (μ, Mμ, M²μ, ...) satisfies a given temporal property. This is a special case of the model-checking problem for linear dynamical systems, which is not known to be decidable in full generality. The goal of this article is to delineate the classes of instances for which this problem can be solved, under the assumption that the dynamics is governed by stochastic matrices.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-75775-4_13.

@inproceedings{ABKNOPV2024,
  author    = {Rajab Aghamov and Christel Baier and Toghrul Karimov and Joris
               Nieuwveld and Jo{\"{e}}l Ouaknine and Jakob Piribauer and Mihir
               Vahanwala},
  title     = {Model Checking Markov Chains as Distribution Transformers},
  editor    = {Nils Jansen and Sebastian Junges and Benjamin Lucien Kaminski and
               Christoph Matheja and Thomas Noll and Tim Quatmann and
               Mari{\"{e}}lle Stoelinga and Matthias Volk},
  booktitle = {Principles of Verification: Cycling the Probabilistic Landscape -
               Essays Dedicated to Joost-Pieter Katoen on the Occasion of His
               60th Birthday, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {15261},
  publisher = {Springer},
  year      = {2024},
  pages     = {293--313},
  doi       = {10.1007/978-3-031-75775-4_13}
}