﻿Three-Valued Abstraction
for Continuous-Time Markov Chains ⋆
Joost-Pieter Katoen 1 , Daniel Klink 1 , Martin Leucker 2 , and Verena Wolf 3
RWTH Aachen University 1 , TU Munich 2 , University of Mannheim 3 , Germany
Abstract. This paper proposes a novel abstraction technique for continuous-time
Markov chains (CTMCs). Our technique fits within the realm
of three-valued abstraction methods that have been used successfully
for traditional model checking. The key idea is to apply abstraction on
uniform CTMCs that are readily obtained from general CTMCs, and
to abstract transition probabilities by intervals. It is shown that this
provides a conservative abstraction for both true and false for a threevalued
semantics of the branching-time logic CSL (Continuous Stochastic
Logic). Experiments on an infinite-state CTMC indicate the feasibility
of our abstraction technique.
1 Introduction
Continuous-time Markov chains (CTMCs) are an important class of stochastic
processes that are extensively used in a wide range of application domains
ranging from planning of production lines and safety-critical systems to systems
biology. Model checking of CTMCs has been proved to extend and complement
long-standing analysis techniques for Markov processes. Tools for stochastic
Petri nets such as SMART [8] and GreatSPN [9], the PEPA Workbench [12] (a
stochastic variant of the CWB), and Statemate [7] have adopted model checkers
to analyse CTMCs, and temporal logics for Markov chains became prominent
property specification techniques in performance and dependability analysis.
Like for traditional model checking, one of the main challenges in the automated
verification of CTMCs is the state-space explosion problem. This paper
proposes a novel abstraction technique for CTMCs. Abstraction amounts to
obtain smaller models by collapsing sets of concrete states to abstract states.
In two-valued semantics, abstraction is typically conservative in the sense that
affirmative verification results for abstract models carry over to concrete models.
False negatives may occur due to overapproximation. Promising results in
traditional model checking have been obtained for a three-valued semantics of
temporal logic formulae, i.e., an interpretation in which a formula evaluates to
either true, false or indefinite. In this setting, abstraction is conservative for both
positive and negative verification results. Only if the verification of the abstract
⋆ The research has been partially funded by the DFG Research Training Group 1298
(AlgoSyn).
model yields an indefinite answer, the validity in the concrete model is unknown.
The abstraction technique proposed here follows this three-valued approach.
We consider abstractions for the branching-time logic CSL [3], a real-time
probabilistic variant of CTL. CSL is a powerful logic for expressing quantitative
time-bounded constrained reachability properties such as the probability to reach
a set of goal states (by avoiding bad states) within a maximal time span exceeds
7
8
. Existing abstraction techniques in this setting that have been applied in
practice consider either bisimulation [16], matrix bounding [6], simulation [24]
or symmetry reduction [19]. (Due to the absence of nondeterminism, techniques
such as partial-order reduction do not yield substantial reductions.) Despite the
fact that fairly large reductions have recently been reported, more aggressive
abstraction techniques are needed. Such techniques would also be useful to obtain
finite abstractions for a larger class of infinite-state CTMCs.
In traditional model checking, abstract models contain may and must transitions
as over- and under-approximation, respectively of the concrete transition
relation. This concept can be lifted to discrete-time Markov chains (DTMCs)
in a rather natural way [11,14,15] by replacing transition probabilities by intervals
where lower and upper bounds act as under- and over-approximation,
respectively. In this paper we investigate such techniques for CTMCs. The main
technical complication is that besides transition probabilities, one has to determine
the residence time of an abstract state that results from concrete states
with distinct residence times. We show that intervals of transition probabilities,
intervals on residence times (or combinations thereof) are not satisfactory in
terms of precision. Instead, we suggest to overcome this imprecision by using
uniform CTMCs, i.e., CTMCs in which all states have equal residence times
and use transition probability intervals. Note that this is not a restriction, as
any CTMC can be transformed into a weak bisimilar uniform CTMC in linear
time. The abstraction is shown to preserve simulation: concrete states are simulated
by their abstract counterparts. Then we show that extreme schedulers
suffice, i.e., schedulers that only consider lower- and upper bounds. This allows
to compute reachability probabilities up to a given tolerance ε rather efficiently
[2]. Using a three-valued semantics of CSL it is shown that the abstraction is
indeed conservative for affirmative and negative verification results. Besides, we
show the relationship with the approach in [11] for DTMCs. The feasibility of
the approach is shown by considering abstractions of different granularity for an
unbounded stochastic Petri net.
Related work. Abstraction-refinement has been applied to reachability problems
in MDPs [10], partial-order reduction techniques using Peled’s ample-set
method have been generalised to MDPs [13], abstract interpretation has been
applied to MDPs [20], and various bisimulation equivalences and simulation preorders
allow model aggregation prior to model checking, see e. g., [4, 23]. Recent
techniques that have been proposed include abstraction of MDPs by two-player
stochastic games [18], and symmetry reduction [19]. To our knowledge, threevalued
abstraction of continuous-time stochastic models has not been considered.
2 Preliminaries
Let X be a finite set. For Y, Y ′ ⊆ X and function Q : X × X → R≥0 let
Q(Y, Y ′ ) = �
y∈Y,y ′ ∈Y ′ Q(y, y′ ). The function Q(x, ·) is given by x ′ ↦→ Q(x, x ′ )
for all x ′ ∈ X. Furthermore a function f is called a distribution on X iff f :
X → [0, 1] and f(X) := �
x∈X f(x) = 1. Let AP be a fixed, finite set of atomic
propositions and B2 = {⊥, ⊤} the two-valued truth domain.
Definition 1 (DTMC). A DTMC is a tuple (S,P, L) with a finite non-empty
set of states S, transition probability function P : S × S → [0, 1] satisfying
P(s, S) = 1 for all s ∈ S, and labeling function L : S × AP → B2.
P(s, s ′ ) is the one-step probability to move from s to s ′ and L(s, a) states if
atomic proposition a holds in s. A DTMC is time-abstract; in contrast, CTMCs
are time-aware, as they have an explicit reference to time, in the form of exit
rates which determine, together with the transition probabilities, the stochastic
evolution of the system in time.
Definition 2 (CTMC). A CTMC M is a tuple (S,P, E, L) with S, P and L
as before, and exit rate E : S → R>0.
The quantity E(s) determines the random residence time of s, i.e. 1−e −E(s)·t
is the probability to take a transition emanating from s within the next t time
units. (Note that self-loops are admitted.) The probability to move from s to s ′
within t time units is now given by P(s, s ′ , t) := P(s, s ′ )·(1 − e −E(s)·t ).
The time-abstract probabilistic behaviour of CTMC M is described by its
embedded DTMC. The embedded DTMC of CTMC M = (S,P, E, L) is simply
given by emb(M) = (S,P, L). A CTMC is uniform if all its states have the
same exit rate, i.e., E(s) = E(s ′ ) = e for all states s, s ′ ∈ S. Each CTMC can
be transformed into a uniformized CTMC by adding self-loops:
Definition 3 (Uniformisation). Let M = (S,P, E, L) be a CTMC and let
(uniformisation rate) e ∈ R>0 such that e ≥ maxs∈S E(s). Then, unif (M) =
(S,P, E, L) is a uniform CTMC with E(s) = e for all s ∈ S and
P(s, s ′ ) = P(s, s ′ )· E(s)
e for s ′ �= s and P(s, s) = 1 − P(s, S\{s}).
The minimal appropriate value of e is determined by the state in M with the
shortest mean residence time 1 . In unif (M) all rates of self-loops are “normalized”
with respect to e. Thus, transitions occur with an average “pace” of e,
uniform for all states. A CTMC is weak bisimilar to its uniformized CTMC [4].
Continuous Stochastic Logic. CSL [1,3] extends CTL by replacing existential
and universal path quantification by a probability operator (as in PCTL) and
by equipping the until-operator with a time bound (as in timed CTL):
ϕ ::= true | a | ϕ ∧ ϕ | ¬ϕ | P ⊲⊳ p(Ψ) Ψ ::= ϕ U I ϕ
1 Strictly speaking, we should write unif e (M) as the uniformization depends on e.
�s,true� = ⊤ �s, a� = L(s, a)
�s, ϕ1 ∧ ϕ2� = �s, ϕ1� ⊓ �s, ϕ2� �s, ¬ϕ� = �s, ϕ� c
�s, P ⊲⊳ p(Ψ)� = ⊤, iff Prob({σ ∈ Paths M s | �σ, Ψ� = ⊤}) ⊲⊳ p
�σ, ϕ1U I ϕ2� = ⊤, iff ∃ t ∈ I : (�σ@t,ϕ2� = ⊤ ∧ ∀ t ′ ∈ [0, t) : �σ@t ′ , ϕ1� = ⊤)
Table 1. Semantics of CSL
where ⊲⊳ ∈ {<, ≤, ≥, >}, p ∈ [0, 1], I = [0, t) | [0, t] | [0, ∞) for t ∈ R>0 and
a ∈ AP. ϕ is a state-formula, whereas Ψ is a path-formula. State formulas are
ranged over by ϕ, ψ, . . . and path formulas are ranged over by Ψ, Φ, . . . .
A path in a CTMC is an alternating sequence σ = s0 t0 s1 t1 s2 . . . with
P(si, si+1) > 0 and ti ∈ R>0 for all i. The time stamps ti denote the amount
of time spent in state si. σ@t denotes the state of σ occupied at time t, i.e.
σ@t = si with i the smallest index such that t < � i
j=0 tj. Let Prob denote the
unique probability measure on sets of paths and let Paths M s
denote the set of all
paths of M, starting in s. The subscript s is omitted when s is clear from the
context; the same applies to superscript M. Note that the probability measure
of the set of infinite paths s0t0s1t1 . . . with � ∞
i=0 ti is converging, is zero [3].
The semantics of CSL is given in Table 1. ⊤ and ⊥ form a complete lattice
such that ⊥ < ⊤ and meet ⊓ as well as complement · c are defined as usual.
Measures of interest can now be expressed as CSL formula in a convenient
way. For example, the liveness property to reach a down state in a system within
52 time units, via premium states, with probability at most 0.01 would be formulated
as P≤0.01(premium U [0,52] down). Another typical example would be to
check, if some designated goal state is reachable at all times: P>0(trueU [0,∞) goal).
As in our abstraction, states may be grouped that satisfy distinct atomic
propositions, we resort to a three-valued interpretation. Let B3 = {⊥, ?,⊤}
with ordering ⊥ < ? < ⊤ and let ? c = ?. When a formula evaluates to ⊥ or ⊤,
the result is definitely true or false respectively, otherwise it is indefinite.
3 Abstraction
Our aim is to provide an abstraction of CTMCs which is conservative for both
positive and negative verification results of CSL formulas. This is established by
adopting a three-valued interpretation. The basic principle is to collapse sets of
concrete states into single abstract states such that concrete states are simulated
by abstract ones. As opposed to abstract interpretation only disjoint sets of concrete
states are collapsed. That is, we consider a partitioning A = {A1, . . . , An}
of the state space S of a CTMC M = (S,P, E, L). The probability to evolve from
abstract state Ai to Aj, i, j ∈ {1, . . .,n} within some time interval is represented
by the functions: P(Ai, Aj) = {P(s, s ′ , ·) | s ∈ Ai, s ′ ∈ Aj}.
Taking minimal and maximal probabilities as under- and over-approximation,
respectively, suggests to define
P l (Ai, Aj, t) = inf f∈P(Ai,Aj) f(t) and P u (Ai, Aj, t) = sup f∈P(Ai,Aj) f(t).
s
1
3
2
10
3
5
2
u1
100
u2
10
u3
2
5
2
3
8
10
v
Fig.1. Abstraction for non-uniform CTMCs
The functions P l (Ai, Aj, t) and P u (Ai, Aj, t) (considered as functions ranging
over t) are in general not of the form p·(1 −e −E·t ) for fixed p ∈ [0, 1] and E > 0.
Example 1. Consider the non-uniform CTMC M = ({s, u1, u2, u3, v},P, E, L)
in Fig. 1 (left). We focus on the transition probabilities of the states u1, u2, u3 (indicated
as labeled edges) and their exit rates which appear above the corresponding
vertices. Further details of M are omitted in Fig. 1. Let A = {As, Au, Av}
with Au = {u1, u2, u3}, As = {s} and Av = {v}. The set P(Au, Av) = {f, f ′ , f ′′ }
is plotted in Fig. 1 (right). Note that P l (Au, Av, t) and P u (Au, Av, t) are not of
the form p·(1 −e −E·t ). In general, the complexity of these functions grows when
the number of transitions between states aggretated to Au and Av increases.
One might combine the infimum (supremum) of an abstract state’s exit rates
with the infimum (supremum) of the one-step transition probabilities to define an
appropriate under- and over-approximation, yielding a rather coarse abstraction
as indicated in Fig. 1 (right) which shows the plot of the functions g and g ′
resulting from this approach. But increasing the number of parameters to obtain
a more accurate approximation results in a far too complex abstraction.
Therefore, we propose to abstract a CTMC by generating its uniformised
CTMC (cf. Def. 3), and apply abstraction on the uniform CTMC, i.e., CTMCs
in which all exit rates are equal to, say, Eunif . The advantage of uniform CTMCs
is that pl·(1 −e −Eunif·t ) ≤ pu·(1 −e −Eunif·t ) iff pl ≤ pu where pl, pu are the lower
and upper bounds of time-abstract transition probabilities. Note that CTMC
M and unif(M) are weak bisimilar, and as weak bisimulation preserves CSL
equivalence 2 [4], the shift to the uniformized CTMC is correct for CSL. Our
abstract model now becomes:
Definition 4 (Abstract CTMC). An abstract CTMC (ACTMC for short)
is a tuple M = (S,P l ,P u , Eunif, L) with a non-empty finite set of states S,
transition probability functions P l ,P u : S × S ↦→ [0, 1] such that P l (s, S) ≤ 1 ≤
P u (s, S) componentwise for all s ∈ S. Eunif ∈ R>0 is the (global) exit rate for
all states, and L : S × AP ↦→ B3 is a labeling function.
2 Recall that we consider the fragment of CSL without the next-step operator.
An ACTMC M has a finite state space and is equipped with a pair of functions
describing the lower and upper bound, respectively for the one-step transition
probabilities. In contrast to CTMCs, states in an ACTMC may be labeled with
?. The set of transition probability functions is given by
PM = { ¯ P : S × S ↦→ [0, 1] | P l ≤ ¯ P ≤ P u and ¯ P(s, S) = 1 for all s ∈ S},
where ≤ is to be interpreted element-wise. We may drop subscript M if M is
clear from the context and write P(s, ·) for the set { ¯ P(s, ·) | ¯ P ∈ P}.
An ACTMC (S,P l ,P u , Eunif, L) with P l = P u and L(s, a) ∈ B2 for any
s ∈ S and a ∈ AP is a uniform CTMC.
Definition 5 (Abstraction). For ACTMC M = (S,P l ,P u , Eunif, L), partitioning
A = {A1, . . .,An} of S and 1 ≤ i, j ≤ n, the abstraction of M induced
by A is the ACTMC abstr(A, M) := (A, ˜ P l , ˜ P u , Eunif, ˜ L) given by:
– ˜ Pl (Ai, Aj) = mins∈Ai Pl (s, Aj) and ˜ Pu (Ai, Aj) = min{1, maxs∈Ai Pu (s, Aj)},
– ˜ ⎧
⎪⎨ ⊤ if L(s, a) = ⊤ for all s ∈ Ai, a ∈ AP,
L(Ai, a) = ⊥ if L(s, a) = ⊥ for all s ∈ Ai, a ∈ AP,
⎪⎩
? otherwise.
Example 2. Consider the CTMC in Fig. 2
(left) with exit rate 12, AP = {a},
L(s0, a) = L(s1, a) = ⊤ and L(s ′ 0 , a) =
L(s2, a) = ⊥. The ACTMC induced
by partition {{s0, s ′ � ��
0} , {s1} , {s2} } is de-
� ���� ����
s0
s
s1
′ 0
1
4
2
3
1
3
3
4
s2
3
4
1
4
1
A0
[
A1
A2
2 3
3 , 4 ]
[ 1 1
4 , 3 ]
[ 3 3
4 , 4 ]
[ 1 1
4 , 4 ]
[1, 1]
=A0
=A1
=A2
picted in Fig. 2 (right) with L(A0, a) = ?, Fig.2. Abstracting a CTMC
L(A1, a) = ⊤, L(A2, a) = ⊥.
The probability to move from s to s ′ in an ACTMC may be any probability
in [Pl (s, s ′ ),Pu (s, s ′ )] and is chosen nondeterministically. As for Markov
decision processes, schedulers are used to resolve nondeterminism. We consider
(time-abstract) history-dependent schedulers that given a time-abstract path
nondeterministically select a transition probability function from the set P.
Definition 6 (Scheduler). A history-dependent scheduler for ACTMC M is
a function D : Pathsabs(M) ↦→ PM.
Here, Pathsabs(M) denotes the set of time-abstract paths in M. A time-abstract
path in M is a finite sequence of states s0s1s2 . . . sn such that ¯ P(si, si+1) > 0
for some ¯ P ∈ P for all i ∈ {0, 1, . . ., n}. The set of history-dependent schedulers
for ACTMC M is denoted by Sched M .
If only lower and upper bounds on transition probabilities are given, it may
happen that not every combination is possible. For instance, in Example 2, a
< 1.
possible choice in state A0 is to select A1 with 1
4 and A2 with 2 1 2
3 , but 4 + 3
Definition 7 (Delimited ACTMC). An ACTMC M = (S,P l ,P u , Eunif, L)
is delimited iff for any s, s ′ ∈ S and p ∈ [P l (s, s ′ ),P u (s, s ′ )], there exists ¯ P ∈ P
with ¯ P(s, s ′ ) = p.
In the following, we define an operation, called cut, that transforms a given
ACTMC into a delimited one. It basically strips off combinations of probabilities
in the intervals that do not yield transition probabilities. A similar function has
been defined for abstractions of DTMCs (see Def. 11) in [11].
Definition 8 (Cut). Let M = (S,P l ,P u , Eunif, L) be an ACTMC. We define
the functions cut(P l ,P u ) = ( ˜ P l , ˜ P u ) by ˜ P l (s, s ′ ) = max{P l (s, s ′ ), 1 − P u (s, S \
{s ′ })} and ˜ P u (s, s ′ ) = min{P u (s, s ′ ), 1 − P l (s, S \ {s ′ })} for all s, s ′ ∈ S.
The cut of M is defined as cut(M) = (S, ˜ P l , ˜ P u , Eunif, L).
Lemma 1. For ACTMC M, cut(M) is delimited and Sched M = Sched cut(M) .
A finite subset of the transition probability distributions, which will prove
useful when considering lower and upper bounds of reachability properties, is the
set of extreme distributions. Intuitively they result from a one by one minimisation/maximisation
of transition probabilities. Note that different priorities for
minimising/maximising yield different minimal/maximal probabilities. Actually,
the number of extreme distributions grows exponentially in the state space size.
Definition 9 (Extreme distributions). Let s ∈ S and S ′ ⊆ S. We define
extr(P l ,P u , S ′ , s) ⊆ P such that µ ∈ extr(P l ,P u , S ′ , s) iff either S ′ = ∅ and
µ = P l (s, ·) = P u (s, ·) or one of the following conditions is true 3
∃s ′ ∈ S ′ : µ(s ′ ) = P l (s, s ′ ) and µ ∈ extr(P l ,P u [s ′ ↦→ µ(s ′ )], S ′ \ {s ′ }, s)
∃s ′ ∈ S ′ : µ(s ′ ) = P u (s, s ′ ) and µ ∈ extr(P l [s ′ ↦→ µ(s ′ )],P u , S ′ \ {s ′ }, s)
We call µ ∈ P(s, ·) an extreme distribution if µ ∈ extr(P l ,P u , S, s).
To compare the behavior described by two ACTMCs, we introduce the notion
of probabilistic simulation which is a variant of probabilistic simulation for
CTMCs as it can be found in [4].
Definition 10 (Probabilistic simulation). Let M = (S,P l ,P u , Eunif, L) be
an ACTMC. We call R ⊆ S × S a probabilistic simulation iff sRs ′ implies:
1. L(s ′ , a) �= ? ⇒ L(s ′ , a) = L(s, a) for all a ∈ AP.
2. For all distributions µ ∈ P(s, ·), there is a distribution µ ′ ∈ P(s ′ , ·) and a
weight function ∆ : S × S → [0, 1] with:
(a) ∆(u, v) > 0 ⇒ uRv, (b) ∆(u, S) = µ(u), (c) ∆(S, v) = µ ′ (v).
State s is simulated by s ′ (written s � s ′ ) if there exists a probabilistic simulation
R with (s, s ′ ) ∈ R. We lift � to the union of two ACTMCs in the usual way.
Theorem 1. For ACTMC M with state space S, and A a partitioning on S
inducing the ACTMC abstr(A, M) with state space A
s ∈ A ⇒ s � A for all s ∈ S, A ∈ A
3 Here, f[s ↦→ x] denotes the function that agrees everywhere with f except at s where
it is equal to x.
Example 3. Consider the CTMC in Fig. 2(a), the partitioning leading to 2(b)
(see Ex. 2) with R = {(s0, A0), (s ′ 0 , A0), (s1, A1), (s2, A2)}. Note that Ai should
be considered as a single abstract state. We have s0RA0 because condition 1 of
Def. 10 is trivially fulfilled since L(A0, a) = ?. For condition 2 we observe that
in s0 there is only one possible distribution µ = (0, 0, 1 3
4 , 4 ) to choose. The only
distribution in P(A0, ·), for which there is a weight function ∆ fulfilling condition
2, is µ ′ = (0, 1 3
4 , 4 ) with ∆(s1, A1) = 1
4 , ∆(s2, A2) = 3
4 and 0 otherwise. The
conditions of Def. 10 can be checked for the remaining elements of R similarly.
In the following we show that our abstraction of CTMCs can be regarded as
a conservative extension of abstraction of DTMCs as recently proposed in [11].
Definition 11 (Abstract DTMC). An abstract DTMC (ADTMC) is a tuple
(S,P l ,P u , L) with S, P l , P u , and L as before.
Abstract DTMCs are thus abstract CTMCs without exit rates. The theorem
below shows that the following diagram commutes:
embedded
abstr. cut
M Mabstr Mdel
abstr. cut
N Nabstr Ndel
embedded
�y x } (A)CTMCs
�y x } (A)DTMCs
Theorem 2. For delimited uniform CTMC M and partitioning A:
emb(cut(abstr(A, M))) = cutADTMC(abstrDTMC(A,emb(M)))
where cutADTMC and abstrDTMC are the counterparts of cut and abstr in the
setting of (A)DTMCs [11].
4 Model Checking Three-valued CSL
Now, we develop a three-valued version of CSL which is interpreted over ACTMCs.
The simulation relation allows us to reason about more concrete systems.
For an ACTMC M, every scheduler D ∈ Sched M induces a probability space
with a probability measure Prob D in the same manner as for CTMCs (see [3]
for details). When interested in the infimum of probabilities of measurable sets
with regard to all schedulers, it suffices to consider only extreme distributions.
A scheduler which only chooses such distributions is an extreme scheduler. The
set of all extreme schedulers for M is denoted as Sched M extr .
Theorem 3. Let M = (S,P l ,P u , Eunif, L) be an ACTMC. For every measurable
set Q of the induced probability space:
inf D∈Sched M extr Prob D (Q) = inf D∈Sched M Prob D (Q).
The proof for the above theorem is rather technical and goes along the structure
of the generated Borel field of the induced probability space. Note that the
number of choices at a state is finite for extreme schedulers, whereas this is
uncountable for arbitrary schedulers.
Before discussing CSL, let us first consider time-dependent reachability probabilities
in ACTMCs, i. e., the probabilities to reach some state in set B within
t time units, formally Reach≤t(s, B) = {σ ∈ Paths M s | σ@t ′ ∈ B for some
t ′ ∈ [0, t]}. When computing the semantics of CSL formulas, the main challenge
is to determine lower bounds of reachability properties, as we will see. Therefore,
we will now analyse how to compute inf D∈Sched M Prob D (Reach≤t(s, B)).
Prob l (Q) will be used as abbreviation for inf D∈Sched M Prob D (Q).
We start with an algorithm for the approximation of probability bounds for
timed reachability properties in uniform CTMDPs (see [2]). By Theorem 3, it
suffices to consider extreme schedulers if one is interested in lower bounds. We
interpret an ACTMC as a CTMDP, where each extreme distribution can be
chosen by some action. From [2], we know that an ε-approximation of transient
probabilities q0 can efficiently be computed in an iterative way 4 :
q0
= ψEunif,t(0) · iB + q1
qi
= ψEunif,t(i) · iB + Pi · qi+1, for i ∈ {1, ..., k(ε, Eunif, t)},
qk(ε,Eunif,t)+1 = 0, where k(ε, Eunif, t) is a proper truncation point,
and ψEunif,t (n) is the probability that
n events occur in a Poisson process of rate Eunif·t
Therefore, instead of checking for all extreme distributions in each iteration,
we can find a minimizing distribution in polynomial time, by minimizing the
vector-product Pi(s, ·) ·qi+1 with additional constraint qi+1(S) = 1. This can be
done by successively assigning as much proportion as possible to the transition
leading to the successor s ′ for which qi+1(s ′ ) is minimal. For N := |S|, sorting the
q-vector can be done in O(N log(N)) and assertion of probabilities takes O(N 3 )
since the cut has to be applied N times and the cut itself has a complexity of
O(N 2 ). This yields a worst-case complexity of O(N 2 · (N log(N) + N 3 ) + N) =
O(N 5 ) for every iteration step.
The following theorem, which states that the above algorithm yields an εaccurate
approximation of reachability properties, follows directly from [2].
Theorem 4. For ACTMC M = (S,P l ,P u , Eunif, L), s ∈ S, B ⊆ S, t ∈ R>0
and error margin ε:
Prob l (Reach≤t(s, B)) − ε ≤ q0(s) ≤ Prob l (Reach≤t(s, B))
Three-valued CSL-semantics. We define the satisfaction function � · � : (S ∪
Paths M ) × CSL → B3 inductively as shown in Table 2, where Prob l (s, Φ, α) =
Prob l ({σ ∈ Paths M s | �σ, Φ� = α}) for α ∈ B3.
Let us have a closer look at the semantics. For the propositional fragment
the semantics is clear. A path σ satisfies until-formula ϕ1 U [0,t] ϕ2 if ϕ1 holds for
sure until ϕ2 holds for sure at the latest at time t. The until-formula ϕ1 U [0,t] ϕ2
is violated, if either before ϕ2 holds, ϕ1 is violated, or if ϕ2 is violated for sure.
Otherwise, the result is indefinite.
4 The truncation point k(ε, Eunif, t) depends linearly on Eunif and t and can easily be
computed on-the-fly.
�s,true� = ⊤ �s,false� = ⊥ �s, a� = L(s, a)
�s, ϕ1 ∧ ϕ2� = �s,ϕ1� ⊓ �s, ϕ2� �s, ¬ϕ� = �s,ϕ� c
�σ, ϕ1U I 8
<
ϕ2� =
:
? otherwise
⊤ if ∃ t ∈ I : (�σ@t,ϕ2� = ⊤ ∧ ∀ t ′ ∈ [0, t) : �σ@t ′ , ϕ1� = ⊤)
⊥ if ∀ t ∈ I : (�σ@t,ϕ2� = ⊥ ∨ ∃ t ′ ∈ [0, t) : �σ@t ′ , ϕ1� = ⊥)
8
< ⊤ if Prob
�s, P�p(Ψ)� =
:
l (s,Ψ, ⊤) � p
⊥ if Prob l (s,Ψ, ⊥) ⊲ 1 − p
? otherwise
8
< ⊤ if 1 − p � Prob
�s, P�p(Ψ)� =
:
l (s, Ψ, ⊥)
⊥ if p ⊳ Prob l (s, Ψ, ⊤)
? otherwise
� ∈ {>, ≥}, ⊲ =
� ∈ {<, ≤}, ⊳ =
Table 2. Three-valued semantics of CSL.
j > if � = ≥
≥ if � = >
j < if � = ≤
≤ if � = <
To determine the satisfaction of P≤p(Ψ) we consider the probability of the
paths for which Ψ is surely violated. If this probability is greater than 1−p, then
paths where Ψ holds may have measure at most p. Similarly, to show that P≤p(Ψ)
is violated, we have to consider the measure of all paths surely satisfying Ψ. If
this measure is greater than p, then obviously P≤p(Ψ) is violated. The semantics
of P�p(Ψ) for � ∈ {<, >, ≥} follows from a similar argumentation.
Example 4. Consider the CTMC in Fig. 2(a). Starting in s0 (s1), the probability
to reach a non-a-state in 0.3 time units is about 0.9037 (0.9328, respectively).
Thus, formula ϕ = a → P≥0.9(true U ≤0.3 ¬a) is true in all states. Consider the
abstraction in Fig. 2(b): The lower and upper probability bounds to reach a nona-state
in 0.3 time units from A0 are about 0.8807 respectively 0.9037. Hence,
�A0, a → P≥0.9(true U ≤0.3 ¬a)� = ? ⊔ �t0, P≥0.9(true U ≤0.3 ¬a)� = ? ⊔? = ?. For
P≥0.88 instead of P≥0.9, the formula would have been satisfied in the abstraction
as well, while for P≥0.91 the result would still be ? since ? ⊔ ⊥ = ?.
The following theorem states that our framework developed so far can indeed
be used for abstraction based model checking. It can be shown by structural
induction on the CSL formulas. Intuitively, the theorem asserts that the result
of checking a CSL formula in the abstract CTMC agrees with the one for the
more concrete model, unless it is indefinite.
Theorem 5 (Preservation of CSL). Let s and s ′ be two states of an ACTMC
M with s � s ′ . Then for all CSL formulas ϕ:
�s ′ , ϕ� �= ? implies �s, ϕ� = �s ′ , ϕ�.
Observe that the 3-valued CSL semantics on a CTMC (viewed as ACTMC)
coincides with the 2-valued CSL semantics for CTMCs (see Section 2), showing
that our abstraction is conservative for positive and negative verification results.
Model checking. As for CTL, model checking works bottom-up the parse tree of
the CSL formula ϕ. Boolean combinations of formulas as well as the P-formulas
are evaluated, as expected. For the latter, however, we need the lower probability
bounds for the satisfaction/violation of an until-formula, which remains the only
operator to discuss.
The idea of dealing with until-operators is similar as in [11]: For getting the
measure of paths surely satisfying Ψ = ϕ1 U [0,t] ϕ2, it suffices to compute the
measure of reaching states satisfying ϕ2 in time bounded by t along paths of
states satisfying ϕ1. By induction, we know which states do not satisfy ϕ1. Removing
these from the CTMC, a path satisfies ϕ1 U [0,t] ϕ2 iff a state ϕ2 is reached
within time bound t. In other words, it remains to solve a time-bounded reachability
problem in the reduced graph. Getting the measure of paths violating Ψ
for sure, is done similarly by exchanging ⊤ and ⊥ in the argumentation above.
Recall that the given algorithm for computing time-bounded reachability
approximates only with error margin ε. However, it can easily be guaranteed
that the error due to approximation only yields ? in cases where a definite value
could be obtained given a smaller error margin.
Theorem 6. Given an ACTMC M, a CSL formula ϕ, and an error margin
ε, we can approximate �M, ϕ� in time polynomial in size of M and linear in
size of ϕ, Eunif and the highest time bound t occurring in ϕ (dependency on ε is
omitted as ε is linear in Eunif · t). In case the approximation yields ⊤ or ⊥, the
result is correct, while ? is correct with an error of at most ε.
5 Case study: Quasi-Birth-Death Processes
Let us consider a simple system with a fixed number m of available processors and
an infinite queue for storing job requests. The processing speed of the processors
is described by an exponential distribution with rate γ and λ is the incoming rate
of jobs. When all processors are being utilized, new jobs are added to the infinite
queue. As soon as processors are getting available again, jobs from the queue
are processed. To model these spontaneous transitions, we choose a high rate
ǫ ≫ λ. In our experiments about 10 times the incoming rate for tasks has been a
sufficiently precise approximation. The system initially has no job to process, i.e.
all three processors are available and the queue is empty. For m = 3, this is being
formally described by the stochastic Petri net (SPN) [5] in Fig. 3(a). Numbers at
edges denote that the corresponding transition consumes or produces the given
number of tokens and can not be fired until there are enough token to consume.
The semantics of this SPN is equal to an infinite CTMC. Uniformization with
rate E results in the infinite uniform CTMC (Fig. 3(b)). For E, x, y, z ∈ R≥0, we
shortly write E x yz = E x y − z, E x y = E x − y and E x = E − x. State si,j represents
idle
λ
ǫ
γ
queue λ
(a)
busy
E
s3,0
λ
γ
s2,0
λ
γ
s1,0
λ
γ
s0,0
3 3
ǫ ǫ ǫ
λ
s3,1
λ s2,1
λ s1,1
λ s0,1
λ
E λ γ E λ γ E λ γ E
s3,0
λ
γ
s2,0
λ
γ
s1,0
λ
γ
s0,0
[0, ǫ] [0, ǫ] [0, ǫ]
λ
s3,≥1
γ
s2,≥1
γ
s1,≥1
γ
s0,≥1
λ
E λ γ E λ γ E λ γ
E γ
γ
γ
λ ǫ E λ γǫ E λ γǫ E λ γ
(b)
E [λ, λ + ǫ] [λ, λ + ǫ] [λ, λ + ǫ]
λ ǫ E λ γǫ E λ γǫ Eγ
Fig.3. (a) SPN, (b) uniformized underlying infinite CTMC, (c) finite abstraction
(c)
the marking of the SPN, where i tokens are at idle, m−i at busy and j at queue.
Aggregating {si,j | j ≥ n} by si,≥n for all i ∈ {0, ..., m} yields Fig. 3(c) (n = 1).
Consider ϕ = (〈l1 = 0〉 ∧ 〈l2 = 0〉) → P≤p(true U [0,t] (〈l1 = m〉 ∧ 〈l2 = 0〉))
where 〈l1 = i〉, 〈l2 = j〉 ∈ AP hold in all states si,j of the infinite CTMCs.
In Fig. 4, for λ ∈ {1, ..., 6}, lower and upper probability bounds for ϕ for
abstractions with n ∈ {1, ..., 9} are plotted. As expected, by increasing n, lower
and upper bounds are closer, i.e. the accuracy of the abstraction improves.
Fig.4. Probability bounds for ϕ.
6 Conclusion
Increasing m improves
the system performance.
The probability for which
ϕ holds decreases for increasing
m. If the system
is upgraded with m ′ additional
processors then the
requirement is not about
m jobs anymore, but about
m + m ′ . Note that CSL
model-checking algorithms
for quasi-birth-death processes
have also been considered
in [21]. Our abstraction
technique, though, is
not restricted to these (regular)
infinite CTMCs.
This paper presented a three-valued abstraction technique for CTMCs that is
conservative for true and false results of CSL. The idea is to abstract uniform
CTMCs and replace transition probabilities by intervals. A polynomial-time approximative
model-checking algorithm for 3-valued CSL has been provided.
Although our approach intends to combat the state-space explosion problem,
model checking of probabilistic interval models is of interest in its own, when
the exact values are not known and e.g., estimated by experiments, cf. [22].
Our experiments indicate that—like for most other abstraction techniques—
the partitioning of the state space determines the accuracy of the abstraction;
e.g., merging “slow” and “fast” states typically yields too coarse abstractions.
To conduct more experiments, we currently incorporate the abstraction into the
model checker MRMC [17]. Besides we plan to work on refinement techniques
to improve abstractions when the verification yields indefinite results.
References
1. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous time
Markov chains. ACM TOCL 1 (2000) 162–170
2. Baier, C., Hermanns, H., Katoen, J. P., Haverkort, B. R. H. M.: Efficient computation
of time-bounded reachability probabilities in uniform continuous-time Markov
decision processes. TCS 345 (2005) 2–26
3. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms
for continuous-time Markov chains. IEEE TSE 29 (2003) 524–541
4. Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time
semantics for Markov chains. Information and Computation 200 (2005) 149–214
5. Bause, F., Kritzinger, P. S.: Stochastic Petri nets: An introduction to the theory.
SIGMETRICS Performance Evaluation Review 26 (1998)
6. Ben Mamoun, M., Pekergin, N., Younès, S.: Model checking of continuous-time
Markov chains by closed-form bounding distributions. In: QEST. IEEE CS (2006)
189–198
7. Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R.,
Wimmer, R., Becker, B.: Compositional performability evaluation for Statemate.
In: QEST. IEEE CS (2006) 167–178
8. Ciardo, G., III, R. L. J., Miner, A., Siminiceanu, R.: Logical and stochastic modeling
with SMART. In: Comp. Perf. Ev. LNCS, Vol. 2794. (2003) 78–97
9. D’Aprile, D., Donatelli, S., Sproston, J.: CSL model checking for the GreatSPN
tool. In: Computer and Information Sc., ISCIS. LNCS, Vol. 3280. (2004) 543–553
10. D’Argenio, P. R., Jeannet, B., Jensen, H. E., Larsen, K. G.: Reachability analysis
of probabilistic systems by successive refinements. In: PAPM–PROBMIV. LNCS,
Vol. 2165., Berlin (2001) 39–56
11. Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Model
Checking Software. LNCS, Vol. 3925., Berlin (2006) 71–88
12. Gilmore, S., Hillston, J.: The PEPA workbench: A tool to support a process
algebra-based approach to performance modelling. In: Computer Performance
Evaluation. LNCS, Vol. 794. (1994) 353–368
13. Groesser, M., Baier, C.: Partial order reduction for Markov decision processes: a
survey. In de Boer, F. S., Bonsangue, M. M., Graf, S., de Roever, W.-P. (eds.):
FMCO. LNCS, Vol. 4111. (2006) 408–427
14. Huth, M.: An abstraction framework for mixed non-deterministic and probabilistic
systems. In: Validation of Stoch. Systems. LNCS, Vol. 2925. (2004) 419–444
15. Huth, M.: On finite-state approximants for probabilistic computation tree logic.
TCS 346 (2005) 113–134
16. Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D. N.: Bisimulation minimisation
mostly speeds up probabilistic model checking. In: TACAS. LNCS, Vol. 4424.
(2007) 87–102
17. Katoen, J.-P., Khattri, M., Zapreev, I. S.: A Markov reward model checker. In:
QEST. IEEE CS (2005) 243–244
18. Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov
decision processes. In: QEST. IEEE CS (2006) 157–166
19. Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic
model checking. In: CAV. LNCS, Vol. 4144., Berlin (2006) 234–248
20. Monniaux, D.: Abstract interpretation of programs as Markov decision processes.
Science of Computer Programming 58 (2005) 179–205
21. Remke, A., Haverkort, B. R., Cloth, L.: Model checking infinite-state Markov
chains. In: TACAS. LNCS, Vol. 3440. (2005) 237–252
22. Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence
of uncertainties. In: TACAS. LNCS, Vol. 3920., Berlin (2006) 394–410
23. Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking.
IEEE TSE 32 (2006) 531–546
24. Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D. N.: Flow faster: efficient
decision algorithms for probabilistic simulations. In: TACAS. LNCS, Vol. 4424.
(2007) 155–170
