IEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x

submitted to IEICE TRANSACTIONS on Information and Systems

1

PAPER

An Abstraction Refinement Technique for Timed Automata Basedon Counterexample-Guided Abstraction Refinement Loop
Takeshi NAGAOKA† , Nonmember, Kozo OKANO† , and Shinji KUSUMOTO† , Members

SUMMARY
Model checking techniques are useful for design of high-reliable information systems. Well-known state explosion, however, might occur inmodel checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques
have been proposed. Some of them are based on CounterExample-Guided
Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke
et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. The proposed technique is based on CEGAR, in which we use a counter example as a guideto refine the model abstracted excessively. Although, in general, the refinement operation is applied to abstract models, our method modifies theoriginal timed automata, and next generates refined abstract models fromthe modified automata. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
key words: Model Checking, Timed Automaton, Model Abstraction, CEGAR

1.

Fig. 1

General CEGAR Algorithm

Fig. 2

Our Proposed Algorithm

Introduction

A model checker checks that a given system modeled in a
finite automaton satisfies given specifications by searching
the finite transition system exhaustively. It sometimes has,
however, limitation in scalability. In order to improve thescalability, model abstraction technique is important[1]–[3].
In verification of real time systems, a timed automaton
has widely been used[7], [8], which can describe behavior of
realtime systems. In a timed automaton, real-valued clock
constraints are assigned to its control state (called a location). Therefore, it has an infinite state space represented ina product of discrete state space made by locations and continuous state space made by clock variables. In traditionalmodel checking for a timed automaton, using the property
that we can treat the state space of clock variables as a finite
set of regions; we can perform model checking on timed automata models. However, the size of such regions increases
exponentially with the number of clock variables; thus anabstraction technique is also needed.
Paper[1] proposed an abstraction algorithm called CEGAR (CounterExample-Guided Abstraction Refinement)
shown in Fig.1. The algorithm is used for abstraction of finite models[1], [2], hybrid systems[3], timed automata[11]–[13], and other models. In the CEGAR algorithm, we use acounter example produced by a model checker as a guide torefine excessively abstracted models. A general CEGAR algorithm consists of several steps. First, it abstracts the origi†
Graduate School of Information Science and Technology, Osaka University
Machikane-yama 1–3, Toyonaka City, Osaka, 560–8531 Japannal model (the obtained model is called abstract model) andperforms model checking on the abstract model. Next, if acounter example (CE) is found, it checks the counter example on the concrete model. If the CE is spurious, it refines
the abstract model. The 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 modelsatisfies given specifications, the concrete model also satisfies them.
This paper proposes a new concrete CEGAR algorithm
for a timed automaton. The first step of the algorithm isabstraction, in which we delete all of time attributes fromthe given timed automaton. The obtained automaton is justa finite automaton preserving the transition relations of thetimed automaton; therefore the obtained finite automaton is,in general, over-approximated of the original one. We restrict the class of the verification properties into reachability; thus if an abstract model satisfies a given property thenthe concrete model also satisfies the property.
In general, CEGAR algorithms[1]–[3], [11]–[13] directly transforms an abstract model using counter examples in the refinement step. Our proposed method, how-

IEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x2

ever, doesn’t directly transform an abstract model. It firsttransforms the original model using counter examples andthen it creates a new abstract model from it by removing
clock attributes; thus our algorithm indirectly refines the abstract model. The algorithm transforms the original timed
automaton by adding extra transitions and removing sometransitions but it preserves the behavioral equivalence of thetimed automaton and prevents the spurious counter examples. More concretely, it duplicates locations and transitions so that its abstract model can tell behavioral difference
caused by clock values which affects the counter examples.
Consequently the obtained new abstract model does not accept the spurious counter example.
As related works, papers[11]–[13] have proposed CEGAR based abstraction techniques for timed automata. Although these techniques mainly refine the abstract models
by adding clock variables which have removed by abstraction, our refinement method modifies the original timed automata and produces the refined abstract model from themodified models, instead of adding clock variables.
The rest of the paper is organized as follows. In Sec.
2, some definitions are described. Sec. 3 gives our CEGAR
algorithm and its application to a simple example. Comparison with other related methods is also given. Sec. 4 proves
the correctness of the algorithm. Sec. 5 concludes the paper.
2.

Preliminaries

In this section, we give definitions of a timed automaton, a
region automaton which specifies whole states of a timed
automaton with finite clock regions, and others.
2.1

Timed Automaton

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 aelement of c(C).
Definition 2.3 (Timed Automaton). A timed automaton A
is a 6-tuple (A, L, l0 , C, I, T ), where
A: a finite set of actions;
L: a finite set of locations;
C: a finite set of clocks;
l0 ∈ L: an initial location; andT ⊂ L × A × 2c(C) × R × L,
where 2c(C) is a set of clock constraints, called guards;

R = 2C : a set of clocks to reset;
and I ⊂ (L → 2c(C) ): a mapping from locations to clock
constraints, called location invariants.
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 can extend the domain of ν into a set of C
as follows: ν ∈ RC
≥0 . We define (ν + d)(x) = ν(x) + d
for d ∈ R≥0 . r(ν) = ν[x 7→ 0], x ∈ r is also defined forr ∈ 2C . By N , a set of whole ν is denoted.
a,g,r

Definition 2.4 (Semantics of Timed Automaton). For agiven timed automaton A = (A, L, l0 , C, I, T ), let a setof whole states of A be S = L × N . The initial state of A
shall be given as (l0 , 0C ) ∈ S.
a,g,r
For a transition l1 −→ l2 (∈ T ), the following two transitions are semantically defined. The first 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)

Definition 2.5 (A semantic model of 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. By T (A ),the semantic model of A is denoted.
2.2

Region Automaton

For a given timed automaton A , we can introduce a corresponding clock region CR(A ) [4], [5]. By [u], an element(a region) in CR(A ) is denoted. For [u] ∈ CR(A ), g([u])
and I([u]) represent that any point in [u] satisfies a guard g
and invariant I, respectively. Also by r([u]), applying clock
resetting r onto [u] is denoted, where r([u]) = [u][x 7→ 0],
and x ∈ r.
Definition 2.6 (Region Automaton). A region automaton
Ar = (A, Lr , lr 0 , Tr ) of a given timed automaton A =(A, L, l0 , C, I, T ) is defined as follows. Lr ⊂ L × CR(A ),lr 0 = (l0 , [0C ]), where [0C ] satisfies I(l0 ),Tr ⊂ Lr × A × Lr ,Tr consists of(l , [u]) ⇒ (l ′ , [v]) iff (l , u) ⇒ (l, u′ ) ∈ T (A ) for d ∈ R≥0ad∧ (l , u′ ) ⇒ (l ′ , v) ∈ T (A ) for a ∈ A∧ u ∈ [u] ∧ v ∈ [v].
a2.3

DBM (Difference Bound Matrix)

In [7], [10], a data structure DBM(difference bound matrix)
is introduced to manage a set of differential inequalities of
two clocks over a finite clock set C.
We represent DBM as a set of some elements in theclock region CR(A ). Therefore a set of states of a region

NAGAOKA et al.: AN ABSTRACTION REFINEMENT TECHNIQUE FOR TIMED AUTOMATA BASED ON CEGAR LOOP

3

automaton Ar = (Lr , lr 0 , Tr , A), can be represented in(l , D) = {(l , [u]) | [u] ∈ D} using the corresponding DBM
D. Paper[7] gives operation functions on DBM, such as up,
and and other functions, which represent elapsing time, intersection of time spaces and so on, respectively. There isa minimum set of differential inequalities which can represent DBM D [7]. Such a set is denoted by Ineqset(D).
Ineqset(D) can be obtained by reduction operations on
DBM. A set of every region which satisfies an invariant I(l )of location l is denoted by (l , DInv ).
2.4

General CEGAR Algorithm

Model abstraction sometimes over-approximates an original model, which may produce spurious counter examples. They are not actually counter examples in the original model. Paper [1] gives an algorithm called CEGAR(Counterexample-Guided Abstraction Refinement) (Fig.1).
In the algorithm, at the first step (called Initial Abstraction), it over-approximates the original model. Next, we perform model checking on the abstract model. In this step, if
the model checker reports that the model satisfies a given
specification, the original model also satisfies the specification, because the abstract model is an over-approximationof the original model. If the model checker reports that themodel does not satisfy the specification, however, we haveto check whether a counter example produced is spurious
counter example or not in the next step (called Simulation).
In the Simulation step, if we find the counter example isvalid, we stop the loop. Otherwise, we have to refine the abstract model to eliminate the spurious counter example, andrepeat these steps until valid output is obtained.
3.

Our CEGAR Algorithm for Timed Automaton

Our proposed algorithm generates an abstract model M̂from a given timed automaton A by applying an abstraction function h, and performs model checking on M̂ . M̂is in fact a finite automaton. If a counter example T̂ (represented as a path on the abstract model) is found duringmodel checking, we concretize T̂ by applying inverse function h−1 .The concretized one is a set of paths. We denote it
by T (which is a set of paths on A ). At Simulation Step, it
checks whether each path in T is feasible on A or not. If
every path in T is infeasible, the next step shall refine themodel so that the counter example T̂ becomes infeasible.
Our algorithm does not directly refine M̂ but it modifies A
and then obtains a new abstract mode by applying h to themodified timed automaton. Figure 2 shows flow of our CEGAR algorithm.
∨
The proposed algorithm checks a property AG e∈E ¬e,where E (⊂ L) of a timed automaton A is a set of error locations of the target system. The property means there is nopath to locations in E from the initial state. Please note thatany counter example of such a property can be represented
in a finite length of sequence without loops. Therefore, hereafter, we assume that counter examples are finite sequences

without loops.
3.1

Abstract Model

Definition 3.1 defines the abstraction function h on Lr of aregion automaton Ar .
Definition 3.1 (Abstraction Function h). For a region automaton Ar = (A, Lr , lr 0 , Tr ) of a given timed automaton
A , an abstraction function h : Lr → Ŝ is defined as follows:∀lr i , lr j ∈ Lr . h(lr i ) = h(lr j ) ⇐⇒ Loc(lr i ) = Loc(lr j ),where Loc : Lr → L is a function which retrieves a location attribute from a state of Ar . The inverse function
h−1 : Ŝ → 2Lr of h is also defined as in a usual manner.
The abstraction function h defined in Definition 3.1
maps any state of Lr which belongs to the same location
into the same abstract state. Otherwise they are mapped into
the different states. This means that there is a one-to-one
correspondence between the location set of A and the abstract state set Ŝ. Therefore, the abstraction function h canbe extended its domain as in Definition 3.2.
Definition 3.2 (Extension of Abstraction Function h). Abstraction function h : L → Ŝ of a timed automaton A =(A, L, l0 , C, I, T ) is defined as follows:∀li , lj ∈ L. h(li ) = h(lj ) ⇐⇒ li = lj .
Similarly, the inverse function h−1 : Ŝ → L of h is also
defined.
Symbols decorated with ‘ˆ’ represent those of an abstract model (i.e. Ŝ represents a state set of an abstract
model). Definition 3.3 gives an abstract model M̂ of a given
timed automaton A using the abstraction function h definedin Definition 3.2.
Definition 3.3 (Abstract Model). An abstract modelM̂ = (Ŝ, ŝ0 , →)
ˆ of a given timed automaton A =(A, L, l0 , C, I, T ) using the abstraction function h definedin Definition 3.2 is defined as follows:• Ŝ = {h(l ) | l ∈ L)},• sˆ0 = h(l0 ), and• →ˆ = {(lˆ1 , a, lˆ2 ) | (l1 , a, g, r, l2 ) ∈ T }.
Definition 3.4 (Counter Example). A counter example onM̂ is a sequence of states of Ŝ. A counter example T̂ oflength n is represented in T̂ = ⟨ŝ0 , · · · , ŝn ⟩.
A set T of a run sequences on A obtained by concretizing a counter example T̂ = ⟨ŝ0 , · · · , ŝn ⟩, is defined asfollows:
a1 ,g1 ,r1

a2 ,g2 ,r2

an ,gn ,rn

T = {(l0 −→ l1 −→ · · · −→ ln )|( li = h−1 (si ) for 0 ≤ i ≤ n ) ∧( (li−1 , ai , gi , ri , li ) ∈ T for 1 ≤ i ≤ n )}.

IEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x

4Abstraction
Inputs A , h{h = abstraction function}Ŝ := ∅, →
ˆ := ∅ {M̂ = (Ŝ, ŝ0 , →)}ˆ
foreach l ∈ L do
Ŝ := Ŝ ∪ {h(l)}end forŝ0 := h(l0 )foreach (l1 , a, g, r, l2 ) ∈ T do→:=→ ∪{(h(l1 ), h(l2 ))}end forreturn M̂
Fig. 3

Abstraction

Fig. 6Counter Example

Fig. 7

Refined Model

Simulation
a ,g1 ,r1
a ,g2 ,r2
an ,gn ,rn
Inputs A , t = (l0 1−→
l1 2−→· · · −→ ln (ln = e))C
R0 := (l0 , D0 ) {D0 = {0 }}D := up(D0 ) {Any elapsing time}
D := and(D, I(l0 )) {Add Invariant of l0 }for i := 1 to n do
Ri :=Reach(A , Ri−1 , (li−1 , ai , gi , ri , li ))if Ri = ∅ thenreturn false
end ifend forreturn true
Fig. 4

Simulation

Reach
Inputs A , R = (l, D), (l1 , a, g, r, l2 )D := and(D, g) {add guards of transitions}
D := reset(D, r) {reset the clocks}
D := and(D, I(l2 )) {add Invariant of l2 }D := up(D) {Any elapsing time}
D := and(D, I(l2 )) {add Invariant of l2 }return (l2 , D)
Fig. 5

3.2

Reach

Initial Abstraction

Initial Abstraction generates an abstract model M̂ from a
timed automaton A using the abstraction function h. Figure
3 shows the algorithm of Initial Abstraction.
3.3 Simulation
For a set T of concretized counter example sequences obtained from T̂ on M̂ , Simulation performs the algorithm in
Fig.4 on each sequence t ∈ T . Reachability from the firstlocation of t to the last location of t is checked in Simulation
using a procedure Reach in Fig.5. Reach uses some operation functions of DBM. The DBM operation “up” applies
time elapsing to the DBM, and “and” imposes a differential
inequality to the DBM[7]. In the algorithm, we extend thedomain of the operation “and” to clock constraints. Whenthe algorithm in Fig.4 returns false, the counter example T̂ isjudged as a spurious counter example. By tunable , the concrete path input is denoted. The next step refines the abstract
model with tunable .

3.4

Refinement of Abstract ModelIn this step, we have to generate a refined abstract model
which does not admit the spurious counter example (wecall it the spurious CE free model for a given CE). Whena counter example is judged as a spurious counter example
for a concretized path tunable , there is a Bad State l̂b in the
abstract model (Fig.6). A Bad State l̂b is the abstract statethat the state sets B1 (= (lb , D1 )) and B2 (= (lb , D2 )) are
merged (mapped into the same state). The state set B1 has
the states which are reachable from the initial state but unreachable to the next location lnext . On the other hand, thestate set B2 has the states which are unreachable from theinitial state, but reachable to lnext . In general, refinement algorithm should divide the state l̂b into more than two states
as the state set B1 and the state set B2 are mapped into differential states. Dividing of a state space of a timed automaton usually needs subtraction operation of DBM. However,
DBM is not closed under subtraction operation[10]; therefore, applying such an approach is difficult.
We propose another approach, in which we duplicate
the state set B1 on the concrete model instead of dividing
a bad state. Also we perform other transformation on theconcrete model so that the states in B2 become unreachable
from the initial state obviously (without considering clock
constraints). Next, we produce the spurious CE free modelby applying the abstraction function to the transformed concrete model.
The algorithm of Refinement in Fig.8 consists of threeNAGAOKA et al.: AN ABSTRACTION REFINEMENT TECHNIQUE FOR TIMED AUTOMATA BASED ON CEGAR LOOP5

sub algorithms, called duplication of states, duplication oftransitions, and removal of transitions, shown in Fig.9, 10,
and 11, respectively. The state set B1 is obtained on the way
in the Simulation algorithm. At the line 6 in Fig.4, when
Ri = ∅ is true, B1 corresponds to a previous reachable set
Ri−1 .
In the algorithm ‘DuplicateState’, we generate the state
set B1′ = (lb′ , D1 ) as the duplication of B1 . In the timed automaton level, this transformation generates just a new location lb′ , and the location lb′ has an invariant Ineqset(D1 )which represents D1 .
The algorithm ‘DuplicateTransition’ generates a transition (lprev , a, g, r, lb′ ) as a duplication of the transition(lprev , a, g, r, lb ). Also, we duplicate transitions which arefeasible from the states in (lb , D1 ). Due to this transformation, we can establish bi-simulation relations between thestates in (lb , D1 ) and their duplications in (lb′ , D1 )[15].
The algorithm ‘RemoveTransition’ removes the transition (lprev , a, g, r, lb ) if the following condition is satisfied; the state set which is reachable from (lprev , Dinv )through (lprev , a, g, r, lb ) equals B1 . In such a case, because we can assume the transition (lprev , a, g, r, lb ) equals(lprev , a, g, r, lb′ ), we can remove the transition. Otherwise,
we cannot remove the spurious counter example with only
one-time application of a Refinement algorithm. In such acase, the following CEGAR loops will find the same spurious counter example, and we apply Refinement algorithm
for it again. In Sec.4, we prove that applying Refinement algorithm for the same spurious counter example several times
can remove it from the abstract model.
The operation “relation(D, D′ )” returns a relation between D, D′ such as ⟨D ⊆ D′ , D ⊇ D′ ⟩.
Figure 7 shows a refined model. Dotted arrows in the
figure denote transitions which are removed through Refinement algorithm.
For states to duplicate, transitions to duplicate and transitions to remove, the following lemmas hold. Proofs ofthem are obtained from algorithm straightforward way, andis omitted due to paper space.
Lemma 3.1 (States to Duplicate). Let B1 = (lb , D1 ) andduplication of a location lb be lb′ . A set of states to duplicate,of a region automaton is (lb′ , D1 ).
Duplication of transition duplicates the following kindsof transitions: “transitions from lprev to lb ,” and “ transitions
not only from lb but also enable from (lb , D1 ).”Lemma 3.2 (Transitions to Duplicate). For a region automaton Ar = (A, Lr , lr 0 , Tr ), B1 = (lb , D1 ), states toduplicate (lb′ , D1 ), and a transition eb = (lprev , a, g, r, lb )in a counter example, transitions to duplicate of a region
automaton is:
Tr d = {(lprev , [v]) ⇒ (lb′ , [v ′ ]) |∀(lprev , [v]) ∈ (lprev , DInv ).
a′aFig. 8

Refinement

DuplicateState
Input A , B1 = (lb , D1 )lb′ := newLoc() {Generate a new location lb′ }L := L ∪ {lb′ }I( lb′ ) := Ineqset(D1 ) {A set of inequalities representing D1 }Fig. 9Duplication of States

DuplicateTransition
Inputs A , B1 = (lb , D1 ), eb = (lprev , a, g, r, lb ){eb = a transition to lb }T := T ∪ {(lprev , a, g, r, lb′ )}{Duplicate a transition eb to a BadState}
foreach (l1 , a′ , g ′ , r ′ , l2 ) ∈ T such that l1 = lb do
if Reach( A , (lb , D1 ), (l1 , a′ , g ′ , r ′ , l2 )) ̸= ∅ thenT := T ∪ {(lb′ , a′ , g ′ , r ′ , l2 )}{duplicate transitions from lb only enable from ((lb′ , D1 ).)}
end ifend forFig. 10Duplication of Transitions

RemoveTransition
Inputs A , B1 = (lb , D1 ), eb = (lprev , a, g, r, lb ){eb = a transition to lb }P rev := (lprev , DInv ){a set of every region satisfying an invariant of lprev }R :=Reach(A , P rev, eb ) {obtain regions of lb reachable from P rev}
if relation(R, B1 ) = ⟨true, true⟩ then{when R = B, relation(R, B1 ) returns ⟨ true, true⟩.}
T := T \ {(l, a, g, r, lb )}end ifFig. 11

Removal of Transitions

Lemma 3.3 (Transitions to Remove). For a region automaton Ar = (A, Lr , lr 0 , Tr ), B1 = (lb , D1 ), states to duplicate (lb′ , D1 ), and a previous location lprev of a location in acounter example, transitions to remove of a region automaton is:
Tr r = {(lprev , [v]) ⇒ (lb , [v ′ ]) |∀(lprev , [v]) ∈ (lprev , DInv ).
a(lprev , [v]) ⇒ (lb , [v ′ ]) ∈ Tr }.
a

The algorithm of Removal of Transitions removes transitions only when a set of states reachable from lprev is thesame as a set (lb , D1 ) of Bad States. Therefore, for everya(lprev , [v]) ⇒ (lb , [v ′ ]) ∈ Tr r , (lb , [v ′ ]) ∈ (lb , D1 ) holds.
It means that every transition in Tr r has its duplication in
Tr d .
3.5

Example′∀(lb , [v ]) ∈ (lb , D1 ).(lprev , [v]) ⇒ (lb , [v ]) ∈ Tr }∪{(lb′ , [v]) ⇒ (l, [v ′ ]) |∀a ∈ A.∀(lb , [v]) ∈ (lb , D1 ).
a∀(l, [v ′ ]) ∈ Lr .(lb , [v]) ⇒ (l, [v ′ ]) ∈ Tr }.
aRefinement
Inputs Ai , h, B1 = (lb , D1 ), eb = (lprev , a, g, r, lb ){eb = a transition to lb }Ai+1 := Ai
Ai+1 := DuplicateState(Ai+1 , B1 ) {Duplication of States}
Ai+1 := DuplicateTransition(Ai+1 , B1 , eb ){Duplication of Transitions}
Ai+1 := RemoveTransition(Ai+1 , B1 ) {Removal of Transitions}M̂i+1 :=Abstraction(Ai+1 , h)return M̂i+1

Here, we give an example of applying our abstraction
method to Light Switch model[7]. The model is shown in
Fig12, and it is composed of a switch model (left side of theIEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x

6

Fig. 12Light Switch modelFig. 15First refinement

Here, we show an example of applying our abstraction
method to the model.
As a first step, we produce an initial abstract modelfrom the parallel composition. In this step, we apply Initial
Abstraction which removes clock variables x and y from thecomposition. Figure 14 shows the initial abstract model.
Next, we perform model checking on the abstract
model, and the model checker outputs a counter example ⟨(of f, idle), (dim, relax), (bright, idle)⟩.
Thiscounter example corresponds to a path from (of f, idle) to(bright, idle) in the original automaton.
The path in the concrete model in Fig.13 correspondFig. 13

Fig. 14

ing to this counter example is (of f, idle)

Parallel composed model

τ,x≤10∧y>10,∅

Initial abstract model

figure) and a user model (right side of the model). Hereafter,
we assume that locations (dim, idle) and (bright, idle) of
the two models are error locations.
In order to apply our method to these models, first, wehave to produce a parallel composition of the models. Figure 13 shows the composition. Transitions with no label inthe figure are assumed to be labeled with an action τ . The
property which we want to check is:AG¬((dim, idle) ∨ (bright, idle)).

(1)

For the property (1) and the model of Fig13, the model
checker UPPAAL[9] outputs a result of “valid”. This means
the model of Fig13 satisfies the property (1).

τ,true,{x,y}−→(dim, relax)−→(bright, idle) only. Therefore,
we reproduce the path on the concrete model. When we simulate this path on the original automaton, however, a transition from (dim, relax) to (bright, idle) is unable. The
reason is as follows; a reachable clock state space of the(bright, idle) always satisfies x = y, and it does not satisfy
the guard condition x ≤ 10 ∧ y > 10. Therefore, we canconclude that the counter example is spurious. At the sametime, we can obtain the state set ((dim, relax), D1 )(D1 is aset of regions which satisfy x = y) as B1 , and the transition((of f, idle), τ, true, {x, y}, (dim, relax)) as eb .
In the refinement step, first, we duplicate the location (dim, relax) on the timed automaton. (a duplicate of(dim, relax) is denoted by (dim, relax′ )). Please note that
we duplicate states only reachable from the initial state, andthe reachable state space of (dim, relax) always satisfies
x = y. Consequently, we have to add an invariant x = y to
the duplicated location (dim, relax′ ). Next, we duplicate
a transition eb , and the duplication of this transition is thatfrom (of f, idle) to (dim, relax′ ). Also, we duplicate transitions from (dim, relax) except that being unable from thestate space which satisfies x = y. In this example, we duplicate a transition from (dim, relax) to (of f, idle) (and the
duplicated transition from (dim, relax′ ) to (of f, idle) is
depicted in Fig.17), but we don’t duplicate a transition from(dim, relax) to (bright, idle) which is infeasible from B1 .
Finally, we remove a transition between (of f, idle) and(dim, relax). We can remove the transition because there
is a corresponding transition (of f, idle) to (dim, relax′ ).
Figure 15 represents the refinement guided by this counterexample. Finally, we produce a refined abstract model fromthe refined timed automaton.

NAGAOKA et al.: AN ABSTRACTION REFINEMENT TECHNIQUE FOR TIMED AUTOMATA BASED ON CEGAR LOOP

7

3.6

Fig. 16

Fig. 17

Second refinement

Timed automaton generated in the final loop

Related works

As related works, papers[11]–[13] have proposed CEGAR
based abstraction techniques for timed automata. In the approach of [11], they perform abstraction by removing all
clock variables from timed automata, and refine the abstract model by removing transitions which are always impossible. However, they can remove such transitions only
when it is guaranteed that such removal preserves underapproximation, otherwise they have to restore clock variables to the abstract models. The technique of [12] is basedon bounded model checking using SAT. In this approach,they refine propositions representing models using spurious
counter examples. The technique of [13] limits the modelto PLC automata, a sub class of timed automaton. Although these techniques mainly refine abstract models byadding clock variables which have been removed by abstraction, our refinement approach modifies transition relationsof models so that the abstract models partially contain realtime behavior. The refinement approach of adding clock
variables is more effective in that it can remove more spurious counter examples. Adding clock variables, however,may decrease the efficiency of abstraction. On the other
hand, because our approach does not add clock variables,
we expect our abstraction reduces more state space of themodel using traditional techniques on space reduction forordinal finite automata.
4.

Correctness Proof

As mentioned∨in Section 3, the proposed algorithm checks aproperty AG e∈E ¬e, where E (⊂ L) of a timed automaton
A is a set of error locations of the target system. In otherwords, we treat only reachability problem. As mentioned
in Section 3, any counter example of such a property canbe represented in a finite length of sequence without loops.
Therefore, we assume that counter examples are finite sequences without loops.
Paper [2] gives a theorem on a conservative class of abstractions which attempts to preserve semantics of automata
against state reductions under the condition that it checks
only a property AG p for a proposition p. From the theorem,
we can derive the following theorem.
Fig. 18

Abstract model generated in the final loop

After the refinement, we perform model checking again, and we obtain another counter example⟨(of f, idle), (dim, t), (of f, study), (dim, idle)⟩. For thiscounter example, Simulation decides it is spurious, and therefinement is performed in the same way. Figure 16 depicts
the second refinement.
The third time model checking proves that the modelsatisfies the property. The timed automaton and abstract
model generated in the final loop are presented in Fig17 andFig18 respectively.

Theorem 4.1. For a timed automaton A = (A, L, l0 , C, I, T )and a set E of error locations. Let the abstract modeland a set of error states of the abstract model be M̂ andÊ = {h(e) | e ∈ E}, respectively. The following statement
always holds.
∨∨
M̂ |= AG¬ê ⇒ A |= AG
¬e
(2)
ê∈Ê

e∈E

Proof. Let a concrete model and its abstract model abstracted by h be M and M̂ , respectively. For a proposition p,
if an abstraction function h satisfies the following for everys ∈ S:

IEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x

8

The sketch of proof is as follows. In the worst case,the states of abstract model are divided as fine as productof clock region and locations. They are both finite. One
time application of Refinement always divides state space.
Consequently, the loop terminates.
Theorem 4.2 (Correctness). If a counter example is spurious, at most n times repetition of Refinement in Fig.8 produces a spurious CE free model. CEGAR loop will terminate.

Fig. 19

Proof. From Lemma 4.1, Refinement preserves bi-simulationequivalence. From Lemma 4.2, at most n times repetition
of Refinement produces a refined spurious CE free model.
Lemma 4.3 shows loop’s termination.

Relations among models

h(s) |= p ⇒ s |= p(3)then M̂ |= AG p ⇒ M |= AG p holds from Theorem 1 inPaper [2].
∨Hereê∈Ê ¬ê for M̂ , and∨ we assume that p =p = e∈E ¬e for A . In addition, an abstraction function defined in Definition 3.2 maps each location in A toa state M̂ and the mapping is one-to-one mapping. Thus,∀l ∈ L. h(l ) = ê ⇐⇒ l = e holds. As a result, the abstraction function h satisfies the statement 3; Theorem 4.1
is proved.
Next, we prove the correctness of our abstraction technique; first, we prove the correctness of our refinement algorithms ‘duplicateState,’ ‘duplicateTransition,’ ‘removeTransition.’ Figure 19 represents the relations among the timed
automata generated by each algorithm. Second, we provethat repeating our refinement algorithm can remove a spurious counter example correctly.
Lemma 4.1 (Bi-simulation equivalence among timed automata). Let denote by Ai and Ai+1 a timed automaton before and after applying i + 1-th application of Refinement ,respectively. Ai is bi-simulation equivalent to Ai+1 .
Proof of Lemma 4.1 is given in Appendix.
For an abstract model M̂ and a spurious counter example on M̂ , we use the term ‘the spurious CE free model,’if the refined abstract model of M̂ doesn’t have the spurious
counter example (which may have potentially other spuriousCE’s).
Lemma 4.2. For the spurious CE and an abstract model M̂ ,at most n times repetition of Refinement produces the spurious CE free model, where n is the length of the spurious
counter example.
The proof of this lemma is given by showing inductively that for a sub-sequence starting from l0 to lk (1 ≤k ≤ n) of the spurious counter example, at most k times
application of the Refinement algorithm refines the abstract
model correctly with respect to the sub-sequence. The detailis given in [15].
Lemma 4.3 (Termination). The CEGAR loop terminates.

5.

Conclusion

This paper proposes a model abstraction technique for timed
automata based on the CEGAR algorithm. In general, most
CEGAR based algorithms obtain refined abstract models
from the previous abstract models by modifying some transformations. In our algorithm, however, the refined model
is obtained indirectly; we transform the original timed automaton preserving the equivalence and from it we generate
an abstract model by eliminating clock attributes.
This paper gives a formal description and correctness
proof of our algorithms.
As a preliminary experiment, we have applied our abstraction technique to some examples, including Gear Box
controller[14], and we have obtained the encouraging result
on memory consumption.
Future work contains applying subtraction operation[10] in order to divide a bad state into a reachable state
and unreachable one instead of duplicating it, during refinement of an abstract model. Comparison its efficiency withthe method proposed in this paper is also considered.
References[1] 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(5), pp752-794, 2003.
[2] E M. Clarke, A. Gupta, J. Kukula, and O. Strichman: “SAT based
Abstraction-Refinement using ILP and Machine Learning Techniques,” In Proc. of the 14th Int. Conf. on Computer Aided Verification, vol.2404, pp.695-709, 2002.
[3] E M. Clarke, A. Fehnker, Z. Han, J Ouaknine, O. Stursberg, and M.
Theobald: “Abstraction and Counterexample-guided Refinement inModel Checking of Hybrid Systems,” In Int. Journal of Foundationsof Computer Science, vol.14(4), 2003.
[4] R. Alur: “Techniques for Automatic Verification of Real-Time Systems,” PhD thesis, Stanford University, 1991.
[5] R. Alur, C. Courcoubetis, and D. L. Dill: “Model-checking for realtime systems,” In Proc. of the 5th Annual Symposium on Logic in
Computer Science, IEEE, pp.414-425, 1990.
[6] S. Das, D. L. Dill, and S.Park : “Experience with predicate abstraction,” In Proc. of the 11th Int. Conf. on Computer Aided Verification,
vol.1633, pp.160-171, 1999.

NAGAOKA et al.: AN ABSTRACTION REFINEMENT TECHNIQUE FOR TIMED AUTOMATA BASED ON CEGAR LOOP

9[7] J. Bengtsson, and W .Yi: “Timed Automata: Semantics, Algorithms
and Tools,” In Lectures on Concurrency and Petri Nets, vol.3098,
pp.87-124, 2004.
[8] F. Wang, K. Schmidt, G D. Huang, F. Yu, B Y. Wang: “Formal Verification of Timed Systems: A Survey and Perspective,” In Proc. of
the IEEE, vol.92, No.8, pp.1283-1307, 2004.
[9] G. Behrmann, A. David, and K G. Larsen: “A Tutorial on UPPAAL,” In Proc. of the 4th Int. School on Formal Methods forthe Design of Computer, Communication, and Software Systems,
vol.3185, pp.200-236, 2004[10] 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 ofTimed Systems, pp.128-142, 2006[11] H. Nakajima and Y. Kameyama: “Improvement on Real-Time
Model Checking using Abstraction-Refinement (In Japanese),” In
Transactions of Information Processing Society of Japan, vol.45,
No.SIG12 (PRO23), pp.11-24.
[12] S. Kemper, and A. Platzer: “SAT-based Abstraction Refinement forReal-time Systems,” In Proc. of the Third Int. Workshop on Formal
Aspects of Component Software, vol.182, pp.107-122, 2006.
[13] H. Dierks, S. Kupferschmid, and K G. Larsen: “Automatic Abstraction Refinement for Timed Automata,” In Proc. of the 5th Int. Conf.
on Formal Modelling and Analysis of Timed Systems, vol.4763,
pp.114-129, 2007.
[14] M. Lindahl, P. Pettersson, and W. Yi: “Formal Design and Analysis
of a Gear Controller,” In Proc. of the 4th International Workshop on
Tools and Algorithms for the Constraction and Analysis of Systems,
vol.1384, pp.281-297, 1998.
[15] T. Nagaoka, K. Okano, and S. Kusumoto: “Abstraction of Timed
Automata Based on Counterexample-Guided Abstraction Refinement Loop,” IEICE Technical Report, vol.107, No.505, pp.103-108,
2008.

Appendix: Proof of Lemma 4.1
Proof. For region Automata Ar = (A, Lr and lr 0 , Tr )and Ar′ = (A′ , L′r , lr′ 0 , Tr′ ), we define the following bisimulation relation ∼ recursively.
• For lr 1 ∈ Lr and lr′ 1 ∈ L′r , if there is a bi-simulation
relation lr 1 ∼ lr′ 1 , the following conditions are satisfied.
afor all a ∈ A and lr 1 ⇒ lr 2 ∈ Tr , there exists a transia ′′′tion lr 1 ⇒ lr 2 ∈ Tr such as lr 2 ∼ lr′ 2 holds, and fora
all a ∈ A and lr′ 1 ⇒ lr′ 2 ∈ Tr′ , there exists a transitionalr 1 ⇒ lr 2 ∈ Tr such as lr 2 ∼ lr′ 2 holds.
• For initial states, if lr 0 ∼ lr′ 0 holds, under the bisimulation relation ∼, Ar and Ar′ are bi-simulationequivalent.
Let denote by Ar i and Ar i+1 their region automaton for Ai and Ai+1 , respectively. In a similar way, Ai1 ,Ar1i , Ai2 , Ar2i , Ai3 (= Ai+1 ), Ar3i (= Ar i+1 ) are defined,
where the superfix means a sub algorithm of the Refinement.
Therefore the superfixes 1, 2, and 3 stand for after applying
Duplication of States, Duplication of Transitions, and Removal of Transition, respectively.
Here, we will prove that Ai is bi-simulation equivalent
to Ai+1 by proving bi-simulation equivalence over the eachpair of region automata (before and after applying each algorithm). For the state set B1 = (lb , D1), we denote theduplicate state set by B1′ = (l′ , D1 ).
Let Tr d and Tr r be a set of transitions to be added in
A , a set of transitions to be removed in A , that to be a setof transitions be added in Ar and that to be removed in Ar ,respectively.
i) Ar i and Ar1i
Ar i is obviously bi-simulation equivalent to Ar1i overthe bi-simulation relation ∼. We omit the proof of it.
ii) Ar1i and Ar2i
Let consider Ar i = (Lr i , lr i 0 , Tr i , Ai ), and Ar2i =2(Lr i , lr2 i 0 , Tr2 i , A2i ). Obviously, Tr2 i = Tr1 i ∪ Tr d holds.
Because Tr1 i ⊂ Tr2 i holds, for lr1 i ∈ L1r i and lr2 i ∈2
Lr i , such that a bi-simulation relation lr1 i ∼ lr2 i holds,athere exists a transition lr2 i ⇒ lr2′i ∈ Tr2 i where a relation
a 1′
1
1
lr i ⇒ lr i ∈ Tr i is satisfied for any a ∈ A1i . Consequently,
the bi-simulation relation lr1′i ∼ lr2′i also holds.
Let consider converse. For lr1 i ∈ L1r i and lr2 i ∈ L2r isuch that the bi-simulation relation lr1 i ∼ lr2 i holds, thereaexists some transitions such that lr2 i ⇒ lr2′i ∈ Tr2 i is satisfied. For such transitions, we consider the following cases.
a

1. The case lr2 i ⇒ lr2′i ∈ Tr1 i holds.
aIn this case, lr1 i ⇒ lr1′i ∈ Tr1 i exists, and the bisimulation relation lr1′i ∼ lr2′i holds.
a2. The case lr2 i ⇒ lr2′i ∈ Tr d holds. (a case in which thetransition is duplicated)
In this case, lr2 i or lr2′i is in duplicated state set B1′ =If lr2 i ∈ B1′ holds, as mentioned in Lemma 3.2,
there is a transition which is the source transition for duplication. Therefore, if lr2′i ∈/ B1′ holds, lr1′i ∼ lr2′i also holds.
2′′2′
If lr i ∈ B1 holds, lr i is a duplicate of lr1′i , and B1′ is finite. Consequently, from the definition of ∼, lr1′i ∼ lr2′i also
holds.
If lr2′i ∈ B1′ holds, as mentioned in Lemma 3.2, there
is a transition that is the source transition for duplication.
Therefore, lr2′i is a duplicate of lr1′i , and B1′ is finite. Consequently, from the definition of ∼, lr1′i ∼ lr2′i holds.
For initial states, lr1 i 0 ∼ lr2 i 0 also holds. Therefore,
there is the bi-simulation relation ∼ between Ar1i and Ar2i .
(lb′ , D1 ).

iii) Ar2i and Ar3i
Let consider Ar3i = (L3r i , lr3 i 0 , Tr3 i , A3i ). Obviously,3
Tr i = Tr1 i \ Tr r holds.
For lr2 i ∈ L2r i and lr3 i ∈ L3r i such that lr2 i ∼ lr3 iaholds, lr2 i ⇒ lr2′i ∈ Tr2 i holds for any a ∈ A2i . For such atransition, we consider the following cases.
a/ Tr r holds.
1. The case in which lr2 i ⇒ lr2′i ∈aaIn this case, lr2 i ⇒ lr2′i ∈ Tr3 i holds. Therefore, lr3 i ⇒
3′
3
2′
3′
lr i ∈ Tr i exists, and the bi-simulation relation lr i ∼ lr iholds.
a

2. The case in which lr2 i ⇒ lr2′i ∈ Tr r holds.

IEICE TRANS. INF. & SYST., VOL.Exx–??, NO.xx XXXX 200x

10

As mentioned in Lemma 3.3, because the transitions
to remove have corresponding duplications, there is a dua
aplication of lr2 i ⇒ lr2′i , such that lr3 i ⇒ lr3′i ∈ Tr3 i , and2′3′
lr i ∼ lr i holds.
Let consider converse, because Tr3 i ⊂ Tr2 i holds, fora
all a ∈ A2i such that lr2 i ⇒ lr2′i ∈ Tr2 i , there exists a trana
sition lr2 i ⇒ lr2′i ∈ Tr2 i . Consequently, the bi-simulation
relation lr2′i ∼ lr3′i holds.
For initial states, lr2 i 0 ∼ lr3 i 0 also holds. Therefore,
there is the bi-simulation relation ∼ between Ar2i and Ar3i .
From the facts i), ii) and iii), we can conclude that Ar i
and Ar i+1 are bi-simulation equivalent, and also Ai andAi+1 are.

Takeshi Nagaoka
received the M.I. degreein Computer Science from Osaka University in2007. He currently belongs in a doctoral course.
His research interests include abstraction techniques in model checking, especially timed automaton.

Kozo Okano
received the BE, ME, and Ph.D
degrees in Information and Computer Sciencesfrom Osaka University, in 1990, 1992, and 1995,
respectively. Since 2002 he has been an associate professor in the Graduate School of Information Science and Technology, Osaka University. In 2002, he was a visiting researcher of the
Department of Computer Science, University of
Kent at Canterbury. In 2003, he was a visiting
lecturer at the School of Computer Science, University of Birmingham. His current research interests include formal methods for software and information system design.
He is a member of IEEE, IEICE of Japan and IPS of Japan.

Shinji Kusumotoreceived the BE, ME, andDE degrees in information and computer sciences from Osaka University in 1988, 1990, and1993, respectively. He is currently a professor in
the Graduate School of Information Science andTechnology at Osaka University. His researchinterests include software metrics and software
quality assurance technique. He is a member of
the IEEE, the IEEE Computer Society, IPSJ, IEICE, and JFPUG.