pith. sign in

arxiv: 2606.24880 · v1 · pith:XAZPNSLQnew · submitted 2026-06-23 · 💻 cs.LO · cs.FL

Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)

Lena Becker , Holger Hermanns This is my paper

Pith reviewed 2026-06-25 21:43 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords Markov jump linear systemsprobabilistic computation tree logicstability checkingmoment-based stabilitymodel checkinglinear algebraic techniquesinitial conditions
0
0 comments X

The pith

Moment-based stability properties of Markov jump linear systems for prescribed initial states reduce to linear-algebraic checks via extended probabilistic temporal logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper formalizes probabilistic computation tree logic on Markov jump linear systems to express state-based temporal properties. It then adds extensions that capture moment-based stability notions applied only to a chosen subset of initial states rather than globally. Classical mean and mean-square stability can be too broad or misleading when interest is limited to specific starting conditions, so the model-checking framing allows reasoning directly about those sets. Although no decision procedure is obtained for the full base logic, the stability extensions are shown to be manageable through linear-algebraic techniques on the system matrices and initial sets.

Core claim

Markov jump linear systems consist of linear modes switched by an underlying Markov chain. The work establishes that extensions of PCTL can express moment-based stability relative to any prescribed set of initial states, and that these extended properties are decidable by linear-algebraic methods even though the base logic on MJLSs lacks a general decision procedure.

What carries the argument

The logical extensions of PCTL that encode moment-based stability relative to initial state sets, reduced to linear-algebraic problems on the mode matrices and transition probabilities.

If this is right

  • Stability verification becomes possible for any user-specified subset of initial conditions without the conservatism inherent in global mean or mean-square definitions.
  • State-based temporal properties on MJLSs can be specified and checked using the formalized PCTL syntax.
  • The stability extensions avoid the need to solve the full undecidable or hard model-checking problem for the base logic.
  • Linear-algebraic routines on the system matrices suffice to decide the extended stability queries.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same linear-algebraic reduction might be reusable for other moment-derived properties such as variance bounds or higher-order moment constraints.
  • Integration with existing linear-system verification tools could allow hybrid analysis where only the jump component is treated via the new logic.
  • The approach suggests a route toward compositional or assume-guarantee reasoning for networks of MJLSs by restricting attention to local initial sets.

Load-bearing premise

The moment-based stability properties relative to initial states can be reduced to linear-algebraic problems without requiring a decision procedure for the full base PCTL logic on MJLSs.

What would settle it

An explicit MJLS example together with a concrete initial state set for which the linear-algebraic procedure returns a stability verdict that is contradicted by direct simulation of the moments or by an alternative analysis method.

Figures

Figures reproduced from arXiv: 2606.24880 by Holger Hermanns, Lena Becker.

Figure 1
Figure 1. Figure 1: An MJLS J = (P, {A1, A2, A3}) with the DTMC visualized on the right. 2 Background Notation. The indicator function that evaluates to 1 if x ∈ S and 0 otherwise is denoted 1S (x). For i ∈ {1, . . . , m}, let ei be the i-th canonical base vector for the m-dimensional space. Let In and 0n be the identity and all-zeros matrix of size n × n, respectively. AT denotes the transpose of matrix A. Further, ρ (A) = m… view at source ↗
Figure 1
Figure 1. Figure 1: Let Π ∈ R 2 be the convex polytope de￾fined by the vertices (30, 14),(22, 35),(−32, −5), and (36, −27). We are interested in the set of states that satisfy EΠ. Furthermore, we would like to allow for a five-step grace period to reach a state with the desired long-run expected value, while still avoiding unsafe states. We de￾fine another convex polytope Λ with vertices (−15, −10),(50, −29),(45, 50), and (0,… view at source ↗
Figure 2
Figure 2. Figure 2: A visualization of the polytopes from Example 4. Example 4. Consider again the MJLS given in [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: A visualization of the satisfaction sets of [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper formalizes probabilistic computation tree logic (PCTL) on Markov jump linear systems (MJLSs) to enable specification of state-based temporal properties. It extends the logic to express moment-based stability properties relative to a prescribed set of initial states. Although no decision procedure is obtained for the full base PCTL logic on MJLSs, the authors claim that the stability extensions can be handled (with technical subtleties) via linear-algebraic techniques.

Significance. If the claimed reductions hold, the work would enable more precise, initial-state-specific stability verification for MJLSs than classical mean or mean-square stability notions, by combining model-checking ideas with linear algebra. This could be useful in control applications where only subsets of initial conditions matter, provided the technical subtleties do not introduce hidden dependencies on undecidable fragments.

major comments (1)
  1. [Abstract] Abstract (final paragraph): the claim that moment-based stability extensions relative to initial states can be reduced to linear-algebraic problems without a decision procedure for the base PCTL logic lacks any visible concrete reduction steps, matrix constructions, or proof sketches; without these it is impossible to verify whether the separation is valid or whether the approach inadvertently relies on solving the undecidable base problem.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thoughtful review and for highlighting the need for greater clarity regarding our claims about reductions for the stability extensions. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract (final paragraph): the claim that moment-based stability extensions relative to initial states can be reduced to linear-algebraic problems without a decision procedure for the base PCTL logic lacks any visible concrete reduction steps, matrix constructions, or proof sketches; without these it is impossible to verify whether the separation is valid or whether the approach inadvertently relies on solving the undecidable base problem.

    Authors: The abstract provides only a high-level summary; the concrete reductions, matrix constructions, and proof sketches appear in the body of the manuscript (Sections 4–6). We define the moment-based stability properties as specific PCTL formulas over the first- and second-moment dynamics. These formulas are then reduced to checking the spectral radius of certain Kronecker-product matrices or solving linear systems whose coefficients are derived directly from the mode-dependent system matrices and the initial-state distribution. The reduction exploits the closed-form evolution of moments under MJLS dynamics and does not invoke the general PCTL model-checking procedure, which we explicitly leave open. We are happy to expand the abstract with a one-sentence pointer to these constructions if the editor considers it useful. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via linear algebra

full rationale

The paper's core claim is that moment-based stability extensions (relative to initial states) reduce to linear-algebraic problems on MJLSs, while explicitly disclaiming a decision procedure for full base PCTL. No equations, self-definitional loops, fitted inputs renamed as predictions, or load-bearing self-citations appear in the abstract or description. The separation between the undecidable full logic and the algebraically solvable moment properties is presented without internal reduction to the result itself. This matches the default case of an independent application of standard techniques.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach relies on standard properties of Markov chains and linear algebra; no free parameters, invented entities, or ad-hoc axioms are mentioned in the abstract.

axioms (2)
  • standard math Markov chains have well-defined transition probabilities and can be composed with linear dynamics.
    Invoked implicitly when defining MJLS and PCTL semantics on them.
  • domain assumption Linear-algebraic operations on matrices derived from the MJLS modes suffice to decide moment stability.
    Stated as the method that handles the stability extensions.

pith-pipeline@v0.9.1-grok · 5694 in / 1358 out tokens · 22022 ms · 2026-06-25T21:43:58.525409+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 15 canonical work pages

  1. [1]

    In: Formal Modeling and Analysis of Timed Systems

    Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: Formal Modeling and Analysis of Timed Systems. pp. 88–104. Springer (2004)

    2004

  2. [2]

    In: 40th Annual ACM/IEEE Symposium on Logic in Com- puter Science, LICS 2025

    Baier, C., Chatterjee, K., Meggendorfer, T., Piribauer, J.: Multiplicative rewards in Markovian models. In: 40th Annual ACM/IEEE Symposium on Logic in Com- puter Science, LICS 2025. pp. 499–512. IEEE (2025). https://doi.org/10.1109/ LICS65433.2025.00044

    arXiv 2025

  3. [3]

    MIT Press (2008)

    Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)

    2008

  4. [4]

    Prentice-Hall, 3 edn

    Brogan, W.L.: Modern control theory. Prentice-Hall, 3 edn. (1991)

    1991

  5. [5]

    Oxford University Press, 4 edn

    Chen, C.T.: Linear system theory and design. Oxford University Press, 4 edn. (2014)

    2014

  6. [6]

    Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the orbit problem. J. ACM63(3) (2016). https://doi.org/10.1145/2857050

    work page doi:10.1145/2857050 2016

  7. [7]

    Journal of Mathematical Analysis and Ap- plications179(1), 154–178 (1993)

    Costa, O.L.V., Fragoso, M.D.: Stability results for discrete-time linear systems with markovian jumping parameters. Journal of Mathematical Analysis and Ap- plications179(1), 154–178 (1993). https://doi.org/10.1006/jmaa.1993.1341

    work page doi:10.1006/jmaa.1993.1341 1993

  8. [8]

    Springer (2005)

    Costa, O.L.V., Fragoso, M.D., Marques, R.P.: Discrete-time Markov jump linear systems. Springer (2005). https://doi.org/10.1007/b138575

    work page doi:10.1007/b138575 2005

  9. [9]

    Springer (2012)

    Costa, O.L.V., Fragoso, M.D., Todorov, M.G.: Continuous-time Markov jump lin- ear systems. Springer (2012). https://doi.org/10.1007/978-3-642-34100-7

    work page doi:10.1007/978-3-642-34100-7 2012

  10. [10]

    Wiley, 3 edn

    Dummit, D.S., Foote, R.M.: Abstract Algebra. Wiley, 3 edn. (2003)

    2003

  11. [11]

    IEEE Transactions on Automatic Control37(1), 38–53 (1992)

    Feng, X., Loparo, K., Ji, Y., Chizeck, H.: Stochastic stability properties of jump linear systems. IEEE Transactions on Automatic Control37(1), 38–53 (1992). https://doi.org/10.1109/9.109637

    work page doi:10.1109/9.109637 1992

  12. [12]

    IEEE Transactions on Aerospace and Electronic Systems36(4), 1204–1218 (2000)

    Gray, W., Gonzalez, O., Dogan, M.: Stability analysis of digital linear flight con- trollers subject to electromagnetic disturbances. IEEE Transactions on Aerospace and Electronic Systems36(4), 1204–1218 (2000). https://doi.org/10.1109/7. 892669

    work page doi:10.1109/7 2000

  13. [13]

    Grötschel, M., Lovász, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization, Algorithms and Combinatorics, vol. 2. Springer, 2 edn. (1993). https: //doi.org/10.1007/978-3-642-78240-4

    work page doi:10.1007/978-3-642-78240-4 1993

  14. [14]

    Formal Aspects of Computing6(5), 512–535 (1994)

    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing6(5), 512–535 (1994). https://doi.org/10.1007/bf01211866

    work page doi:10.1007/bf01211866 1994

  15. [15]

    Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM33(4), 808–821 (1986). https://doi.org/10.1145/6490.6496

    work page doi:10.1145/6490.6496 1986

  16. [16]

    Karimov, T., Kelmendi, E., Ouaknine, J., Worrell, J.: What’s Decidable About Discrete Linear Dynamical Systems?, pp. 21–38. Springer (2022). https://doi.org/ 10.1007/978-3-031-22337-2_2

    work page doi:10.1007/978-3-031-22337-2_2 2022

  17. [17]

    In: 45th International Symposium on Math- ematical Foundations of Computer Science, MFCS 2020

    Karimov,T.,Ouaknine,J.,Worrell,J.:OnLTLmodelcheckingforlow-dimensional discrete linear dynamical systems. In: 45th International Symposium on Math- ematical Foundations of Computer Science, MFCS 2020. LIPIcs, vol. 170, pp. 54:1–54:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020). https: //doi.org/10.4230/LIPIcs.MFCS.2020.54 18 L. Becker, H. Hermanns

    work page doi:10.4230/lipics.mfcs.2020.54 2020

  18. [18]

    Springer (1976)

    Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Springer (1976)

    1976

  19. [19]

    IEEE Transactions on Automatic Control60(8), 2031–2045 (2015)

    Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Transactions on Automatic Control60(8), 2031–2045 (2015). https://doi.org/10.1109/TAC.2015.2398883

    work page doi:10.1109/tac.2015.2398883 2031

  20. [20]

    IEEE Transactions on Circuits and Systems II: Express Briefs62(8), 801–805 (2015)

    Lian, J., Liu, J., Zhuang, Y.: Mean stability of positive Markov jump linear systems with homogeneous and switching transition probabilities. IEEE Transactions on Circuits and Systems II: Express Briefs62(8), 801–805 (2015). https://doi.org/10. 1109/TCSII.2015.2433371

    arXiv 2015

  21. [21]

    IEEE Transactions on Circuits and Systems37(6), 787–798 (1990)

    Loparo, K., Abdel-Malek, F.: A probabilistic approach to dynamic power system security. IEEE Transactions on Circuits and Systems37(6), 787–798 (1990). https: //doi.org/10.1109/31.55036

    work page doi:10.1109/31.55036 1990

  22. [22]

    https://doi.org/10.3390/s140101835

    Nogueira, S.L., Siqueira, A.A.G., Inoue, R.S., Terra, M.H.: Markov jump linear systems-basedpositionestimationforlowerlimbexoskeletons.Sensors14(1),1835– 1849 (2014). https://doi.org/10.3390/s140101835

    work page doi:10.3390/s140101835 2014

  23. [23]

    In: Proceedings of the 13th ACM International ConferenceonHybridSystems:ComputationandControl,HSCC2010,Stockholm, Sweden, April 12-15, 2010

    Ramponi, F., Chatterjee, D.,Summers, S., Lygeros, J.: On the connections between PCTL and dynamic programming. In: Proceedings of the 13th ACM International ConferenceonHybridSystems:ComputationandControl,HSCC2010,Stockholm, Sweden, April 12-15, 2010. pp. 253–262. ACM (2010). https://doi.org/10.1145/ 1755952.1755988

    arXiv 2010

  24. [24]

    Ziegler, G.M.: Lectures on Polytopes, vol. 152. Springer (1994). https://doi.org/ 10.1007/978-1-4613-8431-1 Stability Checking of MJLS via Probabilistic Temporal Logic 19 A Appendix A.1 Example MJLS The running example in Fig. 1 has been crafted to illustrate many of the phe- nomena in a tiny model. The precise numbers used are as follows: A1 = 300/847 49...

    work page doi:10.1007/978-1-4613-8431-1 1994