Reachability Analysis of Probabilistic Timed Automata
Based on an Abstraction Refinement Technique
Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
Graduate School of Information Science and Technology, Osaka University{t-nagaok,a-ito,tstanaka,okano,kusumoto}@ist.osaka-u.ac.jp

ABSTRACT
Model checking techniques are considered as promising techniquesfor verification of information systems due to their ability of exhaustive checking. Well-known state explosion, however, mightoccur in model checking of large systems. In order to avoid it, several abstraction techniques have been proposed. Some of them arebased on CounterExample-Guided Abstraction Refinement (CEGAR) technique proposed by E. Clarke et al.. This paper proposesa reachability analysis technique for probabilistic timed automata.
In the technique, we abstract time attributes of probabilistic timed
automata by our abstraction technique proposed in our previous
work. Then, we apply probabilistic model checking to the generated abstract model which is just a markov decision process (MDP)
with no time attributes. Also, our technique can produce a counterexample as a set of paths when a given model does not satisfy a
specification. The paper also provides some experimental results
on applying our method to IEEE 1394, FireWire protocol. Experimental results show our algorithm can reduce the number of states
and total execution time dramatically compared to one of existing
approaches.

Keywords
Probabilistic Timed Automaton, CEGAR, Model Checking, Realtime System, Formal Verification

1. INTRODUCTION
Model checking[1] techniques are considered as promising techniques for verification of information systems due to their abilityof exhaustive checking. For verification of real-time systems suchas embedded systems, timed automata are often used. On the other
hand, probabilistic model checking[2, 3, 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 of probabilistic timed automata.

Clarke et al. proposed an abstraction technique called CEGAR(CounterExample-Guided Abstraction Refinement)[5]. In the CEGAR technique, we use a counter example (CE) produced by amodel checker as a guide to refine abstracted models. In [6], wehave proposed an abstraction algorithm for timed automata basedon CEGAR. In this algorithm, we generate finite transition systems
as abstract models where all time attributes are removed. The refinement modifies the transition relations of the abstract model sothat the model behaves correctly even if we don’t consider the clock
constraints.
This paper proposes a reachability analysis technique for probabilistic timed automata. In the technique, we abstract time attributes of probabilistic timed automata by applying our abstraction technique for timed automata proposed in [6]. Then, we apply
probabilistic model checking to the generated abstract model which
is just a markov decision process (MDP) with no time attributes.
The probabilistic model checking algorithm calculates summationof 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 constraints,
we add a new flow where we check whether all paths 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.
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 [2, 3, 4] 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 approachalso 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.

2. PRELIMINARY
2.1 Clock and Zone
Let C be a finite set of clock variables which take non-negative realvalues (R≥0 ). A map ν : C → R≥0 is called a clock assignment.
The set of all clock assignments is denoted by RC≥0 . For any ν ∈
RC
and
d
∈
R
we
use
(ν
+
d)
to
denotetheclock
assignment≥0≥0defined as (ν + d)(x) = ν(x) + d for 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.
D EFINITION 2.1. Syntax and semantics of a differential inequality E on a finite set C of clocks 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 thesame as the ordinal inequality.
D EFINITION 2.2. Clock constraints c(C) on a finite set C ofclocks is defined as follows: A differential inequality in on C is anelement of c(C). Let in1 and in2 be elements of c(C), in1 ∧ in2
is also an element 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 of clock assignments that satisfy all the inequalities. In this paper, we treat a zone
D as a set of clock assignments ν ∈ RC
≥0 (For a zone D, ν ∈ Dmeans the assignment ν satisfies all the inequalities in D).

2.2 Probability Distribution
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.

b
a

1

0.5

0.5
x:=0

x<1

d
c

1

x==0∧y>=1

Figure 1: An Example of a PTA

2.4

Timed Automaton

D EFINITION 2.4. A timed automaton A is a 6-tuple (A, L, l0 ,C, I, T ), where A is a finite set of actions, L is a finite set of locations, l0 ∈ L is an initial location, C is a finite set of clocks,
I ⊂ (L → c(C)) is a mapping from locations to clock constraints,
called a location invariant, and T ⊂ L × A × c(C) × R × L isa set of transitions, where c(C) is a clock constraint, called guards
and R = 2C is a set of clocks to reset.
D EFINITION 2.5. 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 be given as (l0 , 0C ) ∈ S. For a transition(l1 , a, g, r, l2 ) ∈ T , the following two transitions are semanticallydefined. The former one is called an action transition, while thelatter 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)

D EFINITION 2.6. 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
2.3 Markov Decision Process
A Markov Decision Process (MDP)[7] is a markov chain with nondeterministic choices.
D EFINITION 2.3. A markov decision process M DP is 3-tuple(S, s0 , Steps), where S is a finite set of states, s0 ∈ S is an initialstate, and Steps ⊆ S × A × Dist(S) is 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.

A PTA is a kind of a timed automaton extended with probabilistic
behavior. In the PTA, a set of probabilistic distributions is usedinstead of a set T of discrete transitions on the timed automaton.
D EFINITION 2.7. A probabilistic timed automaton P T A is a
6-tuple (A, L, l0 , C, I, prov), where A is a finite set of actions, L
is a finite set of locations, l0 ∈ L is an initial location, C is a finite set of clocks, I ⊂ (L → c(C)) is a location invariant andprob ⊆ L × A × c(C) × Dist(2C × L) is a finite set of probabilistic transitions, where c(C) represents a guard condition, andDist(2C × L) represents a finite set of probability distributions p.
The Distribution p(r, l) ∈ Dist(2C ×L) represents the probabilityof resetting clock variables in r and also moving to the location l;

2.3.1 Adversary
An MDP has non-deterministic transitions called action. To resolve
the non-determinism, an adversary is used. The adversary requires
a finite path on an MDP, and decides a transition to be chosen at thenext step.

Figure 1 shows an example of a PTA. In the figure, from the location a, the control moves to the location b with the probability
0.5 and also moves to the location c letting the value of the clock x
reset to zero with the probability 0.5.

2.3.2 Value Iteration
A representative technique of model checking for an MDP is Value
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 obtain the adversary as well as the probability.

D EFINITION 2.8. 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 is a setof states, s0 = (l0 , 0C ) is an initial state, and T Steps ⊆ S ×
A ∪ R≥0 × Dist(S) is composed of action transitions and delaytransitions, where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′ ).

Concrete
model

Initial Abstraction
Counter-example

property

true
property issatisfiedModel Checking

Simulation

refined model+propertyr⊆C∧ν ′ =r(ν)

false
property is
not satisfied

Refinementb) delay transition
if d ∈ R≥0 , and for all d′ ≤ d, I(l)(ν + d′ ), ((l, ν), d, µ) ∈T Steps where µ(l, ν + d) = 1.

Figure 2: A General CEGAR TechniqueConcretemodel

In this paper, using a location l and a zone D, we describe a set ofsemantic states as (l, D) = {(l, ν) | ν ∈ D}.

true
property issatisfied

D EFINITION 2.9. A path ω with length of n on a timed probabilistic system T P SP T A = (S, s0 , T Steps, L′ ) is denoted as follows.
d ,µ

d ,µ

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

dn−1 ,µn−1−→

For model checking of a probabilistic timed automaton, we extract
a number of paths and calculate a summation of their occurrence
probabilities in order to check the probability of satisfying a given
property. The important point is that we have to choose a set ofpaths which are compatible with respect to time elapsing.
L EMMA 2.1. If a set Ω of paths on a timed probabilistic system
T P SP T A satisfies the following predicate isCompatible, then allof the paths over Ω are said to be compatible.
isCompatible(Ω) =

∧ α
β

(li = liβ ∧ dα
true, if ∀i ≤ min(Ω)
i = di )βαω ,ω ∈Ω∧ω α ̸=ω β




or
there
existsi≤ min(Ω) such that


∧ α β
∧

β

(li ̸= li ∧ dα=dβi ∧ (ljα= ljβ ∧ dαi
j = dj )),j≤iω α ,ω β ∈Ω∧ω α ̸=ω β


∧



and also
isCompatible(Ω′ )



′
Ω

Ω ∈2 ∧
Ω′ ̸=Ω∧|Ω′ |≤2false, otherwise.

In Lemma2.1, we give the predicate isCompatible for a set Ω ofpaths on a timed probabilistic system. In the lemma, we let pathsin Ω be compatible if there is no contradiction with respect to time
elapsing at the branching point of all the paths in Ω, and also if
the compatibility is kept for every subset of Ω which contains morethan two paths.

2.6 CounterExample-Guided Abstraction Refinement
2.6.1 General CEGAR TechniqueSince model abstraction sometimes over-approximates an originalmodel, we may obtain spurious CEs which are infeasible on theCounter-example

Model Checking

Simulation

refined model+property
refined Concrete model+property(ln , νn ), where (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 ) for0 ≤ i ≤ n − 1.

Initial Abstraction

property

Model Transformation

false
property is
not satisfied

Refinement

Compatibility
Checking

Figure 3: Our CEGAR Technique for Reachability Analysis of
a Probabilistic Timed Automaton
original model. Paper[5] gives an abstraction refinement framework called CEGAR (CounterExample-Guided Abstraction Refinement) (Fig.2).
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 the model checker reports thatthe model satisfies a given specification, we can conclude that theoriginal model also satisfies the specification, because the abstract
model is an over-approximation 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 haveto refine the abstract model to eliminate the spurious CE, and repeat
these steps until valid output is obtained.

2.6.2

CEGAR Technique for a Timed Automaton

In [6], we have proposed the abstraction refinement technique fora 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 by model checking on an abstract
model, we transform the transition relation on the abstract model sothat the model behaves correctly even if we don’t consider the clock
constraints. Such transformation obviously represents the difference of behavior caused by the clock attributes. Therefore, the finite number of application of the refinement algorithm enables us
to check the given property without the clock attributes. Since ourapproach does not restore the clock attributes at the refinement step,
the abstract model is always a finite transition system without theclock attributes.

3.

PROPOSED APPROACH

In this section, we will present our abstraction refinement techniquefor a probabilistic timed automaton. In the technique, we use theabstraction refinement technique for a timed automaton proposed

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
Products of zones obtained byforward and backward simulation
d
a
b
0.5
1.0
x==y &
x==y&
x==y &
x<1
x<1
x<1

b
1
0.5

a

d

0.5
x:=0

1

c

Figure 4: An Initial Abstract Modelin [6]. In addition, we resolve the compatibility problem shown in
Sec.2.5 by performing a backward simulation technique and generating additional location to distinguish the required condition forevery incompatible path. Figure 3 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 anda 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 to states where err (which means
an error condition in general) is satisfied, is less than p.

3.1 Initial Abstraction
The initial abstraction removes all the clock attributes from a given
probabilistic timed automaton as well as the technique in The generated abstract model over-approximates the original probabilistic
timed automaton.

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
Products of zones obtained byforward and backward simulation
d
a
c
0.5
1.0
y-x>=1
x==y &
x==0 &
y>=1
y>=1

Figure 5: Products of zones obtained by Forward and Backward Simulationˆ ∧, 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 reset with apath on an abstract model in order to show the difference of r overthe probabilistic distribution p.
For the abstract model shown in Fig.4, Value Iteration outputs 1.0
as the probability that it reaches to the state d from the state a. On
the other hand, k-shortest paths search (k ≥ 2) detects two paths
τ,0.5,{}

τ,1.0,{}

τ,0.5,{x:=0}

τ,1.0,{}

ω̂ α = a −→ b −→ d and ω̂ β = a−→c −→ d,where τ represents a label for transitions with no label in the figure.

3.3 Simulation
D EFINITION 3.1. For a given probabilistic timed automaton
P T A = (A, L, l0 , C, I, prob), a markov decision process
ˆ P T A = (Ŝ, ŝ0 , Steps)ˆ
M DP
is produced as its abstract model,ˆ = { (s, a, p) | (s, a, g, p) ∈where Ŝ = L, ŝ0 = l0 , and Steps
prob }

Simulation checks whether all the paths obtained by k-shortest paths
search are feasible or not on the original probabilistic timed automaton. We use the simulation algorithm proposed in [6] If there
is at least one path which is infeasible on the original PTA, we proceed to the abstraction refinement step.

3.4 Abstraction Refinement
Figure 4 shows an initial abstract model for the PTA shown in Fig.1
As shown in the figure, the abstract model is just an MDP where allof the clock constraints are removed though we keep a set of clock
reset as a label of transitions.

3.2 Model Checking
In model checking, we apply Value Iteration[8] into the markov
decision process obtained by abstraction and calculate a maximum
reachability probability. Also, it decides an action 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 for the probability calculation. To obtain the concrete paths, we use an approach
proposed in [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 kshortest paths search on the graph.
ˆ PTA =D EFINITION 3.2. A path ω̂ on an abstract model M DPˆ(Ŝ, ŝ0 , Steps) for P T A = (A, L, l0 , C, I, prob) is given as follows,ω̂ = ŝ0

a0 ,p0 ,r0−→ ŝ1

a1 ,p1 ,r1−→ . . .

an−1 ,pn−1 ,rn−1

−→

ŝn

In this step, we refine the abstract model so that the given spurious CE also becomes infeasible on the refined abstract model. We
can use the algorithm proposed in [6]. Since the algorithm of [6]performs some operations on transitions of a timed automaton, we
replace such operations by those on probability distributions of aprobabilistic timed automaton.

3.5

Compatibility Checking

When all the paths obtained by k-shortest paths search are feasible
and a summation of occurrence probabilities of them is greater thanp, we also have to check whether all the paths are compatible or not.
In this compatibility checking step, at each location of the paths, wehave to obtain a condition (zone) which is reachable from the initialstate and also reachable to the last state along with the path. Next,
we check the compatibility of such conditions among all paths. To
obtain such conditions, we have to perform both forward simulation
shown in Sec. 3.3 and backward simulation for each path, andmerge the results. For the result of forward simulation, we canreuse the result obtained in the Simulation step. Then we check thecompatibility based on Lemma 2.1. Paper[10] shows the algorithmof compatibility checking in detail. In the algorithm, we check thecompatibility of such products of zones at every location of thepaths.
Figure 5 shows the products of zones obtained by both forward andbackward simulation for two paths ω̂ α and ω̂αβ in Sec.3.2. For theω̂path ω̂ α , the product zone at a is given as Dc,0= (x == y ∧ x <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

Result
false
true
false
true
false
true

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

b1 1

0.5

a

x==y

0.5 x:=0

x<1

c1

4.

b2
x>=1&x==y

0.5
x:=0

0.5
x:=0

Heap(M B)
8.0
8.0
8.0
8.0
64.0
8.0

EXPERIMENTS

We have implemented a prototype of our proposed approach with
Java, and performed some experiments. Though the prototype cancheck the compatibility of a given set of paths, currently it cannot
deal with the model transformation.

x==0∧y>=1

c2 1
y-x>=1

0.5

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

abstract model outputs 0.5 as the maximum probability.

d0<=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)1), which means a zone which is reachable from the initial state
and also can move to d. Similarly, for the path ω̂ β , the product
ω̂ β
ω̂ α
ω̂ β
zone is given as Dc,0= (x == y ∧ y > 1). Since Dc,0and Dc,0α
contradict each other, we can conclude that the paths ω̂ and ω̂ β
are incompatible each other.

The prototype performs k-shortest paths search and simulation concurrently in order to reduce execution time. By implementing thealgorithms concurrently, we have not to wait until all of k paths aredetected, i.e. if a path is detected by the k-shortest paths searchalgorithm, 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 andthe refinement algorithm is applied. If other paths which do not
overlap with the previous spurious CEs, are detected, we can apply simulation and refinement algorithms to it again. This helps us
reduce the number of CEGAR loop.

3.6 Model Transformation

4.1

Figure 6: A Transformed PTA

When the compatibility check procedure decides a given set Ω̂ ofpaths 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 offorward and backward simulation for a path ω̂ ∈ Ω̂. 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 associated with the duplicated location. Detailed Algorithms totransform the model are given in [10].
Figure 6 shows the transformed PTA by applying the model transformation procedure for the paths ω̂ α and ω̂ β . The locations b1
and c1 are duplicated locations based on the path ω̂ α and the zone
ω̂ β
Dc,0
= (x == y ∧ x < 1) on the location a. We associate invariβω̂ants to b1 and c1 based on zones which are reachable from Dc,0through transitions from a to b, and from a to c, respectively. Also,
we duplicate a transition from b to d as the transition from b1 to d
because the transition is feasible from the invariant of b1 . On theother hand, we do not duplicate a transition from c to d because thetransition is not feasible from the invariant of c1 . Similarly, locations b2 and c2 are duplicated locations based on the path ω̂ β andω̂ βthe zone Dc,0
. Locations b3 and c3 are generated as complementsof the invariant associated with each duplicated location in order topreserve the equivalence.

By transforming the original PTA in such a way, if we remove allclock constraints from the model in Fig.6, Value Iteration on its

Goal of the Experiments

The goal of this experiment is to check that our approach, which
also searches a CE, is performed within realistic time. In this experiment, we evaluated the performance of our proposed approachwith regard to execution time, memory consumption, and qualities of obtained results. As a target for comparison, we chose theapproach of Digital Clocks[3], which is considered as a basic approach, where they approximate clock evaluations of a PTA by integer values.

4.2

ExampleWe used a case study of the FireWire Root Contention Protocol[11]as an example for this experiment. This case study concerns theTree Identify Protocol of the IEEE 1394 High Performance Serial
Bus (called “FireWire”) which takes place when a node is addedor removed from the network. In the experiment, we checked theprobability that a leader is not selected within a given deadline. The
probabilistic timed automaton for the example is composed of twoclock 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 thanp.” We considered three scenarios where the parameter deadline
is 5, 10, 20 µs, respectively. Also, for each scenario, 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 half of it, respectively. In the proposed approach,
we searched at most 5000 paths by letting the parameter k of the kshortest paths search algorithm be 5000. For evaluation of existing
approach, we used the probabilistic model checker PRISM[12].

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

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 valueof deadline. For each approach, columns of Results, T ime,
and States show the results of model checking, execution time ofwhole process, and the number of states constructed, respectively.
The column M EM in the columns of the Digital Clocks shows thememory consumption of PRISM. The columns Loop and Heap in
the columns of the proposed approach show the number of CEGAR
loops executed and the 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 thenumber of states and obtain correct results. Moreover, we can reduce the execution time more than 80 percent except for the casewhen 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 columns of P ath,
P robability and CC show the number of CE paths, the summationof occurrence probability of them, and execution time for compatibility checking, respectively. For this example, 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 thenumber of states. Especially, the number of states decrease dramatically. The execution time is also decreased even though we perform model checking several times shown in the column of Loop.
On the other hand, in the case when deadline = 20µs and p =1.85 × 10−4 , the execution time increases drastically. We thinkthat as shown in Table 2 we have to search 2534 paths and thiscauses the increase of execution time especially for k-shortest paths
search. A more detailed analysis shows that the execution time fork-shortest paths search accounts for 1123 seconds of total execution time of 1186 seconds. Also, the results shows that the JVM
needs 64MB as its heap size in this case. This is because compatibility checking for 2534 of paths needs a large amount of thememory. From the results, we have to resolve a problem of thescalability when the number of candidate paths for a CE becomeslarge.

5. CONCLUSION
This paper proposed the abstraction refinement technique for a probabilistic timed automaton by extending the existing abstraction refinement technique for a timed automaton. The main contributionof this work is generation of a CE. Also, the experimental results
show the efficiency of our technique compared to one of existing
approaches.

Future work includes completion of implementation. General DBM
does not support not operator[13]; so we have to investigate 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 and Technology, as
well as Grant-in-Aid for Scientific Research C(21500036), as wellas grant from The Telecommunications Advancement Foundation.

6.

REFERENCES[1] E. M. Clarke, O. Grumberg, and D. A. Peled, editors. Modelchecking. MIT Press, 1999.
[2] M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang.
Symbolic model checking for probabilistic timed automata.
Information and Computation, 205(7):1027–1077, 7 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,
29(1):33–78, 7 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), volume 5813 of LNCS,
pages 212–227, 9 2009.
[5] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut.
Counterexample-guided abstraction refinement for symbolicmodel checking. Journal of the ACM, 50(5):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,
E93-D(5):994–1005, 5 2010.
[7] C. Derman, editor. 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 state-space searchin the generation of counterexamples for stochastic model
checking. IEEE Transactions on Software Engineering,36(1):37–60, 1 2010.
[10] A. Ito, T. Nagaoka, K. Okano, and S. Kusumoto.
Reachability analysis for probabilistic timed system based on
timed abstraction refinement technique (in japanese). In
IEICE Technical Report, volume 109, pages 85–90, 3 2010.
[11] M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic
model checking of deadline properties in the ieee1394
firewire root contention protocol. Formal Aspects ofComputing, 14(3):295–318, 4 2003.
[12] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker:.
PRISM: A tool for automatic verification of probabilistic
systems. In Proc. of the 12th Int. Conf. on Tools andAlgorithms for the Construction and Analysis of Systems(TACAS’06), volume 3920, pages 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, pages 128–142,
2006.