Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)
2026-06-23 • Logic in Computer Science
Logic in Computer ScienceFormal Languages and Automata Theory
AI summaryⓘ
The authors study Markov jump linear systems, which switch randomly between different behaviors described by linear math rules. Traditional ways to analyze these systems look at overall long-term averages but can miss details when focusing on specific starting points. To address this, the authors use a logic-based method called probabilistic computation tree logic (PCTL) to describe and check properties that depend on particular sets of starting states. They expand this logic to also express stability related to those moments and starting points. Though they don't solve the problem completely, they show parts of their approach can be worked out using linear algebra.
Markov jump linear systemsmean stabilitymean-square stabilityMarkov chainprobabilistic computation tree logicmodel checkingmoment-based stabilitylinear algebratemporal properties
Authors
Lena Becker, Holger Hermanns
Abstract
Markov jump linear systems (MJLSs) model dynamical phenomena subject to random switching among multiple linear modes, driven by an underlying Markov chain. Classical notions such as mean and mean-square stability characterize the long-term asymptotic behaviour of the first and second moments of an MJLS, but they can be overly conservative or even misleading when only a specific subset of initial conditions is of interest. We tackle this challenge through the lens of model checking, where reasoning about specific sets of initial conditions is intrinsic to the approach. We begin by formalizing probabilistic computation tree logic (PCTL) on MJLSs, enabling the specification of state-based temporal properties for these systems. Building on this foundation, we extend the logic to capture moment-based stability properties relative to a prescribed set of initial states. While we ultimately do not obtain a decision procedure for the entire base logic, the logical extensions can be handled -- albeit with some technical subtleties -- by exploiting linear-algebraic techniques.