Model Checking Markov Chains as Distribution Transformers

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in Buch/Sammelband/GutachtenBeigetragenBegutachtung

Beitragende

Abstract

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μ,M2μ,⋯) 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.

Details

OriginalspracheEnglisch
TitelPrinciples of Verification: Cycling the Probabilistic Landscape
Herausgeber (Verlag)Springer, Cham
Seiten293-313
Seitenumfang21
ISBN (elektronisch)978-3-031-75775-4
ISBN (Print)978-3-031-75774-7
PublikationsstatusVeröffentlicht - 2025
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science
Band15261
ISSN0302-9743

Externe IDs

Scopus 85211110147
ORCID /0000-0002-5321-9343/work/185738303
ORCID /0000-0003-4829-0476/work/185740145

Schlagworte