Reachability Analysis of Probabilistic Real-Time Systems Based on
CEGAR for Timed Automata
Takeshi NAGAOKA† , Akihiko ITO† , Toshiaki TANAKA† , Kozo OKANO† , and Shinji KUSUMOTO††

Graduate School of Information Science and Technology, Osaka University
Yamadaoka 1–5, Suita City, Osaka, 565-0871, Japan

Abstract - Model checking techniques are considered aspromising techniques for verification of information systems
due to their ability of exhaustive checking. Well-known state
explosion, however, might occur in model checking of large
systems. Such explosion severely limits the scalability ofmodel checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on
CounterExample-Guided Abstraction Refinement (CEGAR)
technique proposed by E. Clarke et al..
This paper proposes a reachability analysis technique forprobabilistic timed automata. In the technique, we abstract
time attributes of probabilistic timed automata by applying
our abstraction refinement technique for timed automata proposed in our previous work. Then, we apply probabilistic
model checking to the generated abstract model which is justa markov decision process (MDP) with no time attributes.
This paper also provides some experimental results on applying our method to IEEE 1394, FireWire protocol. Experimental results show our algorithm can reduce the number ofstates and total execution time dramatically compared to one
of existing approaches.

Concrete
model

Initial Abstraction
Counter-example

property

true
property issatisfiedModel Checking

Simulation

refined model+property

false
property is
not satisfied

Refinement

Figure 1: A General CEGAR TechniqueConcrete
model

Initial Abstraction
Counter-example

property

true
property issatisfiedModel Checking

Simulation

refined model+property
refined Concrete model+property
Model Transformation

false
property is
not satisfied

Refinement

Compatibility
Checking

Keywords: Probabilistic Timed Automaton, CEGAR,
Model Checking, Real-time System, Formal Verification

Figure 2: Our CEGAR Technique for Reachability Analysis
of a Probabilistic Timed Automaton

1 Introduction

last step is repeated until the valid output is obtained. In the
CEGAR loop, an abstract model must satisfy the following
property: if the abstract model satisfies a given specification,
the concrete model also satisfies it.
In Paper[6], we have proposed an abstraction algorithm
for timed automata based on CEGAR. In this algorithm, we
generate finite transition systems as abstract models where
all time attributes are removed. The refinement modifies thetransition relations of the abstract model so that the model
behaves correctly even if we don’t consider the clock constraints.
This paper proposes a reachability analysis technique forprobabilistic timed automata. In the technique, we abstract
time attributes of probabilistic timed automata by applying
our abstraction technique for timed automata proposed in Paper[6]. Then, we apply probabilistic model checking to thegenerated abstract model which is just a markov decision process (MDP) with no time attributes. The probabilistic model
checking algorithm calculates summation of occurrence probability of all paths which reach to a target state for reachability analysis. For probabilistic timed automata, however,
we have to consider required clock constraints for such paths,
and choose the paths whose required constraints are compatible. Since our abstract model does not consider the clock

Model checking[1] techniques are considered as promisingtechniques for verification of information systems due to theirability of exhaustive checking. For verification of real-timesystems such as embedded systems, timed automata are often
used. On the other hand, probabilistic model checking[2]–[4]can evaluate performance, dependability and stability of information processing systems with random behaviors. In recent years, probabilistic models with real-time behaviors, called probabilistic timed automata (PTA) attract attentions. As
well as traditional model checking techniques, however, state
explosion is thought to be a major hurdle for verification ofprobabilistic timed automata.
Clarke et al. proposed an abstraction technique called CEGAR (CounterExample-Guided Abstraction Refinement)[5]shown in Fig.1. In the CEGAR technique, we use a counterexample (CE) produced by a model checker as a guide to refine abstracted models. A general CEGAR technique consistsof several steps. First, it abstracts the original model (the obtained model is called abstract model) and performs model
checking on the abstract model. Next, if a CE is found, it
checks whether the CE is feasible on the concrete model ornot. If the CE is spurious, it refines the abstract model. The

constraints, we add a new flow where we check whether allpaths used for probability calculation are compatible. Also, if
they are not compatible, we transform the model so that we do
not accept such incompatible paths simultaneously. The proposed procedure for the probabilistic timed automata is shownin Fig.2.
This paper also provides some experimental results on applying our method to some examples. Experimental results
show our algorithm can reduce the number of states and total execution time dramatically compared to one of existing
approaches.
Several papers including Paper[3] have proposed probabilistic model checking algorithms. These algorithms, however, don’t provide CEs when properties are not satisfied. Our
proposed method provides a CE as a set of paths based on
k-shortest paths search. This is a major contribution of our
method. The proposed method also performs model checking
considering compatibility problem. Few approaches resolve
the compatibility problem. Our approach also shows the efficiency via performing experiments.
The organization of the rest paper is as follows. Sec.2 provides some definitions and lemmas as preliminaries. Sec.3 describes our proposed abstraction technique for the probabilistic timed automaton. Sec.4 gives some experimental results.
Finally, Sec.5 concludes the paper and gives future works.

1
1.0
0.8

0.2

2

3

1.0

4
1.0
0.2

1.0

0.5 0.3

5

6

7
0.5

0.5 0.5

8
0.5

9

1.0

10

Figure 3: An Example of an MDP
a)

b)

1

1

0.2

c)
1.0

1

1.0

0.8

2

3

1.0
0.5 0.3

5

6

7
0.5

0.5 0.5

4

9

4

1.0

0.2

1.0

7
0.5

10

0.5

9

8
0.5

10

1.0

10

Figure 4: Examples of Adversaries(For a zone D, ν ∈ D means the assignment ν satisfies all theinequalities in D).

2.2 Probability Distribution

This section gives some definitions about models used inthis paper and also describes a general CEGAR technique.

A discrete probability distribution on a finite set Q is given
as the function µ : Q → [0, 1] such that Σq∈Q µ(q) = 1. Also,
support(µ) is a subset of Q such that ∀q ∈ support(µ).µ(q) >0 holds.

2.1 Clock and Zone

2.3 Markov Decision Process

Let C be a finite set of clock variables which take nonnegative real values (R≥0 ). A map ν : C → R≥0 is called aclock assignment. The set of all clock assignments is denotedC
by RC≥0 . For any ν ∈ R≥0 and d ∈ R≥0 we use (ν + d) todenote the clock assignment defined as (ν +d)(x) = ν(x)+dfor all x ∈ C. Also, we use r(ν) to denote the clock assignment obtained from ν by resetting all of the clocks in r ⊆ C
to zero.

A Markov Decision Process (MDP)[7] is a markov chain
with non-deterministic choices.

2 Preliminary

Definition 2.1 (Differential Inequalities on C). Syntax andsemantics of a differential inequality E on a finite set C ofclocks is given as follows:
E ::= x − y ∼ a | x ∼ a,where x, y ∈ C, a is a literal of a real number constant, and∼∈ {≤, ≥, <, >}. Semantics of a differential inequality is
the same as the ordinal inequality.
Definition 2.2 (Clock Constraints on C). Clock constraintsc(C) on a finite set C of clocks is defined as follows:
A differential inequality in on C is an element of c(C).
Let in1 and in2 be elements of c(C), in1 ∧ in2 is also anelement of c(C).
A zone D ∈ c(C) is described as a product of finite differential inequalities on clock set C, which represents a set ofclock assignments that satisfy all the inequalities. In this paper, we treat a zone D as a set of clock assignments ν ∈ RC
≥0

Definition 2.3 (Markov Decision Process). A markov decision process M DP is 3-tuple (S, s0 , Steps), where
S : a finite set of states;s0 ∈ S : an initial state; andSteps ⊆ S × A × Dist(S): a probabilistic transition relation
where Dist(S) is a probability distribution over S.
In our reachability analysis procedure, we transform a given
PTA into a finite MDP, and perform probabilistic verification
based on the Value Iteration[8] technique.
Figure 3 shows an example of an MDP. In the figure, probability distributions are associated with transitions. In the figure, transitions which belong to the same distribution are connected with a small arc at their source points. The MDP has
several non-deterministic choices at the state 1 and 4. For
example, at the state 1, we have two choices; 1) the control
moves to the state 2 with the probability 0.2 and to the state
3 with the probability 0.8, 2) the control moves to the state 4
with the probability 1.0.
2.3.1 Adversary
An MDP has non-deterministic transitions called action. To
resolve the non-determinism, an adversary is used. The adver-sary requires a finite path on an MDP, and decides a transition
to be chosen at the next step.
Figure 4 shows examples of resolving the non-determinismof the MDP shown in Fig.3 by some adversaries. Figure 4. a)is the case where we choose the action which moves to thestate 2 or state 3 at the initial state 1. On the other hand, b)
and c) are the cases where we choose the action which moves
to the state 4 at the initial state 1. In the case of b), we choose
the action which moves to the state 7 when we move from thestate 1 to state 4. Also, in the case of c), we choose the action
which moves to the state 8 in the same trace.
Here, if we want to obtain the reachability probability fromthe state 1 to the state 10, under the adversary of a), we canobtain the probability 0.08 (= 0.8 × 0.2 × 0.5), which is theminimum reachability probability. On the other hand, under
the adversary of c), we can obtain the probability 1.0 (= 1.0×
1.0 × 1.0), which is the maximum reachability probability.
2.3.2 Value Iteration
A representative technique of model checking for an MDP isValue Iteration[8]. The Value Iteration technique can obtain
both of maximum and minimum probabilities of reachability
and safety properties, respectively. At each state, Value Iteration can select an appropriate action according to the property
to be checked. Therefore, the technique can produce the adversary as well as the probability.

2.4 Timed Automaton
Definition 2.4 (Timed Automaton). A timed automaton A isa 6-tuple (A, L, l0 , C, I, T ), where
A: a finite set of actions;
L: a finite set of locations;l0 ∈ L: an initial location;
C: a finite set of clocks;
I ⊂ (L → c(C)): a mapping from locations to clock constraints, called a location invariant; andT ⊂ L × A × c(C) × R × L,
where c(C) is a clock constraint, called guards;
R = 2C : a set of clocks to reset.
a,g,r

A transition t = (l1 , a, g, r, l2 ) ∈ T is denoted by l1 −→l2 . A map ν : C → R≥0 is called a clock assignment. We
define (ν + d)(x) = ν(x) + d for d ∈ R≥0 . r(ν) = ν[x 7→0], x ∈ r, where ν[x 7→ 0] means the valuation that maps x
into zero, is also defined for r ∈ 2C .
Definition 2.5 (Semantics of a Timed Automaton). Given a
timed automaton A = (A, L, l0 , C, I, T ), let S ⊆ L × RC≥0
be a set of whole states of A . The initial state of A shall begiven as (l0 , 0C ) ∈ S.
a,g,r
For a transition l1 −→ l2 (∈ T ), the following two transitions are semantically defined. The former one is called an
action transition, while the latter one is called a delay transition.
a,g,r

l1 −→ l2 , g(ν), I(l2 )(r(ν))
a(l1 , ν) ⇒ (l2 , r(ν)),∀d′ ≤ d I(l1 )(ν + d′ )d(l1 , ν) ⇒ (l1 , ν + d)

b
a

1

0.5

0.5
x:=0

x<1

d
c

1

x==0∧y>=1

Figure 5: An Example of a PTA
Definition 2.6 (A Semantic Model of a Timed Automaton).
For timed automaton A = (A, L, l0 , C, I, T ), an infinite transition system is defined according to the semantics of A ,where the model begins with the initial state.

2.5 Probabilistic Timed Automaton
A PTA is a kind of a timed automaton extended with probabilistic behavior. In the PTA, a set of probabilistic distributions is used instead of a set T of discrete transitions on thetimed automaton.
Definition 2.7 (Probabilistic Timed Automaton). A probabilistic timed automaton P T A is a 6-tuple (A, L, l0 , C,I, prov), where
A: a finite set of actions;
L: a finite set of locations;l0 ∈ L: an initial location;
C: a finite set of clocks;
I ⊂ (L → c(C)): a location invariant; andprob ⊆ L × A × c(C) × Dist(2C × L): a finite set of probabilistic transition relations, where c(C) represents a guard
condition, and Dist(2C × L) represents a finite set of probability distributions p. The Distribution p(r, l) ∈ Dist(2C ×L)
represents the probability of resetting clock variables in r andalso moving to the location l;
Figure 5 shows an example of a PTA. In the figure, fromthe location a, it moves to the location b with the probability
0.5 and also moves to the location c letting the value of theclock x reset to zero with the probability 0.5. Both of thearcs starting location a are connected with a small arc at theirsource points, which represents that they belong to the sameprobability distribution.
Definition 2.8 (Transitions of a Probabilistic Timed Automaton). For P T A = (A, L, l0 , C, I, prov), 6-tuple (l, a, g, p, r, l′ )represents a transition generated by a probabilistic distribution (l, a, g, p) ∈ prob such that p(r, l′ ) > 0.
Definition 2.9 (Semantics of a Probabilistic Timed Automaton). Semantics of a probabilistic timed automaton P T A =(A, L, l0 , C, I, prob) is given as a timed probabilistic system
T P SP T A = (S, s0 , T Steps) where,• S ⊆ L × RC ;• s0 = (l0 , 0C ); and• T Steps ⊆ S × A ∪ R≥0 × Dist(S) is composed ofaction transitions and delay transitions.
a) action transition
if a ∈ A and there exists (l, a, g, p) ∈ prob suchthat g(ν) and I(l′ )(r(ν)) for all (r, l′ ) ∈ support(p),((l, ν), a, µ) ∈ T Steps where for all (l′ , ν ′ ) ∈ S∑µ(l′ , ν ′ ) =p(r, l′ ).
r⊆C∧ν ′ =r(ν)b) delay transition
if d ∈ R≥0 , and for all d′ ≤ d, I(l)(ν + d′ ),((l, ν), d, µ) ∈ T Steps where µ(l, ν + d) = 1.
In this paper, using a location l and a zone D, we describe
a set of semantic states as (l, D) = {(l, ν) | ν ∈ D}.
A probabilistic timed automaton is said to be well-formed
if a probabilistic edge can be taken whenever it is enabled[2].
Formally, a probabilistic timed automaton P T A = (A, L, l0 ,C, I, prob) is well-formed if∀(l, g, p) ∈ prob. ∀ν ∈ RC
≥0 . (g(ν))→ ∀(r, l) ∈ support(p). I(l)(r(ν)).
In this paper, we assume that a given PTA is well-formed.
Definition 2.10 (Path on a Timed Probabilistic System). A
path ω with length of n on a timed probabilistic system
T P SP T A = (S, s0 , T Steps) is denoted as follows.
d0 ,µ0d1 ,µ1

ω = (l0 , ν0 ) −→ (l1 , ν1 ) −→ . . .

dn−1 ,µn−1−→(ln , νn ), where (l0 , ν0 ) = s0 , (li , νi ) ∈ S for 0 ≤ i ≤ n and((li , νi ), di , µ) ∈ T Steps ∧ ((li , νi + di ), 0, µi ) ∈ T Steps ∧(li+1 , νi+1 ) ∈ support(µi ) for 0 ≤ i ≤ n − 1.
For model checking of a probabilistic timed automaton, we
extract a number of paths and calculate a summation of theiroccurrence probabilities in order to check the probability ofsatisfying a given property. The important point is that wehave to choose a set of paths which are compatible with respect to time elapsing.
Lemma 2.1 (Compatibility of two paths). If two paths ω α =dα ,µαdα ,µα1100...
(l0α , ν0α ) −→(l1α , ν1α ) −→dβ ,µβdβ ,µβαdαn−1 ,µn−1−→(lnα , νnα ) andβdβm−1 ,µm−1

0
0
1
1
β
β
ω β = (l0β , ν0β ) −→(l1β , ν1β ) −→
...
−→
(lm
, νm
)
on a timed probabilistic system T P SP T A satisfy the following predicate isCompatible, then ω α and ω β are said to becompatible.
isCompatible(ω α , ω β ) =

β
β
α
α


true, if ∀i < min(n, m). li = li ∧ di = dior there exists i < min(n, m) such thatβliα ̸= liβ ∧ dα
i = di ∧β∀j < i. ljα = ljβ ∧ dαj = djfalse, otherwise.

Above predicate isCompatible stands for that two paths
are compatible if and only if one path is a prefix of the other,or same amount of delay is executed in both paths at thebranching point of them.
Lemma 2.2 (Compatibility of a set of paths). If a set Ω ofpaths on a timed probabilistic system T P SP T A satisfies thefollowing predicate isCompatible, then all of the paths over
Ω are said to be compatible.
isCompatible(Ω) =∧β
true, if ∀i ≤ min(Ω)(liα = liβ ∧ dα
i = di )ω α ,ω β ∈Ω∧ω α ̸=ω β




or
there
existsi≤ min(Ω) such that


∧
∧

β
β

α
α
(li ̸= li ∧ di = dβi ∧ (ljα= ljβ ∧ dα
j = dj )),j≤iω α ,ω β ∈Ω∧ω α ̸=ω β

∧



isCompatible(Ω′ )and alsoΩ′ ∈2Ω ∧Ω′ ̸=Ω∧|Ω′ |≤2false, otherwise.
In Lemma2.2, we give the predicate isCompatible for aset Ω of paths on a timed probabilistic system. In the lemma,
we let paths in Ω be compatible if there is no contradiction
with respect to time elapsing at the branching point of all thepaths in Ω, and also if the compatibility is kept for every subset of Ω which contains more than two paths.
Next, we give a simple example of a pair of paths which
does not satisfy the compatibility. In the Fig.5, paths from the0,0.5
location a to d are given as ω α = (a, x = 0 ∧ y = 0) −→0,1.0(b, x = 0 ∧ y = 0) −→ (d, x = 0 ∧ y = 0) which reaches
1,0.5

to d through b, and ω β = (a, x = 0 ∧ y = 0) −→ (c, x =0,1.0

0 ∧ y = 1) −→ (d, x = 0 ∧ y = 1) which reaches to dthrough c. In the path ω α , we are required to let delay at thelocation a be less than one unit of time because of the guarded
condition x < 1 of the transition between b and d. On theother hand, in the path ω β , we are required to let delay at a be
grater than or equal one unit of time because of the condition
x == 0 ∧ y ≥ 1 of the transition between c and d. Like thepath ω α and ω β , if the required conditions of time elapsing at
the branching point are contradict, we cannot use such paths
simultaneously in the probability calculation.

2.6 CounterExample-Guided Abstraction
Refinement
2.6.1 General CEGAR TechniqueSince model abstraction sometimes over-approximates an original model, we may obtain spurious CEs which are infeasibleon the original model. Paper [5] gives an abstraction refinement framework called CEGAR (CounterExample-Guided Abstraction Refinement) (Fig.1).
In the algorithm, at the first step (called Initial Abstraction), it generates an initial abstract model. Next, it performs
model checking on the abstract model. In this step, if themodel checker reports that the model satisfies a given specification, we can conclude that the original model also satisfies the specification, because the abstract model is an overapproximation of the original model. If the model checker
reports that the model does not satisfy the specification, however, we have to check whether the CE detected is spurious
or not in the next step (called Simulation). In the Simulation
step, if we find that the CE is valid, we stop the loop. Otherwise, we have to refine the abstract model to eliminate thebspurious CE, and repeat these steps until valid output is obtained.

1
0.5

a

d

0.5
x:=0

c

2.6.2 CEGAR Technique for a Timed Automaton
In Paper[6], we have proposed the abstraction refinement technique for a timed automaton based on the framework of CEGAR. In this approach, we remove all the clock attributes
from a timed automaton. If a spurious CE is detected bymodel checking on an abstract model, we transform the transition relation on the abstract model so that the model behavescorrectly even if we don’t consider the clock constraints. Suchtransformation obviously represents the difference of behavior caused by the clock attributes. Therefore, the finite number of application of the refinement algorithm enables us tocheck the given property without the clock attributes. Since
our approach does not restore the clock attributes at the refinement step, the abstract model is always a finite transition
system without the clock attributes.

3 Proposed Approach
In this section, we will present our abstraction refinement
technique for a probabilistic timed automaton. In the technique, we use the abstraction refinement technique for a timed
automaton proposed in Paper[6]. In addition, we resolve thecompatibility problem shown in Sec.2.5 by performing a backward simulation technique and generating additional location
to distinguish the required condition for every incompatible
path. Figure 2 shows our abstraction refinement framework.
As shown in the figure, we add another flow where we resolve
the compatibility problem.
Our abstraction requires a probabilistic timed automaton
P T A and a property to be checked as its inputs. The property
is limited by the PCTL formula P<p [true U err]. The formula represents a property that the probability of reaching tostates where err (which means an error condition in general)is satisfied, is less than p.

1

Figure 6: An Initial Abstract Model

3.2 Model Checking
In model checking, we apply Value Iteration[8] into themarkov decision process obtained by abstraction and calculate a maximum reachability probability. Also, it decides anaction to be chosen at every state as an adversary. If the obtained probability is less than p, we can terminate the CEGAR
loop and conclude that the property is satisfied.
Although Value Iteration can calculate a maximum reachability probability, it cannot produce concrete paths used forthe probability calculation. To obtain the concrete paths, weuse an approach proposed in Paper[9] which can produce CE
paths for PCTL formulas. The approach translates a probabilistic automaton into a weighted digraph. And we can obtain at most k paths by performing k-shortest paths search on
the graph.
Definition 3.2 (Path on the Abstract Model). A path ω̂ on
ˆ P T A = (Ŝ, ŝ0 , Steps)ˆan abstract model M DP
for P T A =(A, L, l0 , C, I, prob) is given as follows,
a0 ,p0 ,r0

a1 ,p1 ,r1ω̂ = ŝ0 −→ ŝ1 −→ . . .

an−1 ,pn−1 ,rn−1

−→

ŝn

ˆ ∧
, where ŝi ∈ Ŝ for 0 ≤ i ≤ n and (ŝi , ai , pi ) ∈ Steps(ri , ŝi+1 ) ∈ support(pi ) for 0 ≤ i ≤ n − 1.
As defined in Def. 3.2, we associate a set r of clock resetwith a path on an abstract model in order to show the difference of r over the probabilistic distribution p.
For the abstract model shown in Fig.6, Value Iteration outputs 1.0 as the probability that it reaches to the location d fromthe location a. On the other hand, k-shortest paths search
τ,0.5,{}

τ,1.0,{}

3.1 Initial Abstraction(k ≥ 2) detects two paths ω̂ α = a

The initial abstraction removes all the clock attributes froma given probabilistic timed automaton as well as the techniquein Paper[6]. The generated abstract model over-approximatesthe original probabilistic timed automaton. Also, the abstract
model is just an MDP without time attributes.

ω̂ = a−→c −→ d, where τ represents a label fortransitions with no label in the figure.

Definition 3.1 (Abstract Model). For a given probabilistic
timed automaton P T A = (A, L, l0 , C, I, prob), a markov deˆ P T A = (Ŝ, ŝ0 , Steps)
ˆcision process M DP
is produced as its
abstract model, where• Ŝ = L• ŝ0 = l0
ˆ = { (s, a, p) | (s, a, g, p) ∈ prob }• Steps
Figure 6 shows an initial abstract model for the PTA shownin Fig.5 As shown in the figure, the abstract model is just an
MDP where all of the clock constraints are removed though
we keep a set of clock reset as a label of transitions.

βτ,0.5,{x:=0}

−→

b

−→

d and

τ,1.0,{}

3.3 Simulation
Simulation checks whether all the paths obtained by kshortest paths search are feasible or not on the original probabilistic timed automaton. We use the simulation algorithm
proposed in Paper[6] where we use some operations of DBM(Difference Bound Matrix)[10] to obtain zones which are reachable from the initial state. If there is at least one path which isinfeasible on the original PTA, we proceed to the abstraction
refinement step.
Figure 7 shows the simulation results for two paths ω̂ α andβω̂ . Simulation concludes that the two paths are feasible on
the original PTA.

3.4 Abstraction Refinement
In this step, we refine the abstract model so that the given
spurious CE also becomes infeasible on the refined abstract

Algorithm 1 BackwardSimulation(P T A, ω)
1: /* P T A = (A, L, l0 , C, I, prob)
a ,p ,ra ,p ,ran−1 ,pn−1 ,rn−1ω̂ = ŝ0 0 →0 0 ŝ1 1 →1 1 . . .
→ŝn */
ω̂:= I(ŝn )2: Db,n3: for i := n − 1 downto 0 do
ω̂
ω̂
4:
Db,i
:= Db,i+1ω̂ω̂5:
Db,i := down(Db,i)/* reverse the time elapse */ω̂ω̂Db,i := and(Db,i , I(ŝi+1 ))
6:
ω̂
ω̂
7:
Db,i
:= f ree(Db,i, ri )/* remove all constraints on ri */ω̂ω̂Db,i := and(Db,i , gi )/* (ŝi , ai , gi , pi ) ∈ prob */
8:
ω̂
ω̂
9:
Db,i
:= and(Db,i, I(ŝi ))10: end for
11: return Dbω̂
A path on the abstract model
a 0.5
b 1.0
d
A corresponding path on the PTA
a 0.5
b 1.0
d
x<1
Reachable zones from the initial state
a
b
d
0.5
1.0
x==y
x==y
x==y & x<1

A path on the abstract model
a 0.5
c 1.0
d
x:=0
A corresponding path on the PTA
1.0
a 0.5
c
d
x:=0
x==0 &
y>=1
Reachable zones from the initial state
a 0.5
c
d
1.0
x==y
y>=x
y-x>=1Figure 7: Simulation Results for a Set of Paths
A path on the abstract model
a 0.5
b 1.0
d
A corresponding path on the PTA
a 0.5
b 1.0
d
x<1
Zones which are reachable to d
a 0.5
b
d
1.0
x<1
x<1
true

A path on the abstract model
a 0.5
c 1.0
d
x:=0
A corresponding path on the PTA
0.5
1.0
a
c
d
x:=0
x==0 &
y>=1
Zones which are reachable to d
a
c
0.5
1.0 d
y>=1
x==0 &
true
y>=1

Figure 8: Results of Backward Simulation for a Set of Paths
model. We can use the algorithm proposed in Paper[6]. Since
the algorithm of Paper[6] performs some operations on transitions of a timed automaton, we replace such operations by
those on probability distributions of a probabilistic timed automaton.

3.5 Compatibility Checking
When all the paths obtained by k-shortest paths search arefeasible and a summation of occurrence probabilities of themis greater than p, we also have to check whether all the paths
are compatible or not. In this compatibility checking step,at each location of the paths, we have to obtain a condition(zone) which is reachable from the initial state and also reachable to the last state along with the path. Next, we check thecompatibility of such conditions among all paths. To obtainsuch conditions, we have to perform both forward simulation
shown in Sec. 3.3 and backward simulation for each path,and merge the results. For the result of forward simulation,
we can reuse the result obtained in the Simulation step. Then
we check the compatibility based on Lemma 2.2.
3.5.1 Backward Simulation
Algorithm 1 implements the backward simulation. Functions and, f ree, down used in the algorithm are operation
functions on a zone, and are defined in Paper[10]. Formally,

Algorithm 2 IsCompatible(P T A, Ω̂, Df , Db )1: /* P T A = (A, L, l0 , C, I, prob), Ω̂ is a set of abstract paths,

and Df and Db are sets of forward and backward simulation
results for each path ω̂ ∈ Ω̂,respectively. */2: return CompatibleCheck(P T A, Ω̂, Df , Db , 0)

Algorithm 3 CompatibleCheck(P T A, Ω̂, Df , Db , i)
1: D ′ := true
2: foreach ω̂ ∈ Ω̂ such that length(ω̂) ≥ i do
ω̂
ω̂
ω̂
3:
Dc,i
:= Df,i∩ Db,iω̂
4:D′ := D′ ∩ Dc,i5:
if D′ = ∅ thenreturn f alse6:
end if7:
8: end for
9: SiΩ̂+1 := SplitP athSet(Ω̂, i + 1)

10: /* split Ω̂ into a set of its subsets without overlap with respect tothe i+1-th location and clock reset for each path in Ω̂ */′11: foreach Ω̂′ ∈ SiΩ̂
+1 such that |Ω̂ | ≥ 2 do

12:
if CompatibleCheck(P T A, Ω̂′ , D, i+1)=f alse then13:
return f alseend if14:
15: end for
16: return true

for a zone D, a constraint c, and a set r of clock reset, thosefunctions are defined as follows; and(D, c) = {u | u ∈D ∧ u ∈ c}, f ree(D, r) = {u | r(u) ∈ D}, and down(D) ={u | u + d ∈ D ∧ d ∈ R≥0 }Figure 8 shows results of backward simulation for two pathsω̂ α and ω̂ β detected in Sec. 3.2.
3.5.2 Determination of Compatibility
In this step, we check compatibility of the set Ω̂ of pathson the abstract model using the required conditions obtainedby both of forward and backward simulation. Algorithm 2
checks the compatibility of Ω̂ using the Algorithm 3.
Algorithm 3 first checks whether the required conditions of
the i-th locations for each path are compatible or not (l2-l8)
using the results of forward and backward simulation. Next,
the algorithm divides Ω̂ into some subsets of it based on the(i+1)-th locations and the set of clock reset for each path (l9).
Then, it checks the compatibility for the following sequencesof paths by applying the algorithm into the divided subsets
recursively (l11-l15). Although the predicate isCompatible
Algorithm 4 SplitPathSet(Ω̂, i)
1: S := ∅2: foreach ω̂ ∈ Ω̂ doan−1 ,pn−1 ,rn−1
a ,p ,ra ,p ,r3:/* ω̂ = ŝ0 0 →0 0 ŝ1 1 →1 1 . . .
→ŝn */
if Ω̂ri−1 ,ŝi ̸∈ S then4:5:Ω̂ri−1 ,ŝi := {ω̂}

6:
S := S ∪ Ω̂ri−1 ,ŝi
7:
else
8:
Ω̂ri−1 ,ŝi := Ω̂ri−1 ,ŝi ∪ {ω̂}9:end if
10: end for
11: return S

Algorithm 5 TransformPTA(P T A, Dc , Ω̂, i)

Algorithm 7 DuplicateDistribution(P T A, ω̂, Ldup , i)

1: Dcomplement := true
2: foreach ω̂ ∈ Ω̂ doω̂3:
Ldup := DuplicateLocation(P T A, ω̂, Dc,i
, i)
4:
L := L ∪ Ldup
5:
probdup := DuplicateDistribution(P T A, ω̂, Ldup , i)6:prob := prob ∪ probdup
ω7:
Dcomplement := Dcomplement ∩ Dc,i
8: end for
9: Ldup := DuplicateLocation(P T A, ω̂, Dcomplement , i)
10: L := L ∪ Ldup
11: probdup := DuplicateDistribution(P T A, ω̂, Ldup , i)12: prob := prob ∪ probdup
13: prob := RemoveDistribution(P T A, ŝi , pi )14: /* for all path ω̂ ∈ Ω̂, the i-th state ŝi and i-th probability distri-

1: /* P T A = (A, L, l0 , C, I, prob)

bution is pi */15: return P T A

a ,p ,ra ,p ,ran−1 ,pn−1 ,rn−1ω̂ = ŝ0 0 →0 0 ŝ1 1 →1 1 . . .
→ŝn */
2: probdup := ∅3: pdup := newDistribution()
4:/* generate a new distribution over L × 2C */5: foreach (l, r) ∈ L × 2C do
6:pdup (ldup , r) := pi (l, r)
7:/* ldup is a duplicate location of l generated by DuplicateLocation algorithm */8: end for
9: probdup := P robdup ∪ {(ŝi , ai , g, pdup )}10:/* (ŝi , ai , g, pi ) ∈ prob */11: foreach ldup ∈ Ldup do
12:
probdup := P robdup ∪13:
DuplicateDistF romDupLoc(P T A, ldup )14: end for
15: return pdup

Algorithm 6 DuplicateLocation(P T A, ω̂, D, i)
1: /* P T A = (A, L, l0 , C, I, prob)
a ,p ,ra ,p ,ran−1 ,pn−1 ,rn−1→ŝn */
ω̂ = ŝ0 0 →0 0 ŝ1 1 →1 1 . . .
2: Ldup := ∅3: foreach (l, r) ∈ L × 2C such that pi (l, r) > 0 do
4:(l, D) := Succ((ŝi , D), e)5:/* succ returns a successor state set through a given edge e,
and e = (ŝi , ai , g, pi , r, l) */6:
ldup := newLocation()7:
I(ldup ) := D
8:
Ldup = ldup
9: end for
10: return Ldup

in the Lemma 2.2 checks the compatibility for each subset ofΩ, the algorithm omit redundant checks by dividing Ω basedon the branches of the paths.
For the path ω̂ α in Sec. 3.2, zones at a which is reachableω̂ αfrom initial state and which can move to d are given as Df,0=ω̂ α(x == y), and Db,0 = (x < 1), respectively. Also, a zoneω̂ α
= (x == y ∧ x <of the product of them is given as Dc,01). Similarly, for the path ω̂ β , the product zone is given as
ω̂ β
ω̂ β
ω̂ α
= (x == y ∧ y > 1). Since Dc,0and Dc,0
contradictDc,0each other, we can conclude that the paths ω̂ α and ω̂ β are
incompatible each other.

3.6 Model Transformation
When the compatibility check procedure decides a given
set Ω̂ of paths is incompatible at i-th location, our proposed
algorithm resolves the incompatibility by refining behaviors
from the i-th location. Our algorithm uses Dcω̂ which is a
product of results of forward and backward simulation for apath ω̂ ∈ Ω̂. It duplicates locations which are reachable fromω̂
the zone Dc,iby an action associated with the i-th distribution
pi . Also it constructs transition relations so that the transformation becomes equivalent transformation. For example,
transition relations from a duplicated location are duplicated
if the relations are executable from the invariant associatedwith the duplicated location.
Algorithm 5 transforms a given PTA with considering its

Algorithm 8 DuplicateDistFromDupLoc(P T A, ldup )1: /* P T A = (A, L, l0 , C, I, prob), and let l be an original loca-

tion of ldup */2: probdup := ∅3: foreach (l, a, g, p) ∈ P rob do
4:fdup := true, pdup := newDistribution()5:
foreach (l′ , r) ∈ L × 2C do
6:
if Succ((l, I(ldup )), e) ̸= ∅ then7:/* e = (l, a, g, p, r, l′ ) */′8:
pdup (l , r) = p(l, r)
9:
else
10:
fdup := false
11:
break
12:
end if13:
end for14:
if fdup then15:/* duplicate the distribution if it is executable from the du-plicate location */16:
P robdup := P robdup ∪ {(l, a, g, pdup )}17:
end if
18: end forcompatibility. The algorithm calls DuplicateLocation (Algorithm 6) which duplicates locations, DuplicateDistribution(Algorithm 7) which duplicates probabilistic transitions, andRemoveDistribution (Algorithm 9) which removes probabilistic transitions. The procedure Succ in Algorithms 6 and
8 calculates a successor state set from a given state set S
through a given edge e = (l, a, g, p, r, l′ ), i.e. Succ(S, e) ={(l′ , r(ν) + d) | (l, ν) ∈ S ∧ g(ν) ∧ I(l′ )(r(ν)) ∧ ∀d′ ≤d.I(l′ )(r(ν) + d′ )}Figure 9 shows the transformed PTA by applying the modeltransformation procedure for the paths ω̂ α and ω̂ β . The locaAlgorithm 9 RemoveDistribution(P T A, l, p)
1: /* P T A = (A, L, l0 , C, I, prob), and let l be an original loca-

tion of ldup */2: foreach (l, a, g, p) do
3:
prob := prob \ {(l, a, g, p)}
4: end for5: return prob

Table 1: Experimental Result
D(µs)
5
10
20

p
1.09×10−1
3.28×10−1
1.26×10−2
3.79×10−2
1.85×10−4
5.56×10−4

Digital Clocks[3]T ime(s)State M EM (M B)
20.90
297,232
10.2
20.89
297,23210.2
54.80
685,232
21.7
54.82
685,23221.7
176.93 1,461,232
41.0
177.46 1,461,232
41.0

Result
false
true
false
true
false
true

b1 1

0.5

a

x==y

0.5 x:=0x<1c1x>=1&x==y4.1 Goals of the Experiments
x==0∧y>=1

c2 1
y-x>=1

0.5
0.5
x:=0

Heap(M B)
8.0
8.0
8.0
8.0
64.0
8.0

reduce the number of CEGAR loop.

b2

0.5
x:=0

Proposed Approach
T ime(s) Loop State
4.19
10
37
3.60
9
36
8.16
19
134
6.57
15
115
1186.08
47
477
31.32
32
435

d

0<=y-x < 1

0.5

Result
false
true
false
true
false
true

b3
￢(x==y)&￢(x>=1&x==y)c3￢(0<=y-x<1)&￢(y-x>=1)

Figure 9: A Transformed PTA
tions b1 and c1 are duplicated locations based on the path ω̂ αω̂ β= (x == y ∧ x < 1) on the location a.
and the zone Dc,0
We associate invariants to b1 and c1 based on zones which areω̂ βthrough transitions from a to b, and fromreachable from Dc,0
a to c, respectively. Also, we duplicate a transition from b tod as the transition from b1 to d because the transition is feasible from the invariant of b1 . On the other hand, we do not
duplicate a transition from c to d because the transition is not
feasible from the invariant of c1 . Similarly, locations b2 andc2 are duplicated locations based on the path ω̂ β and the zone
ω̂ β
Dc,0
. Locations b3 and c3 are generated as complements of
the invariant associated with each duplicated location in orderto preserve the equivalence.
By transforming the original PTA in such a way, if we remove all clock constraints from the model in Fig.9, Value
Iteration on its abstract model outputs 0.5 as the maximum
probability.

4 Experiments
We have implemented a prototype of our proposed approachwith Java, and performed some experiments. Though the prototype can check the compatibility of a given set of paths,
currently it cannot deal with the model transformation.
The prototype performs k-shortest paths search and simulation concurrently in order to reduce execution time. By implementing the algorithms concurrently, we have not to wait
until all of k paths are detected, i.e. if a path is detected by the
k-shortest paths search algorithm, we can immediately apply
simulation and (if needed) abstraction refinement procedures.
Also, our prototype continues the k-shortest search algorithm when a spurious CE is detected and the refinement algorithm is applied. If other paths which do not overlap withthe previous spurious CEs, are detected, we can apply simulation and refinement algorithms to it again. This helps us

In this experiment, we evaluated the performance of our
proposed approach with regard to execution time, memory
consumption, and qualities of obtained results. As a target
for comparison, we chose the approach of Digital Clocks[3]where they approximate clock evaluations of a PTA by integer
values.

4.2 Example
We used a case study of the FireWire Root Contention Protocol[11] as an example for this experiment. This case study
concerns the Tree Identify Protocol of the IEEE 1394 High
Performance Serial Bus (called “FireWire”) which takes placewhen a node is added or removed from the network. In theexperiment, we checked the probability that a leader is notselected within a given deadline. The probabilistic timed automaton for the example is composed of two clock variables,
11 locations, and 24 transitions.

4.3 Procedure of the Experiments
In this experiment, we checked the property that “the probability that a leader cannot be elected within a given deadline
is less than p.” We considered three scenarios where the parameter deadline is 5, 10, 20 µs, respectively. Also, for eachscenario, we conducted two experiments where the value of p
is 1.5 times as an approximate value of the maximum probability obtained by the Digital Clocks approach[3] and a halfof it, respectively. In the proposed approach, we searched atmost 5000 paths by letting the parameter k of the k-shortest
paths search algorithm be 5000. For evaluation of existing approach, we used the probabilistic model checker PRISM[12].
The experiments were performed under Intel Core2 Duo
2.33 GHz, 2GB RAM, and Fedora 12 (64bit).

4.4 Results of the Experiments
The results are shown in Table 1. The column of D means
the value of deadline. For each approach, columns of Results,
T ime, and States show the results of model checking, execution time of whole process, and the number of states constructed, respectively. The column M EM in the columns of
the Digital Clocks shows the memory consumption of PRISM.
The columns Loop and Heap in the columns of the proposed
approach show the number of CEGAR loops executed and theTable 2: Analysis of Counter Example Paths
D(µs)
5
10
20

p
1.0938×10−1
1.2635×10−2
1.8500×10−4

P ath
7
43
2534

P robability
1.2500×10−1
1.2695×10−2
1.8501×10−4

CC(ms)
0.7
5.9
296.9

maximum heap size of the Java Virtual Machine (JVM) which
executes our prototype, respectively.
Table 1 shows that for all cases we can dramatically reduce
the number of states and obtain correct results. Moreover, we
can reduce the execution time more than 80 percent except forthe case when deadline = 20µs and p = 1.85 × 10−4 . In
this case, however, the execution time drastically increases.
Table 2 shows the results of analysis of CE paths obtained
when the results of model checking are false. The columnsof P ath, P robability and CC show the number of CE paths,
the summation of occurrence probability of them, and execution time for compatibility checking, respectively. For thisexample, the obtained sets of CE paths are compatible in every case.

4.5 Discussion
From the results shown in Table 1, we can see that our proposed approach is efficient with regard to both execution time
and the number of states. Especially, the number of states
decrease dramatically. The execution time is also decreased
even though we perform model checking several times shownin the column of Loop.
On the other hand, in the case when deadline = 20µs andp = 1.85×10−4 , the execution time increases drastically. We
think that as shown in Table 2 we have to search 2534 paths
and this causes the increase of execution time especially for kshortest paths search. A more detailed analysis shows that theexecution time for k-shortest paths search accounts for 1123
seconds of total execution time of 1186 seconds. Also, theresults shows that the JVM needs 64MB as its heap size in thiscase. This is because compatibility checking for 2534 of paths
needs a large amount of the memory. From the results, wehave to resolve a problem of the scalability when the numberof candidate paths for a CE becomes large.

5 Conclusion
This paper proposed the abstraction refinement techniquefor a probabilistic timed automaton by extending the existing
abstraction refinement technique for a timed automaton.
Future work includes completion of implementation. General DBM does not support not operator[13]; so we have toinvestigate efficient algorithms for the not operator.

Acknowledgments
This work is being conducted as a part of Stage Project,
the Development of Next Generation IT Infrastructure, supported by Ministry of Education, Culture, Sports, Science andTechnology, as well as Grant-in-Aid for Scientific ResearchC(21500036), as well as grant from The Telecommunications
Advancement Foundation.

REFERENCES[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Modelchecking. MIT Press, 1999.
[2] M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang:“Symbolic model checking for probabilistic timed automata,” Information and Computation, Vol. 205, No. 7,
pp. 1027–1077, 2007.
[3] M. Kwiatkowska, G. Norman, and J. Sproston: “Performance analysis of probabilistic timed automata using
digital clocks,” Int. Journal on Formal Methods in System Design, Vol. 29, No. 1, pp. 33–78, 2006.
[4] M. Kwiatkowska, G. Norman, and D. Parker, “Stochastic Games for Verification of Probabilistic Timed Automata,”. In Proc. of the 7th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS’09),
Vol. 5813 of LNCS, pp. 212–227, 2009.
[5] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut: “Counterexample-guided abstraction refinement
for symbolic model checking,” Journal of the ACM,
Vol. 50, No. 5, pp. 752–794, 2003.
[6] T. Nagaoka, K. Okano, and S. Kusumoto: “An Abstraction Refinement Technique for Timed Automata
Based on Counterexample-Guided Abstraction Refinement Loop,” IEICE Transactions on Information and
Systems, Vol. E93-D, No. 5, pp. 994–1005, 2010.
[7] C. Derman. Finite-State Markovian Decision Processes.
New York: Academic Press, 1970.
[8] D. P. Bertsekas. Dynamic programming and optimal
control. Athena Scientific, 1995.
[9] H. Aljazzar and S. Leue: “Directed Explicit StateSpace Search in the Generation of Counterexamples
for Stochastic Model Checking,” IEEE Transactions on
Software Engineering, Vol. 36, No. 1, pp. 37–60, 2010.
[10] J. Bengtsson and W. Yi, “Timed Automata: Semantics,
Algorithms and Tools,”. In Lecture Notes on Concurrency and Petri Nets, Vol. 3098, pp. 87–124, 2004.
[11] M. Kwiatkowska, G. Norman, and J. Sproston: “Probabilistic model checking of deadline properties in theieee1394 firewire root contention protocol,” Formal Aspects of Computing, Vol. 14, No. 3, pp. 295–318, 2003.
[12] A. Hinton, M. Kwiatkowska, G. Norman, and
D. Parker:, “PRISM: A Tool for Automatic Verificationof Probabilistic Systems,”. In Proc. of the 12th Int. Conf.
on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), Vol. 3920, pp. 441–444,
2006.
[13] A. David, J. Hakansson, K. G. Larsen, and P. pettersson,“Model Checking Timed Automata with Priorities using
DBM Subtraction,”. In Proc. of the 4th Int. Conf. on
Formal Modelling and Analysis of Timed Systems, pp.
128–142, 2006.