PaperlayerView exact revision on arXiv

Source-linked AI summary

Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems

Maxence Dutreix, Samuel Coogan

arXiv:1903.02191v2eess.SP

TL;DR

Verifying continuous-state stochastic systems against expressive ω-regular specifications requires finite abstractions, while exact transition probabilities may be costly to obtain. This paper constructs IMC abstractions for mixed-monotone systems, verifies specifications through Rabin-product reachability, and refines uncertain regions; it demonstrates the approach in two examples.

  • Problem

    Continuous-state stochastic systems need finite abstractions for ω-regular verification, but exact transition bounds can require costly state-space searches and existing methods may rely on fine gridding.

    Source: §I · p. 1

  • Method

    The paper constructs IMC abstractions for mixed-monotone systems with affine disturbances and uses Rabin-product reachability plus specification-guided refinement to verify ω-regular properties.

    Source: §I · pp. 1–2, §VIII · p. 13

  • Results

    The authors report an efficient IMC construction procedure and demonstrate the practicality of their verification and refinement approach in two examples.

    Source: §IV · p. 6, §VIII · pp. 13–14

  • Takeaways & Limitations

    The method targets regions likely to confirm or destroy winning and losing components in the product IMC, refining the partition toward a chosen precision threshold.

    Source: §VIII · pp. 13–14

    The abstraction procedure is presented for mixed-monotone systems with affine disturbances and rectangular partitions.

    Source: §I · p. 1, §IV · p. 6

Abstract

from arXiv · show

This paper addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mixed monotone dynamics. This class has recently been show to be amenable to efficient reachable set computation and models a wide-range of physically relevant systems. In general, finite-state abstractions of continuous state stochastic systems give rise to augmented Markov Chains wherein the probabilities of transition between states are restricted to an interval. We present a procedure to compute a finite-state Interval-valued Markov Chain abstraction of discrete-time, mixed monotone stochastic systems subject to affine disturbances given a rectangular partition of the state-space. Then, we suggest an algorithm for performing verification against omega-regular properties in IMCs. Specifically, we aim to compute bounds on the probability of satisfying the specification of interest from any initial state in the IMC. This is achieved by solving a reachability problem on sets of so-called winning and losing components in the Cartesian product between the IMC and a Rabin automaton representing the specification. Next, the verification of IMCs may yield a set of states whose acceptance status is undecided with respect to the specification, requiring a refinement of the abstraction. We describe a specification-guided approach that compares the best-case and worst-case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study.

I. INTRODUCTION

The paper develops finite-state IMC abstractions and verification methods for stochastic systems with mixed-monotone dynamics and ω-regular specifications. It also introduces specification-guided refinement that targets regions based on best- and worst-case path behavior.

I. INTRODUCTION

  • Exact-probability Markov-chain models may be unrealistic for abstracted continuous-state systems, while computing tight IMC transition bounds can require costly state-space searches.The proposed approach exploits system structure to avoid that computational blowup while retaining conservative bounds sufficient for verification.Source: §I · p. 1
  • Mixed-monotone systems with affine, unimodal, symmetric disturbances admit IMC transition bounds using two integrals per dimension and transition.The resulting conservative ranges remain suitable for verification.Source: §I · pp. 1–2
  • The approach extends IMC verification beyond PCTL to ω-regular properties, which include LTL and properties such as liveness.Existing IMC verification algorithms discussed here address PCTL.Source: §I · p. 2
  • The verification algorithm computes best- and worst-case satisfaction bounds by reachability analysis in the product of an IMC and a specification’s Rabin automaton.It identifies winning and losing components and bounds the probability of reaching them.Source: §I · p. 2
  • Specification-guided refinement selects states using best- and worst-case accepting paths and the product IMC’s largest and permanent components.This targets regions with high potential to reduce uncertainty rather than relying only on one-step transitions.Source: §I · p. 2
  • Compared with the preliminary conference papers and, this work does not require computing the specification complement and provides a more advanced partition-refinement algorithm.The paper reports preliminary results in those conference papers.Source: §I · p. 2

II. PRELIMINARIES

The preliminaries represent ω-regular properties with deterministic Rabin automata and define acceptance through the states visited infinitely or finitely often. They also establish the elementwise ordering and rectangular-set conventions used in the paper.

II. PRELIMINARIES

  • A deterministic Rabin automaton is a tuple containing states, an alphabet, a transition function, an initial state, and an acceptance condition of Rabin pairs.Each Rabin pair consists of sets E_i and F_i.Source: §II · p. 2
  • A run is accepting when, for some Rabin pair, it visits F_i infinitely often and E_i only finitely often.A word is accepted when it produces an accepting run.Source: §II · p. 3
  • Every LTL-defined property is ω-regular and therefore is accepted by a Rabin automaton.The text refers readers to [1, Section 4.3.1] for fuller definitions.Source: §II · p. 3
  • Vector inequalities are interpreted elementwise, and a rectangular set Q_j has least and greatest points a_j and b_j.The rectangular set is specified by a_j ≤ x ≤ b_j.Source: §II · p. 3

III. PROBLEM FORMULATION

The problem formulation models continuous-state stochastic dynamics through rectangular finite-state partitions and IMC abstractions, then asks for satisfaction bounds and refinement against a probabilistic specification. The framework preserves uncertainty in transitions and permits iterative refinement of states whose specification status remains undecided.

III. PROBLEM FORMULATION

  • The system evolves as x[k + 1] = F(x[k], w[k]), where the continuous state and disturbance remain in the domain and disturbance set, respectively.The disturbance is sampled from a density, and a labeling function maps states to an alphabet that generates words along paths.Source: §III · p. 3
  • A rectangular partition divides the compact domain into compact rectangular states with disjoint interiors, and each state respects the labeling boundaries.The domain is assumed amenable to such a partition.Source: §III · pp. 3–4
  • An IMC abstraction assigns lower and upper transition-probability bounds to partition states, capturing the differing probabilities of continuous states within one discrete state.The abstraction uses the partition as its state set and is interpreted as an IMDP.Source: §III · pp. 3–4
  • For an ω-regular property, verification seeks lower and upper satisfaction-probability bounds from each initial IMC state under the induced transition choices.The bounds support classifying states as satisfying, not satisfying, or undecided with respect to the probability-threshold formula.Source: §III · p. 4
  • The first subproblem is to construct a non-trivial IMC abstraction from a rectangular partition for an affine-in-disturbance stochastic mixed-monotone system.A trivial abstraction with every transition ranging from 0 to 1 is always possible, but tighter bounds depend on system dynamics and partition geometry.Source: §III · p. 4
  • When too many states remain undecided, the partition is refined and verification repeated until a chosen precision level is reached.The proposed targeting method selects states with the greatest potential to reduce specification-dependent uncertainty while avoiding state-space explosion.Source: §III · p. 4

IV. IMC ABSTRACTION OF MIXED MONOTONE SYSTEMS AFFINE IN DISTURBANCE

The section constructs an IMC abstraction for mixed-monotone systems with affine disturbances by bounding transition probabilities over a rectangular partition. Its computation uses extremal reachable-set bounds and optimizes disturbance shifts under symmetry and unimodality assumptions.

Reachable-set bounds

  • Mixed monotonicity over-approximates a rectangle’s one-step reachable set using the decomposition function at two extremal points.The enclosing rectangle is bounded by g(a, b) and g(b, a).Source: §IV · p. 5

Assumptions

  • The abstraction requires mixed-monotone dynamics on a rectangularly partitioned domain and independent, symmetric unimodal disturbance components.Each disturbance component has an interval support and a density with a unique mode.Source: §IV · p. 5

Transition-probability bounds

  • For symmetric unimodal disturbances, maximum overlap places the distribution peak as near the target interval’s center as allowed, while minimum overlap places it farthest from the maximizing shift.The shift is restricted to the reachable interval.Source: §IV · p. 6, Figure 2 · p. 6

IMC abstraction

  • Theorem 1 combines Lemma 1 and Proposition 2 to give a procedure for constructing an IMC abstraction of system (6) from a rectangular partition of its domain D, under Assumptions 1–3.Source: §IV · p. 6

Computational cost

  • The computation uses 2n evaluations of disturbance CDFs per transition bound and linear-in-n operations to find maximizing and minimizing shifts.The decomposition function is evaluated at only two points for the reachable-set over-approximation.Source: §IV · p. 6

V. VERIFICATION OF IMCS

The section verifies omega-regular specifications on IMCs by pairing the IMC with a Rabin automaton and bounding satisfaction probabilities. It identifies winning and losing components across induced product chains, then uses these components to compute bounds.

Satisfaction bounds

  • The verification computes lower and upper bounds on the probability that paths from each initial IMC state satisfy the omega-regular property.The bounds correspond to best- and worst-case outcomes over adversaries inducing product Markov chains.Source: §V · pp. 6–7

Product construction

  • The method forms a product of the IMC and a deterministic Rabin automaton recognizing the specification, with initial product states paired to the automaton’s initial state.The automaton represents the omega-regular property being checked.Source: §V · p. 7

Why verification is challenging

  • A product IMC may induce different accepting and non-accepting BSCCs as transition bounds permit transitions to be on or off.The figure’s two induced product Markov chains illustrate that all states may be non-accepting in one chain even when another has accepting states.Source: §V · pp. 7–8, Figure 3 · p. 8

Winning and losing components

  • Largest winning and losing components contain states that reach an accepting or non-accepting BSCC with probability 1, respectively.Reachability probabilities for these sets are used to compute satisfaction bounds.Source: §V · pp. 7–8

Graph search and refinement

  • The component-finding procedure uses graph search, and permanent winning and losing components are used by the refinement algorithm.The components help determine which regions matter for refinement.Source: §V · pp. 7–8

A. Computation of Satisfiability Bounds in IMCs

This section establishes that satisfaction-probability bounds in an IMC can be computed through reachability to fixed winning and losing components in its product with a Rabin automaton. It characterizes these components and identifies graph search and reachability computation as the route to the bounds.

A. Computation of Satisfiability Bounds in IMCs

  • Largest components include states belonging to a winning or losing component for at least one induced product Markov chain, including states outside BSCCs that are bound to reach one.Source: A. Computation of Satisfiability… · p. 8
  • Potential winning and losing sets may intersect, whereas permanent winning and losing sets are disjoint; largest-component states can occur together in a winning or losing component in an induced chain.Source: A. Computation of Satisfiability… · p. 8
  • Satisfaction bounds for any initial IMC state reduce to reachability probabilities for fixed largest winning and losing components in the product IMC.The theorem also identifies induced product Markov chains that attain the worst- and best-case reachability probabilities.Source: A. Computation of Satisfiability… · pp. 8–9
  • The procedure finds largest components by graph search, then uses reachability algorithms to compute bounds from all product states.Transitions within the components do not affect the reachability probabilities.Source: A. Computation of Satisfiability… · p. 9

B. Winning and Losing Components Search Algorithm

This section presents a graph-based procedure for finding potential and permanent BSCCs and deriving winning and losing components in product IMCs. The algorithms use SCC decomposition and iterative removal of leaky states.

B. Winning and Losing Components Search Algorithm

  • Algorithms 1 and 2 find potential and permanent BSCCs, then derive potential and permanent winning and losing components; the largest components are their unions.Source: B. Winning and Losing Components… · p. 9
  • Algorithm 1 builds a graph from transitions with nonzero upper bounds, finds its SCCs, and tests whether each can be a BSCC under an induced Markov chain.A state is checked for whether its outgoing transitions can be turned off while the within-component upper bounds sum to more than 1.Source: B. Winning and Losing Components… · p. 9
  • Algorithm 1 iteratively removes leaky states and rechecks the remaining SCCs; Rabin-pair mappings determine whether the resulting BSCCs are accepting.Source: B. Winning and Losing Components… · pp. 9–10
  • Algorithm 2 works backward from BSCCs, repeatedly removing states that leak toward trap states; remaining states inherit the BSCC's winning or losing status.Source: B. Winning and Losing Components… · p. 10
  • The proposed verification avoids constructing the exponentially large Markov decision process used in.Source: B. Winning and Losing Components… · p. 10

VI. STATE-SPACE REFINEMENT

The refinement procedure uses the specification and best- and worst-case path behavior to target uncertain states, then repeats abstraction and verification until the uncertain-state volume meets a threshold. Path scoring prioritizes states that could change potential winning or losing components.

VI. STATE-SPACE REFINEMENT

  • Refinement iterates between scoring states, partitioning high-scoring states, rebuilding the IMC, and verifying until the uncertain-state volume is at most Vstop.The procedure starts from a rough partition and targets states for reducing uncertainty with respect to the specification.Source: §VI · pp. 11–12
  • For each undecided state, the algorithm explores best-case paths and scores encountered states according to their behavior in the worst-case product MC.Exploration stops at a losing or winning component, or when path probability falls below pstop.Source: §VI · p. 11
  • Potential winning or losing components receive refinement scores for states inside related potential BSCCs whose outgoing transitions can be on or off.The heuristic estimates possible reduction in the satisfaction-interval width if refinement fixes the probability of reaching an accepting BSCC.Source: §VI · pp. 11–12
  • Paths stop exploring a region when they reach a permanent winning or losing component, which does not require refinement.The path search also returns when a path falls below pstop or all continuations have been explored.Source: §VI · p. 11
  • The uncertain-state volume need not decrease at every refinement step, but for continuous F it tends to zero as grid size decreases.Refining a parent into children can increase the sum of their upper transition bounds relative to the parent's bound.Source: §VI · p. 12
  • Worst-case product-IMC growth is exponential, O(|S| · 2|Q|), if the scoring procedure selects the entire state-space for refinement.The stated common refinement splits selected partition states in half along their greatest dimension.Source: §VI · p. 12
  • Path-based scoring focuses refinement on specification-relevant regions and reached lower uncertainty-volume thresholds before partition size became prohibitive versus refining all undecided states.The comparison is with the naive method in.Source: §VI · p. 12

VII. CASE STUDY

In a bistable-switch case study, specification-guided refinement produced different partitions for two temporal objectives. The method used fewer undecided states than a baseline in one reported comparison, while its specification-specific partitions suit objectives known in advance.

VII. CASE STUDY

  • The case study uses independent truncated Gaussian disturbances and rectangular partitions, with selected states split along their largest dimension.States scoring above 10% of the highest score were refined; stopping thresholds were Vstop = 0.13 for φ1 and 0.1 for φ2.Source: §VII · p. 12
  • 3531 states in 1h56min for φ1 and 4845 states in 3h15min for φ2; for φ1, reached V? = 0.2137 in 2 hours 58 min.The proposed refinements terminated after 12 steps for φ1 and 13 for φ2; used 11 steps in the comparison.Source: §VII · pp. 12–13
  • The φ1 and φ2 figures show initial partitions above final partitions, coloring satisfying states green, violating states red, and undecided states yellow.The specifications concern probabilistic LTL objectives with different Rabin automaton sizes: 5 states for φ1 and 7 for φ2.Source: §VII · p. 12, Figure 6 · p. 13, Figure 7 · p. 13
  • The φ1 and φ2 partitions differ despite sharing the same dynamics, with refinement concentrating on regions important to each specification.For φ1, boundaries involving reachability to A and remaining in A for one or two steps were targeted; for φ2, edges of a region leading to A via B were targeted.Source: §VII · p. 13
  • Because partitions depend on temporal objectives, the method suits specifications known a priori, while FAUST2 better accommodates analysis across numerous specifications.The paper states that FAUST2 permits only bounded-time temporal operators.Source: §VII · p. 13

VIII. CONCLUSION

The paper concludes that its IMC-based verification and refinement algorithms address ω-regular properties for continuous-state stochastic systems. Two examples demonstrate the practicality of targeting states likely to confirm or destroy winning and losing components.

VIII. CONCLUSION

  • The approach combines IMC abstraction, ω-regular verification, and specification-guided refinement of continuous-domain partitions.The refinement targets states likely to confirm or destroy winning and losing components in a product IMC.Source: §VIII · pp. 13–14
  • Two examples demonstrate the practicality of targeting states likely to confirm or destroy winning and losing components in a product IMC.Source: §VIII · p. 14

A. Proof of Proposition 2

The proof establishes the bound using a rectangular enclosure of the reachable set, independence of disturbance components, and a symmetric argument for the upper bound.

A. Proof of Proposition 2

B. Proof Lemma 1

The proof establishes the extrema in Lemma 1 using monotonicity, then derives the IMC validity result and develops component-based reachability arguments. In the appendix, it proves how winning and losing components can be combined or enlarged under stated conditions.

B. Proof Lemma 1

  • The maximum and minimum of H on [r1,r2] occur at the points nearest to and farthest from smax, respectively.The proof uses that H decreases as |smax − s| increases.Source: B. Proof Lemma 1 · p. 14
  • Symmetry and unimodality of fω make the integral in (22) nonnegative and decreasing as |smax − s| increases.This establishes the monotonicity claim used to prove the extrema.Source: B. Proof Lemma 1 · p. 14

C. Proof of Theorem 1

  • The proof combines the stated inequalities to conclude that I = (P, T, bT) is a valid IMC.The argument invokes Lemma 1 and Proposition 2 before deriving the defining bounds.Source: C. Proof of Theorem 1 · p. 14

APPENDIX II LEMMAS AND PROOFS OF SECTION V

  • Every infinite state sequence in a Markov chain eventually reaches a bottom strongly connected component.The appendix states this as Lemma 2.Source: APPENDIX II LEMMAS AND PROOFS OF… · p. 14
  • If two state sets reach the same BSCC with probability 1 under possibly different induced chains, one induced chain makes their union reach it with probability 1.The construction uses the first chain's transitions on C1 and the second's on C2 outside their intersection.Source: APPENDIX II LEMMAS AND PROOFS OF… · p. 14
  • An induced product Markov chain can have a losing component containing the losing components of any given induced chain.The proof invokes the existence of a largest set of non-accepting BSCCs.Source: APPENDIX II LEMMAS AND PROOFS OF… · pp. 14–15
  • An induced product Markov chain can have a winning component containing the winning components of any given induced chain.Lemma 7 states existence of such a chain and component.Source: APPENDIX II LEMMAS AND PROOFS OF… · p. 15
  • Lemma 10 states that induced chains exist with permanent winning and largest losing components, and with permanent losing and largest winning components.These paired component-set configurations are asserted for the product IMC.Source: APPENDIX II LEMMAS AND PROOFS OF… · p. 15
Loading 1903.02191v2…