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.

  • Method

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

  • Results

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

  • 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.

  • Takeaways & Limitations

    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.

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: Probabilistic model checking is used to verify embedded systems modeled with stochastic behaviors such as communication failures.Markov chains are presented as widely used probabilistic models for such systems.
  • 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.
  • 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.
  • 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.
  • 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.

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.
  • 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.
  • 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.
  • 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.
  • 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.

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.
  • A DRA is a five-tuple containing finite positions, atomic propositions, a transition function, an initial position, and a generalized Rabin acceptance condition.
  • 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.
  • 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.
  • 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.

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.
  • 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.
  • 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.
  • 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.
  • 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.
  • The construction of R(M, e) is well-defined: its new transition function forms a valid transition probability.

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.

  • Theorem 19 establishes that replacing a replaceable edge preserves the specification satisfaction probability.
  • For every edge of the replaced MC, T(s,c,s′) contains paths with matching endpoints whose output labels are compatible with c.
  • A BSCC in the replaced product MC is contained in a unique BSCC of the original product MC, with acceptance preserved in both directions.
  • The example shows that the corresponding original BSCC can be strictly larger than the BSCC in the replaced product MC.
  • The proof decomposes replaced paths into disjoint path families, allowing their probability mass to correspond to paths in the original product MC.

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.
  • A state is erasable when it is non-initial and all of its incoming edges are replaceable.
  • Erasable states can be removed to construct an equivalent MC that excludes those states.
  • The erased MC is well-defined, and Theorem 27 states that erasing an erasable state preserves the satisfaction probability.
  • If no erasable states exist under the stated acceptance-preserving condition, every non-initial state has a self-loop.

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.
  • Replaceability is monotone under edge replacement: an edge replaceable after another replacement was already replaceable before it.
  • The bounded MCCS construction explores candidate paths up to length K and rejects an edge when construction fails or a target state reappears.
  • When every incoming edge of a state has an MCCS, the algorithm removes that state, and Theorem 27 guarantees unchanged satisfaction probability.
  • The abstraction is denoted M/∼A and is designed to reduce the MC with respect to the specification automaton.

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.
  • The experiments compare Storm-SGPS with Storm on the efficiency of probabilistic model checking.
  • The evaluation isolates shortcutting by comparing the full Storm-SGPS workflow with the same workflow without shortcutting.
  • Additional research questions examine combining shortcutting with bisimulation minimization and sensitivity to the MCCS bound K.

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.
  • Formula design: Most LTL formulas are original and were designed to be more complex than the properties in the QComp source files.
  • Benchmark descriptions: BRP models a bounded retransmission protocol for sending files over a lossy channel with bounded retransmissions.
  • Benchmark descriptions: CROWDS represents an anonymity protocol for web browsing, while EGL represents a probabilistic contract-signing protocol.
  • Benchmark descriptions: Leader models synchronous leader election, and its formulas are taken from prior work.
  • Benchmark descriptions: NAND models NAND multiplexing for constructing reliable circuits from unreliable components, while HM was used to motivate a model-checking algorithm.

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: Storm-SGPS was compared with Storm using 30 runs per benchmark and mean execution time, with MCCS bound K = 3 for RQ1.
  • RQ1 results: Storm-SGPS is faster than Storm in most cases, particularly when abstraction substantially reduces states or formulas contain multiple temporal operators.
  • RQ1 results: The resulting product MC has at most two labels in the benchmarks, which can improve efficiency even without state reduction.
  • RQ1 caveats: A speedup during model checking does not always reduce end-to-end runtime because specification-guided shortcutting adds preprocessing overhead.
  • RQ1 caveats: Leader’s model-checking time fell from 0.27 seconds to 0.24 seconds, while total time rose to 0.44 seconds because of shortcutting overhead.
  • RQ1 caveats: Product-MC state-space blow-up can increase execution time, including when formula time bounds are encoded in deterministic Rabin automata.
  • RQ1 conclusion: Storm-SGPS usually reduces end-to-end execution time, particularly when specification-guided path shortcutting substantially reduces the state space.

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: “No Abstraction” is typically faster than Storm, indicating benefits from DRA product construction and label reduction alone.
  • Cost of shortcutting: Removing 17 states in Leader increased model-checking time from 0.038 seconds to 0.24 seconds because product edges grew from 5,268 to 132,103.
  • Benefits of shortcutting: In NAND, states decreased from 18,826,082 to 7,879,952 and end-to-end time from 1064.97 seconds to 493.50 seconds.
  • Benefits of shortcutting: In BRP, reducing states from 5,192 to 3,469 reduced end-to-end time from 0.35 seconds to 0.25 seconds.
  • Contribution of shortcutting: Shortcutting can further improve efficiency when it significantly reduces the state space, although its overhead can make “No Abstraction” faster in some cases.
  • Bisimulation comparison: For NAND, bisimulation reduced “No Abstraction” time from 1064.97 to 1058.30 seconds, whereas combining shortcutting reduced it to 493.48 seconds.
  • RQ3 conclusion: Bisimulation generally improved Storm-SGPS, but its influence was usually less significant than specification-guided path shortcutting.

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: The study evaluated K ∈ {2, 3, 4, 5, 8, 13} on seven formulas, using mean execution time over 30 runs.
  • K sensitivity: Changing K from 2 to 13 did not affect the number of reduced states for the seven formulas.
  • K sensitivity: For most formulas, K had little runtime effect, but CROWDS runtime increased substantially as K increased because deeper MCCS exploration was required.
  • K selection: K = 2 or K = 3 is likely a good practical choice for these benchmarks because the MCCSs needed for effective abstraction are typically short.
  • Interpretability: For HM with K = 3, the abstracted MC has five states instead of 102 and is easier for humans to interpret.
  • Interpretability: The abstracted MC preserves the satisfaction probability of φ1_HM and highlights behaviors relevant to that property.
  • 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.
Loading 2609.02457v1…