PaperlayerView exact revision on arXiv

Source-linked AI summary

Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking

Tsubasa Matsumoto, Kazuki Watanabe, Masaki Waga

arXiv:2609.02457v1cs.LO

TL;DR

Probabilistic model checking must handle state-space explosion in stochastic systems, motivating abstractions that preserve property satisfaction probabilities. This paper introduces specification-guided path shortcutting for Markov chains and ω-regular properties, implements it with Storm and Spot, and reports frequent performance gains, especially for complex specifications, while noting a scope limitation for other automata constructions.

  • Problem

    State-space explosion makes probabilistic model checking slower and can degrade performance when Markov-chain representations exceed memory.

    Source: C. Existing Approach and Challenge · p. 1

  • Method

    For a fixed ω-regular property, specification-guided path shortcutting replaces suitable transition sequences with shortcuts and constructs an equivalent reduced Markov chain.

    Source: D. Our Approach · p. 2, §II · p. 2

  • Results

    The prototype often outperforms Storm, with especially strong gains on benchmark instances involving LTL formulas with multiple temporal operators.

    Source: §IX · p. 13

  • Takeaways & Limitations

    The abstraction provides a preprocessing technique that exactly preserves the satisfaction probability of the given property while reducing the model to be checked.

    Source: D. Our Approach · p. 2, §IX · p. 13

    Generalizing the abstraction to other ω-automata remains future work because the current BSCC-based proof is not directly applicable to weighted systems that may not be stochastic.

    Source: §IX · p. 13

Abstract

from arXiv · show

Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a particularly important technique. However, there is a well-known scalability issue due to state-space explosion, especially when verifying complex properties. To mitigate this issue, we propose specification-guided path shortcutting for probabilistic systems, focusing on Markov chains (MCs) and $ω$-regular properties. The key idea is that, when the verified property is fixed, certain sequences of transitions in an MC can be replaced with a single transition without changing the satisfaction probability, and thus, we can reduce the state space of the MC. We implement the proposed path shortcutting and evaluate its contribution to the performance of probabilistic model checking, using Storm as the baseline model checker. The results suggest that our approach often outperforms the baseline, particularly on benchmark instances with complex specifications.

I. INTRODUCTION

Probabilistic model checking addresses stochastic embedded systems but faces state-space scalability limits. The paper proposes specification-guided path shortcutting, an abstraction for Markov chains and ω-regular properties, and evaluates it against Storm.

Motivation

Challenge

  • State-space explosion increases verification time and can degrade model-checker performance when the model representation exceeds available memory.The paper identifies state-space size as a long-standing bottleneck in probabilistic model checking.Source: C. Existing Approach and Challenge · p. 1

Existing Approach and Challenge

  • Bisimulation minimization can reduce state spaces while preserving satisfaction probabilities, but its requirement is often too strong for realistic Markov chains.The paper notes an example where no two distinct states are bisimilar.Source: C. Existing Approach and Challenge · p. 1

Our Approach

  • Specification-guided path shortcutting constructs a property-specific Markov chain that preserves satisfaction probability for a given ω-regular property, including LTL properties.Its specification dependence allows elimination of states irrelevant to checking the selected property.Source: D. Our Approach · pp. 1–2

Evaluation

  • The method is implemented in Storm-SGPS and evaluated against Storm on QComp benchmark instances, with reported end-to-end speedups of up to 18×.The evaluation compares the proposed workflow with the state-of-the-art model checker Storm.Source: D. Our Approach · p. 2, E. Contributions and Outline · p. 2

II. OVERVIEW

The overview illustrates specification-guided shortcutting by using a DRA for an LTL property to replace equivalent path segments and eliminate unreachable states. The resulting Markov chain preserves the specification-relevant behavior while reducing the example from six states to four.

  • The example constructs a DRA for φ := □(a =⇒ ♢b) before applying specification-guided shortcutting to the Markov chain.Source: §II · p. 2
  • Reading {a}{b} is equivalent to reading {b}, so the two-step transition from s1 to s5 is replaced by one transition of probability 0.4.The replacement removes the edge from s1 to s4 and makes s4 unreachable from the initial state.Source: §II · p. 2, Figure 4 · p. 2
  • Reading {a}{a} is equivalent to {a}, allowing the cycle s1 · s4 · s5 to be shrunk into a self-loop at s5.The probabilities of the replacement edges are obtained by multiplication, such as 0.3 × 0.5 for the edge from s5 to s2.Source: §II · p. 2, Figure 5 · p. 3
  • Replacing the edge from s0 to s1 and eliminating unreachable s1 yields an equivalent four-state MC instead of the original six-state MC.The example states that this reduction goes beyond classical bisimulation-based reductions, which do not eliminate states in M.Source: §II · p. 2, Figure 6 · p. 3
  • The paper studies probabilistic model checking for Markov chains and quantitative ω-regular properties using labeled finite and infinite paths and their traces.An MC has finite states, atomic propositions, transition probabilities, and a fixed initial state; paths carry label traces.Source: §III · p. 3, A. Markov chain · p. 3

B. Deterministic Rabin Automaton

The paper represents ω-regular specifications with deterministic Rabin automata and combines them with Markov chains through a product construction. Model checking then becomes reachability analysis of accepting BSCCs, solved using existing algorithms such as Storm.

  • Deterministic Rabin automata recognize ω-regular languages and can be constructed from LTL formulas.Source: B. Deterministic Rabin Automaton · p. 3
  • A DRA is a five-tuple containing finite positions, atomic propositions, a transition function, an initial position, and a generalized Rabin acceptance condition.Source: B. Deterministic Rabin Automaton · p. 3
  • A run is accepting when some Rabin L-set position occurs infinitely often while every position in the corresponding U-set occurs only finitely often.Source: B. Deterministic Rabin Automaton · p. 3
  • The product MC M ⊗ A tracks MC states and DRA positions, with transitions determined by MC probabilities and the automaton transition function.Labels are retained so paths in M correspond bijectively to product paths starting from a given automaton state.Source: D. The Product Construction · p. 4
  • The model-checking problem reduces to reaching accepting BSCCs, and reachability probabilities can be computed in polynomial time by solving linear equation systems.The proposed preprocessing is followed by reachability computation on the product MC using an algorithm implemented in Storm.Source: D. The Product Construction · p. 4

IV. REPLACEABILITY OF EDGES

The paper defines edge replaceability through acceptance-preserving path suffixes that are compatible with single labels, then constructs a replaced MC by redistributing transition probabilities. The construction is well-defined because the resulting transition function remains probabilistic.

  • Acceptance-preserving words retain membership in each Rabin acceptance set reached by their prefixes.Source: A. Replaceable Edges and Replaced MC · p. 4
  • Two acceptance-preserving words are compatible when they lead every DRA position to the same position.The compatibility relation is an equivalence relation; distinct compatible labels may be identified without changing the automaton's essential behavior.Source: A. Replaceable Edges and Replaced MC · p. 4
  • An edge is replaceable when a set of path suffixes covers every continuation, each suffix is acceptance-preserving and compatible with a single label, and minimality and endpoint-uniqueness conditions hold.The paper gives s0→s1, s1→s4, and s5→s1 as replaceable edges in its example MC.Source: A. Replaceable Edges and Replaced MC · p. 5
  • The unique covering set for a replaceable edge is called the minimum compatible covering suffixes, abbreviated MCCS(e, A).The uniqueness argument relies on the fact that compatible suffixes cannot properly prefix one another.Source: A. Replaceable Edges and Replaced MC · p. 5
  • The replaced MC removes the chosen edge and adds probability mass to replacement edges grouped by compatible label and destination state.The construction defines the new transition function by preserving unaffected probabilities and combining the replaced edge's probability with corresponding MCCS contributions.Source: A. Replaceable Edges and Replaced MC · p. 5
  • The construction of R(M, e) is well-defined: its new transition function forms a valid transition probability.Source: A. Replaceable Edges and Replaced MC · p. 5

B. Correctness of Replaced MCs

The replacement construction preserves the satisfaction probability of a fixed automaton specification by replacing suitable edges with path-covering transitions. Its correctness follows by relating accepting bottom strongly connected components and corresponding path probabilities in the original and replaced product MCs.

V. ERASABILITY OF STATES

Erasability identifies non-initial states whose incoming edges can all be safely shortcut, enabling their removal while preserving satisfaction probability. The resulting erased MC is well-defined and correct under the replacement theorems.

  • The algorithm attempts to eliminate non-initial states one by one by checking replaceability for every incoming edge.Source: §V · p. 7
  • A state is erasable when it is non-initial and all of its incoming edges are replaceable.Source: §V · p. 7
  • Erasable states can be removed to construct an equivalent MC that excludes those states.Source: §V · p. 7
  • The erased MC is well-defined, and Theorem 27 states that erasing an erasable state preserves the satisfaction probability.Source: §V · p. 7
  • If no erasable states exist under the stated acceptance-preserving condition, every non-initial state has a self-loop.Source: §V · p. 7

VI. SPECIFICATION-GUIDED PATH SHORTCUTTING

Specification-guided path shortcutting abstracts an MC relative to a deterministic Rabin automaton by repeatedly identifying replaceable edges and erasable states. A bounded MCCS procedure makes this abstraction practical while retaining the stated correctness guarantee.

  • Algorithm 1 abstracts an MC with respect to a DRA by attempting to remove each non-initial state once.Source: §VI · p. 7
  • Replaceability is monotone under edge replacement: an edge replaceable after another replacement was already replaceable before it.Source: §VI · pp. 7–8
  • The bounded MCCS construction explores candidate paths up to length K and rejects an edge when construction fails or a target state reappears.Source: §VI · p. 8
  • When every incoming edge of a state has an MCCS, the algorithm removes that state, and Theorem 27 guarantees unchanged satisfaction probability.Source: §VI · p. 8
  • The abstraction is denoted M/∼A and is designed to reduce the MC with respect to the specification automaton.Source: §VI · p. 8

VII. EXPERIMENTAL EVALUATION

The evaluation implements specification-guided path shortcutting in Storm-SGPS and studies its efficiency, isolated contribution, interaction with bisimulation minimization, and sensitivity to the MCCS bound K.

  • Storm-SGPS is implemented in C++ using Spot 2.15.13 and integrates MC translation, DRA construction, abstraction, product processing, and Storm model checking.Source: §VII · p. 8
  • The experiments compare Storm-SGPS with Storm on the efficiency of probabilistic model checking.Source: §VII · p. 8
  • The evaluation isolates shortcutting by comparing the full Storm-SGPS workflow with the same workflow without shortcutting.Source: §VII · p. 8
  • Additional research questions examine combining shortcutting with bisimulation minimization and sensitivity to the MCCS bound K.Source: §VII · p. 8

A. Benchmarks

The evaluation uses six Markov-chain benchmarks with multiple LTL properties, including several original formulas designed to be more complex than prior benchmark properties.

Benchmark suite

  • The six benchmarks are BRP, CROWDS, EGL, Leader, NAND, and HM, each paired with multiple LTL formulas.The MCs and formulas are summarized in Tables I and II.Source: A. Benchmarks · p. 8

Formula design

  • Most LTL formulas are original and were designed to be more complex than the properties in the QComp source files.Source: A. Benchmarks · pp. 8–9

Benchmark descriptions

  • BRP models a bounded retransmission protocol for sending files over a lossy channel with bounded retransmissions.Source: A. Benchmarks · p. 8
  • CROWDS represents an anonymity protocol for web browsing, while EGL represents a probabilistic contract-signing protocol.Source: A. Benchmarks · p. 9
  • Leader models synchronous leader election, and its formulas are taken from prior work.Source: A. Benchmarks · p. 9
  • NAND models NAND multiplexing for constructing reliable circuits from unreliable components, while HM was used to motivate a model-checking algorithm.Source: A. Benchmarks · p. 9

B. Experiments

The experiments compare Storm-SGPS with Storm under controlled hardware and repeated runs. Storm-SGPS usually reduces end-to-end time, especially when shortcutting reduces states or specifications are complex, but preprocessing overhead and product growth can reverse the benefit.

Experimental setup

RQ1 results

RQ1 caveats

RQ1 conclusion

  • Storm-SGPS usually reduces end-to-end execution time, particularly when specification-guided path shortcutting substantially reduces the state space.Source: C. RQ1: Comparison with Storm · p. 10

D. RQ2: Isolating the Contribution of Path Shortcutting

The isolation study finds that DRA product construction and label reduction already improve model-checking efficiency, while path shortcutting adds further gains when it substantially reduces the state space.

Baseline decomposition

Cost of shortcutting

Benefits of shortcutting

Contribution of shortcutting

Bisimulation comparison

RQ3 conclusion

F. RQ4: Sensitivity to the MCCS Bound K

Across selected formulas, varying the MCCS bound K did not change the number of reduced states, and small-to-moderate bounds were generally sufficient. The abstraction also produces specification-focused MCs that can be easier to interpret.

K sensitivity

K selection

Interpretability

Scope and future work

  • The current approach is limited to MCs and its proof does not directly apply to products with unambiguous Büchi automata that may yield non-stochastic weighted systems.Source: §IX · p. 13
Loading 2609.02457v1…