Model Checking Markov Chains as Distribution Transformers

TL;DR

This work reframes Markov chains as distribution transformers, studying the infinite sequence of distributions $(\mu, M\mu, M^2\mu, \dots)$ against temporal specifications via a linear dynamical-system framework. It develops a spectral/ dimensional analysis, introducing the dynamical-dimension concept (the number of nonzero eigenvalues with $|\lambda|<1$) and proving decidability when either the update induces low dynamical dimension (at most $3$) or the target sets are Markov-low-dimensional, with an additional result for low intrinsic/linear-dimensional targets under taming conditions. The authors also prove hardness results, showing that without these restrictions the problem can encode Skolem-type problems, including reductions from Skolem-$5$ to ergodic Markov-chain reachability with low-dimensional semialgebraic targets. Together, these results delineate a near-tight boundary between decidability and hardness for model-checking the evolution of distributions under stochastic dynamics, guiding practical applicability by exploiting spectral structure. The work thus connects stochastic processes, algebraic geometry, and automata theory to extend verification concepts beyond traditional probability-of-events questions.

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μ, M^2μ, \dots)$ 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.

Theorems & Definitions (30)

• definition thmcounterdefinition
• theorem thmcountertheorem: Auxiliary decidability result
• theorem thmcountertheorem: Main result of tamedecidable
• definition thmcounterdefinition
• theorem thmcountertheorem: Main decidability result
• theorem thmcountertheorem: First hardness result
• theorem thmcountertheorem: Second Hardness Result
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition