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 asdistribution 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\(\mu \), a stochastic update transition matrixM, we ask whether the ensuing sequence of distributions\((\mu , M\mu , M^2\mu , \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.

1. 1.

   In this paper, we study a more linear-algebraic perspective than usual, and hence take distributions to be column vectors, and matrices to be left-stochastic, i.e. columns sum up to 1.

2. 2.

   The Skolem problem is often formulated equivalently in terms of linear recurrence sequences (LRS) that satisfy a recurrence relation\(u_{n+k} = a_{k-1}u_{n+k-1}+\dots + a_0 u_n\).

3. 3.

   If either ofi, j is 1, then the proof is even simpler because the corresponding\(v'\) is the zero vector.

4. 4.

   A matrixA is said to benon-degenerate if for every pair of distinct eigenvalues\(\lambda , \lambda '\), the ratio\(\lambda /\lambda '\) is not a root of unity.

5. 5.

   This is easily seen: let\(v_\lambda , \overline{v_\lambda }, v_\gamma , \overline{v_\gamma }, v_\rho \) be eigenvectors of\(\kappa A\), and take the columns ofP to be\((v_\lambda + \overline{ v_\lambda }), i(v_\lambda - \overline{v_\lambda }), (v_\gamma + \overline{v_\gamma }), i(v_\gamma - \overline{v_\gamma }), v_\rho \).

This work was funded by DFG grant 389792660 as part of TRR 248 - CPEC (seehttps://www.perspicuous-computing.science). Joël Ouaknine is also affiliated with Keble College, Oxford asemmy.network fellow (https://emmy.network/).

Authors and Affiliations

1. Technische Universität Dresden, Dresden, Germany

   Rajab Aghamov, Christel Baier & Jakob Piribauer

2. Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

   Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine & Mihir Vahanwala

Corresponding author

Correspondence toJakob Piribauer.

Editors and Affiliations

1. Ruhr University Bochum and Radboud University Nijmegen, Bochum, Germany

   Nils Jansen

2. Radboud University Nijmegen, Nijmegen, The Netherlands

   Sebastian Junges

3. Saarland University and University College London, Saarbrücken, Germany

   Benjamin Lucien Kaminski

4. University of Oldenburg, Oldenburg, Germany

   Christoph Matheja

5. RWTH Aachen University, Aachen, Germany

   Thomas Noll

6. RWTH Aachen University, Aachen, Germany

   Tim Quatmann

7. University of Twente and Radboud University Nijmegen, Enschede, The Netherlands

   Mariëlle Stoelinga

8. Eindhoven University of Technology, Eindhoven, The Netherlands

   Matthias Volk

Disclosure of Interests

The authors have no competing interests to declare that are relevant to the content of this article.

Reprints and permissions

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics