PaperlayerView exact revision on arXiv

Source-linked AI summary

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre

arXiv:1101.3694v2cs.LO

TL;DR

The paper asks how to determine the probability that a finite CTMC satisfies a linear real-time specification given by a DTA. It constructs an embedded PDP and relates satisfaction to reachability there; quantitative analysis uses integral equations, with a single-clock reduction to CTMC transient probabilities.

  • Problem

    The paper asks for the probability that paths of a finite CTMC are accepted by a linear real-time DTA, a setting where the product has an infinite state space and is neither a CTMC nor a DTA.

    Source: §1 · pp. 2–3

  • Method

    The authors adapt the timed-automata region construction to obtain an embedded PDP and characterize reachability probabilities with Volterra integral equations, approximated by PDE solutions.

    Source: §1 · pp. 3–4

  • Results

    For finite acceptance, satisfaction probability equals reachability probability in the embedded PDP; for Muller acceptance, it equals reachability of accepting terminal strongly connected components.

    Source: §1 · pp. 3–4

  • Takeaways & Limitations

    For single-clock DTA, the integral-equation system becomes linear equations with ODE-solved coefficients that are CTMC transient probabilities, so standard CTMC algorithms suffice.

    Source: §1 · p. 4

    The single-clock equation transformation fails for two-clock DTA because after a reset one clock may be fixed while the other remains undetermined.

    Source: §4.2 · p. 31

Abstract

from arXiv · show

We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.

1. Introduction

The paper asks how to compute the probability that a finite CTMC satisfies a linear real-time specification expressed as a deterministic timed automaton. It reduces verification to reachability in an embedded PDP, with integral- and differential-equation analyses for quantitative probabilities.

1. Introduction

  • Prior work on untimed linear specifications reduces CTMC verification to reachability in a product with the embedded DTMC.That reduction does not suffice when the DTA constrains event timing.Source: §1 · pp. 2–3
  • The central problem is computing the probability that a CTMC path is accepted by a DTA specifying linear real-time behavior.Timing constraints make the product more difficult than untimed verification: the product has an infinite state space and is neither a CTMC nor a DTA.Source: §1 · pp. 2–3
  • For finite acceptance, satisfaction probability equals reachability probability in the embedded PDP; for Muller acceptance, it equals reachability of accepting terminal strongly connected components.Qualitative verification reduces to graph traversal of the embedded PDP.Source: §1 · pp. 3–4
  • The authors show that reachability probabilities in the PDP are characterized by least solutions of Volterra integral equations and approximated by solutions of PDEs.For single-clock DTA, the integral equations become linear equations with coefficients given by solutions of ODEs.Source: §1 · p. 4

Related work.

  • Related approaches asCSL and CSLTA address some real-time specifications, but the paper states that the CSLTA technique does not generalize to multiple clocks.The paper says its approach does not restrict the number of clocks and covers the robot example, which neither CSLTA nor asCSL can express.Source: Related work · p. 4

Organization of the paper.

  • The paper extends conference paper with complete proofs, illustrative examples, and Muller acceptance criteria.The paper is organized around model definitions, the CTMC–DTA product, finite-acceptance verification, and then Muller and qualitative verification.Source: Organization of the paper · pp. 4–5

2. Preliminaries

The preliminaries introduce CTMCs, deterministic timed automata, and PDPs, then define how to embed a PDP as a discrete-time Markov process.

2.1. Continuous-time Markov chains.

  • A CTMC has finite labeled states, an initial distribution, transition probabilities, and state-specific exit rates that govern residence times.Its embedded DTMC retains the states, labels, initial distribution, and transition probabilities while deleting exit rates.Source: §2.1 · p. 5

2.2. Deterministic timed automata.

  • A DTA uses clocks, guarded transitions, and resets; determinism requires disjoint guards on same-symbol outgoing edges, and acceptance may be reachability-based or Muller.The paper excludes diagonal clock constraints, while noting that this restriction does not harm expressiveness.Source: §2.2 · pp. 6–7

2.3. Piecewise-deterministic Markov processes.

  • A PDP combines discrete locations with continuous variables whose within-location evolution is specified by a flow function, alongside exit rates and transition probabilities.It can evolve by deterministic delay, a Markovian jump, or a forced jump at an invariant boundary.Source: §2.3 · p. 8

2.4. Embedded PDP.

  • The embedded discrete-time Markov process retains the PDP state space and assigns one-jump transition probabilities that account for both Markovian jumps and boundary jumps.The probability formula includes delays before a Markovian jump and the possibility of reaching the invariant boundary first.Source: §2.4 · p. 9
  • The PDP example has three locations, unit-rate clock flow, constant exit rate 5, and a boundary at x = 2 in location z0.From (z0, 0), the boundary is reached after two time units; the example distinguishes transitions before that time from the forced boundary jump.Source: §2.4 · p. 9

3. The Product of a CTMC and a DTA

The section shows how to represent accepted CTMC paths through the product with a DTA and compute their probability as a reachability probability. It constructs a PDP from the product DMTA using a region construction and simplifies its region graph by merging boundary regions with their successors.

3. The Product of a CTMC and a DTA

  • Adapting the timed-automata region construction to the product yields a PDP for effective reachability-probability computation.The analysis of these PDPs is deferred to the following sections.Source: §3 · p. 10

3.1. Measurability.

  • For any CTMC and DTA, the set of CTMC paths accepted by the DTA is measurable, including under reachability and Muller acceptance.The proof treats clock guards including strict, equality, and non-strict constraints.Source: §3.1 · pp. 10–12

3.2. The product of a CTMC and a DTA.

  • A DMTA combines finite locations and clocks with an exit rate per location and probabilistic target distributions on edges; it supports reachability or Muller acceptance.Residence time in a location is exponentially distributed according to its exit rate, and the edge relation is deterministic.Source: §3.2 · pp. 12–13

DMTA semantics.

  • A DMTA one-jump probability combines the exponential residence-time distribution, a guard indicator, and the probability of the selected transition, defining a well-defined path probability measure.Probabilities of cylinder sets are defined recursively from one-jump probabilities and suffix-cylinder probabilities.Source: DMTA semantics · pp. 13–14

3.3. Product DMTA.

  • The synchronous product pairs CTMC states with DTA states, using CTMC labels as DTA inputs and carrying over the CTMC transition probabilities and exit rates.The DTA's determinism ensures the product is deterministic.Source: §3.3 · pp. 14–15
  • The product gives a one-to-one correspondence between accepted CTMC paths and accepting product paths, and the satisfaction probability equals reachability probability in the product.The product result applies to DTA with reachability or Muller acceptance.Source: §3 · p. 10, §3.3 · p. 15

3.4. Region graph construction.

  • Each region-graph vertex pairs a DMTA location with a clock region, and accepting vertices are those whose location is accepting.The graph's vertex set is finite.Source: §3.4 · p. 18
  • The construction merges boundary regions with their unique non-boundary successors because Markovian edges from boundary regions do not affect reachability.The clock equivalence also merges boundary regions into non-boundary regions; the stated reason is that time to hit the boundary is always zero.Source: §3.4 · p. 18
  • Applying the timed-automata region construction to a DMTA yields a PDP, reducing verification to analyzing that process.The construction is stated for finite acceptance conditions; the Muller case differs only in its acceptance set and is treated in Section 5.Source: §3.4 · pp. 17, 19

4. Verifying CTMCs Against Finite DTA Specifications

This section studies verification of CTMCs against finite DTA specifications by reducing acceptance probabilities to reachability in an embedded PDP and characterizing their computation. For single-clock DTA, it gives an ODE-based linear-system approach; this approach does not extend to two-clock DTA because after a reset the other clock’s value may be undetermined.

Characterizing reachability probabilities.

  • For unbounded reachability, the embedded PDP preserves the original PDP’s locations and discrete probabilistic evolution while abstracting away timing.The embedded process is time-abstract, which supports determining reachability of untimed events.Source: Characterizing reachability… · p. 19, §4 · p. 19
  • Accepted-path probabilities are characterized as the least solution of a Volterra integral equation system for reachability in the embedded PDP.The equations need not have a unique solution; the reachability probability is the least fixpoint of their integration operator.Source: Characterizing reachability… · p. 21

Approximating reachability probabilities.

  • Reachability probabilities can be approximated with a system of PDEs by bounding the time within which the DTA must accept a path.The construction adds a never-reset clock and restricts guards on incoming edges to accepting locations with z ≤ tf.Source: Approximating reachability probabilities · pp. 24–25

4.2. Single-clock DTA♦specifications.

  • For single-clock DTA, verification reduces to linear equations whose coefficients are solutions of ODEs for transient CTMC probabilities.The region graph is partitioned into subgraphs that correspond to CTMCs; standard CTMC methods such as uniformization can solve the ODEs.Source: §4.2 · pp. 25, 26, 28
  • Solving the linear system yields the probability of reaching the accepting vertices from the initial vertex.The solution vector U0(0) contains the reachability probability.Source: §4.2 · p. 30
  • The equations represent delay transitions between subgraphs and Markovian transitions with reset back to G0.In the augmented CTMC, reset probabilities describe transitions within Gi followed by a one-step Markovian transition back to G0.Source: §4.2 · p. 30
  • The single-clock approach does not extend to two-clock DTA, since after a reset the other clock's value may remain undetermined.With one clock, resets lead to G0(0) and delays lead to Gi+1(0).Source: §4.2 · p. 31
  • The computation takes O(m^2·|S|·|Loc|·λ·∆c + m^3·|S|^3·|Loc|^3) time.Here m is the number of constants in A, |S| and |Loc| are the numbers of CTMC states and DTA locations, λ is the maximal exit rate, and ∆c is the maximum region width.Source: §4.2 · p. 31

5. Verifying CTMCs Against Muller DTA Specifications

For Muller acceptance, verification reduces to reaching accepting terminal strongly connected components in the product PDP. Qualitative verification can be performed by graph analysis of the PDP, ignoring transition probabilities.

5. Verifying CTMCs Against Muller DTA Specifications

  • In the example region graph, only the component corresponding to LF2 is accepting; sink vertices reachable from ℓ1 and ℓ2 when x ≥ 2 prevent an LF1 component.Accepting bottom components are disjoint, and once entered, the process remains in one with probability one.Source: §5 · p. 31, Figure 11 · p. 32
  • For Muller acceptance, the probability of paths visiting accepting states infinitely often equals the reachability probability of accepting bottom strongly connected components in the embedded PDP.A component is terminal if it cannot be left once entered; an accepting component has all its vertices associated with an accepting location.Source: §5 · pp. 31–32

Verifying qualitative specifications.

  • Qualitative verification reduces to graph-based CTL model checking on the PDP’s finite digraph, without using transition probabilities.The result characterizes probability-one satisfaction using the weak-until condition stated for the product region graph.Source: Verifying qualitative specifications · p. 33

6. Conclusion

The paper reduces verification of finite CTMCs against timed automata to reachability analysis in PDPs, with specialized ODE-based methods for single-clock specifications. It also identifies nondeterministic timed automata and real-time temporal logics as future directions.

6. Conclusion

  • For finite acceptance, satisfaction probability is PDP reachability, characterized by Volterra integral equations and approximated by PDEs; Muller acceptance reduces to reaching accepting terminal SCCs.These results apply to DTA with any finite number of clocks.Source: §6 · p. 33
  • For single-clock DTA with finite acceptance, verification reduces to linear equations whose ODE coefficients are CTMC transient probabilities, allowing standard CTMC algorithms to suffice.Source: §6 · p. 33
  • Future directions include verification with more expressive nondeterministic timed automata and real-time logics such as metric temporal logic.The proposed approach would require a nondeterministic variant of PDP for nondeterministic timed automata.Source: §6 · p. 33
Loading 1101.3694v2…