社団法人 電子情報通信学会
THE INSTITUTE OF ELECTRONICS,
INFORMATION AND COMMUNICATION ENGINEERS

信学技報
TECHNICAL REPORT OF IEICE.

反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
長岡 武志†

岡野

浩三†

楠本

真二†

† 大阪大学大学院情報科学研究科〒 560–8531 大阪府豊中市待兼山 1–3
あらまし時間オートマトンを対象としたモデル抽象化手法を著者らは提案している．提案手法では，反例を元に抽象モデルを改良し，適切な抽象モデルを自動的に生成する CEGAR (CounterExample-Guided Abstraction Refinement)
ループに基づく．抽象モデルの改良の際，元になる時間オートマトンの変形で行うなどの特徴を持つ．本稿では，提案手法の具体的なアルゴリズムを形式的に記述し，アルゴリズムの正当性の証明を与える．
キーワード

モデル検査，時間オートマトン，モデル抽象化，CEGAR

Abstraction of Timed Automata Based on Counterexample-Guided Abstraction
Refinement Loop
Takeshi NAGAOKA† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Information Science and Technology, Osaka University
Machikane-yama 1–3, Toyonaka City, Osaka, 560–8531 Japan
Abstract We have proposed a method of model abstraction for timed automata. The proposed method is based on CEGAR(CounterExample-Guided Abstraction Refinement) loop which automatically refines an abstract model using counter examples. Our algorithm has some features such as refinements are performed indirectly through transformation of the original
timed automaton. This paper gives formal descriptions of the algorithm and the correctness proof of the algorithm.
Key words Model Checking, Timed Automaton, Model Abstraction, CEGAR

1. Introduction

free.
The rest of the paper is organized as follows. In Sec. 2., someThis paper gives correctness proof of our algorithm proposed

definitions are described. Sec. 3. gives our CEGAR algorithm. Sec.

in [8]. The algorithm is CEGAR [1] based algorithm of abstract

4. proves the correctness of the algorithm. Sec. 5. concludes themodel refinement used for model checking on timed automata.

paper.

A general CEGAR algorithm consists of several steps. First, it
abstracts the original model (the obtained model is called abstract

2. Preliminaries

model) and performs model checking on the abstract model. Next,

In this Section, we give definitions of a timed automaton, a region

if a counter example (CE) is found, it checks the counter example

automaton which specifies whole states of a timed automaton withon the concrete model. If the CE is spurious, it refines the abstract

finite clock regions, and others.

model. The last step is repeated until the valid output is obtained.
In general, most CEGAR based algorithms [1], [2] 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 proves that the transformation preserves bi-simulationequivalence and also the refined abstract model is the spurious CE

Let c(C) be a set of whole differential inequalities of 2 clocks
over a finite clock set C. A subset of c(C) is called clock constraints.
Definition 2.1 (Timed Automaton). A timed automaton A is a 6tuple (L, l0 , T, I, C, A), whereC : a finite set of clocks; A : a finite set of actions; L : a finite set of
locations; l0 ∈ L :an initial location; T ⊂ L × A × 2c(C) × R × L;
where, 2c(C) is a set of clock constraints, called guards; R = 2C—1—

: a set of clocks to reset; and I ⊂ (L → 2c(C) ) : a mapping fromlocations to clock constraints, called location invariants.
a,g,r

A transition t = (l1 , a, g, r, l2 ) ∈ T is denoted by l1 −→ l2 .
A map ν : C → R>
is called a clock assignment. We can ex=0
tend the domain of ν into a set of C as follows: ν ∈ RC
. We define>=0(ν + d)(x) = ν(x) + d for d ∈ R>
. r(ν) = ν[x 7→ 0], x ∈ r is=0
also defined for r ∈ 2C . By N , a set of whole ν is denoted.
Definition 2.2 (Semantics of Timed Automaton). For a given timed
automaton A = (L, l0 , T, I, C, A), let a set of whole states of A

Figure 1 General CEGAR Algorithm

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 aresemantically defined. The first one is called an action transition,
while the latter one is called a delay transition.
0∀d0 <= d I(l1 )(ν + d )a,g,rl1 −→ l2 , g(ν), I(l2 )(r(ν))
a,d(l1 , ν) ⇒ (l2 , r(ν))(l1 , ν) ⇒ (l1 , ν + d)
For a given timed automaton A , we can introduce a correspond-

ing clock region CR(A ) [4], [5]. In general, a clock region divides a |C|-dimensional Euclidean space into finite points, segments, and faces. By [u], an element (a region) in CR(A ) is de-Figure 2 Our Proposed Algorithm

noted. For [u] ∈ CR(A ), g([u]) and I([u]) represent that any
point in [u] satisfies a guard g and invariant I, respectively. Alsoby r([u]), applying clock resetting r onto [u] is denoted, wherer([u]) = [u][x 7→ 0], and x ∈ r.

3. Algorithm
3. 1 General CEGAR Algorithm

Definition 2.3 (Region Automaton). A region automaton Ar =Model abstraction sometimes over-approximates an original(Lr , lr 0 , Tr , A) of a given timed automaton A = (L, l0 , T, I, C, A)

model, which causes spurious counter examples which are not actu-

is defined as follows.

ally counter examples in the original model. Paper [1] gives an algo-

Lr ⊂ L × CR(A ), lr 0 = (l0 , [0 ]), where [0 ] satisfies I(l0 ),rithm called CEGAR (Counterexample-Guided Abstraction Refine-Tr ⊂ Lr × A × Lr , Tr consists ofment). In the algorithm, at the first step (called Initial Abstraction),

C

•

a

0

C

0

d

(l , [u]) ⇒ (l , [v]) if (l , u) ⇒ (l , u ) for d ∈ R>
∧
=0
0

a

0

(l , u ) ⇒ (l , v) for a ∈ A.

it approximates the original model, and the next step, if a spurious
counter example is found in the abstract model, it refines the abstract model as it does not admit the spurious counter example. The

There is a bi-simulation equivalence between a timed automaton
A and its region automaton Ar [3].
In [6], [7], a data structure DBM (Difference Bound Matrix) is introduced to represent a convex space in |C| -dimensional Euclidean
space, where C is a set of clock variables. It is also represented asa set of some elements in the clock region CR(A ). A state set ofstates of a region automaton Ar = (Lr , lr 0 , Tr , A), can be represented in (l , D) = {(l , [u]) | [u] ∈ D} using the corresponding
DBM D. Paper [6] gives operation functions on DBM, such as up,

next step is repeated until valid output is obtained. Figure 1 shows
the general flow of the CEGAR algorithm.
3. 2 Our Proposed Algorithm
Our proposed algorithm generates an abstract model M̂ from agiven timed automaton A by applying an abstraction function h,and performs model checking on M̂ . If a counter example T̂ (represented as a path on the abstract model) is found while model
checking, it concretizes T̂ by applying inverse function h−1 .The
concretized one is a set of paths. We denote it by T (which is a set

and and other functions, which represent elapsing time, intersec-

of paths on A ). At Simulation Step, it checks whether each pathtion of time spaces and so on, respectively. There is a minimum set

in T is feasible on A or not. If every path in T is infeasible, theof differential inequalities which can represents DBM D [6]. Sucha set is denoted by c(D). c(D) can be obtained by reduction operations on DBM. A set of every region which satisfies an invariantI(l ) of location l is denoted by (l , DInv ).

next step shall refine the model so that the counter example T̂ becomes infeasible. Our algorithm does not directly refine M̂ but it
refines A and then obtains a new abstract mode by applying h to
the refined timed automaton. Figure 2 shows flow of our CEGAR
algorithm.
—2—

The proposed algorithm checks a property AG

We∈E ¬e, whereE (⊂ L) of a timed automaton A is a set of error locations of thetarget system. The property means there is no path to locations in E
from the initial state. Please note that any counter example of sucha property can be represented in a finite length of sequence without

Abstraction
Inputs A , h{h = abstraction function}Ŝ := ∅, →
ˆ := ∅ {M̂ = (Ŝ, ŝ0 , →)}ˆ
foreach l ∈ L do
Ŝ := Ŝ ∪ {h(l)}loops. Therefore, hereafter, we assume that counter examples areend forfinite sequences without loops.

ŝ0 := h(l0 )foreach (l1 , a, g, r, l2 ) ∈ T do

3. 2. 1 Abstract Model
Definition 3.1 defines the abstraction function h on Lr of a region→:=→ ∪{(h(l1 ), h(l2 ))}end forautomaton Ar .

return M̂

Definition 3.1 (Abstraction Function h). For a region automaton
Ar = (Lr , lr 0 , Tr , A) of a given timed automaton A , an abstraction function h : Lr → Ŝ is defined as follows:•

Figure 3 Abstraction
Simulation
a ,g ,ra ,g ,r

1 1
2 2
Inputs A , (l0 1−→
l1 2−→···
C
R0 := (l0 , D0 ) {D0 = {0 }}∀lr i , lr j ∈ Lr . h(lr i ) = h(lr j )⇐⇒ Loc(lr i ) = Loc(lr j ),an ,gn ,rn−→

D := up(D0 ) {Any elapsing time}

where Loc : Lr → L is a function which retrieves a location at-

D := and(D, I(l0 )) {Add Invariant of l0 }tribute from a state of Ar . The inverse function h−1 : Ŝ → 2Lr offor i := 1 to n do
Ri :=Reach(A , Ri−1 , (li−1 , ai , gi , ri , li ))h is also defined as in a usual manner.

if Ri = ∅ thenThe abstraction function h defined in Definition 3.1 maps any

return false

state of Lr which belongs to the same location into the same ab-

end ifstract state. Otherwise they are mapped into the different states.

end forThis means that there is a one-to-one correspondence between the

return true
Figure 4 Simulation

location set of A and the abstract state set Ŝ. Therefore, the abstraction function h can be extended its domain as in Definition 3.2.

Reach

Definition 3.2 (Extension of Abstraction Function h). Abstraction

Inputs A , R = (l, D), (l1 , a, g, r, l2 )D := and(D, g) {add guards of transitions}function h : L → Ŝ of a timed automaton A = (L, l0 , T, I, C, A)
is defined as follows:•ln (ln = e))

D := reset(D, r) {reset the clocks}
D := and(D, I(l2 )) {add Invariant of l2 }

∀li , lj ∈ L. h(li ) = h(lj ) ⇐⇒ li = lj .

D := up(D) {Any elapsing time}

Similarly, the inverse function h−1 : Ŝ → L of h is also defined.

D := and(D, I(l2 )) {add Invariant of l2 }Definition 3.3 gives an abstract model M̂ of a given timed au-

return (l2 , D)
Figure 5 Reach

tomaton A using the abstraction function h defined in Definition
3.2.

3. 2. 2 Initial Abstraction

Definition 3.3 (Abstract Model). An abstract model M̂

=Initial Abstraction generates an abstract model M̂ from a timed(Ŝ, ŝ0 , →)
ˆ of a given timed automaton A = (L, l0 , T, I, C, A) us-

automaton A = (L, l0 , T, I, C, A) using the abstraction function

ing the abstraction function h defined in Definition 3.2 is defined ash. Figure 3 shows the algorithm of Initial Abstraction.

follows:

3. 2. 3 Simulation•Ŝ = {h(l ) | l ∈ L)},•sˆ0 = h(l0 ),→ˆ = {(lˆ1 , a, lˆ2 ) | (l1 , a, g, r, l2 ) ∈ T }.

•For a set T of concretized counter example sequences obtained
from T̂ on M̂ , Simulation performs the algorithm in Fig. 4 on eachsequence t ∈ T . Reachability from the first location of t to the last

Definition 3.4 (Counter Example). A counter example on M̂ is alocation of t is checked in Simulation using a procedure Reach insequence of states of Ŝ. A counter example T̂ of length n is repre-

Fig. 5. Reach uses some operation functions of DBM. When thesented in T̂ = hŝ0 , · · · , ŝn i.

algorithm in Fig. 4 returns false, the counter example T̂ is judged

A set T of a run sequences on A obtained by concertizing acounter example T̂ = hŝ0 , · · · , ŝn i, is defined as follows:
T = {(l0a1 ,g1 ,r1−→ l1

a2 ,g2 ,r2−→ · · ·an ,gn ,rn

−→

ln )|

as a spurious counter example.
3. 2. 4 Refinement of Abstract ModelIn this step, we have to generate a refined abstract model which
does not admit the spurious counter example (we call it the spurious( li = h−1 (si ) for 0 <
=i<
=n) ∧

CE free model for a given CE). When a counter example is judged( (li−1 , ai , gi , ri , li ) ∈ T for 1 <=i<= n )}.

as a spurious counter example, there is a Bad State l̂b which has—3—DuplicateState
Input A , B1 = (lb , D1 )lb0 := newLoc() {Generate a new location lb0 }L := L ∪ {lb0 }I( lb0 ) := c(Db ) {A set of inequalities representing Db }Figure 9 Duplication 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, lb0 )}Figure 6 Counter Example{Duplicate a transition eb to a BadState}
foreach (l1 , a0 , g 0 , r 0 , l2 ) ∈ T such that l1 = lb do
if Reach( A , (lb , Db ), (l1 , a0 , g 0 , r 0 , l2 )) 6= ∅ thenT := T ∪ {(lb0 , a0 , g 0 , r 0 , l2 )}{duplicate transitions from lb only enable from ((lb0 , Db ).)}
end ifend forFigure 10 Duplication 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 }Figure 7 Refined Model

R :=Reach(A , P rev, eb ) {obtain regions of lb reachable from P rev}
if relation(R, B1 ) = htrue, truei thenRefinement
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 , B) {Duplication of States}{when R = B, relation(R, B1 ) returns h true, truei.}
T := T \ {(l, a, g, r, lb )}end ifFigure 11 Removal of Transitions

Ai+1 := DuplicateTransition(Ai+1 , B, eb ){Duplication of Transitions}
Ai+1 := RemoveTransition(Ai+1 , B) {Removal of Transitions}M̂i+1 :=Abstraction(Ai+1 , h)return M̂i+1

Here, we gives definitions of states to duplicate, transitions to duplicate, and transitions to remove.
Definition 3.5 (States to Duplicate). Let B1 = (lb , D1 ) and dupli-

Figure 8 Refinement

cation of a location lb be lb0 . A set of states to duplicate, of a region
automaton is defined as (lb0 , D1 ).

a corresponding state set B1 = (lb , D1 ) reachable from the initialstate but unreachable to lnext , and another state set B2 = (lb , D2 )unreachable from the initial state but reachable to lnext , are merged(mapped into the same state) as in Fig. 6.

Duplication of transition duplicates the following kinds of transitions: “transitions from lprev to lb ,” and “ transitions not only fromlb but also enable from (lb , D1 ).”In general, refinement algorithm should divide state l̂b into more

Definition 3.6 (Transitions to Duplicate). For a region automaton

than two states as state B1 and state B2 are mapped into differential

Ar = (Lr , lr 0 , Tr , A), B1 = (lb , D1 ), states to duplicate (lb0 , D1 ),states. Dividing of a state space of a timed automaton usually needs

and a previous location lprev of a location lb in a counter example,

Subtraction operation of DBM. However, DBM is not closed undertransitions to duplicate of a region automaton is defined as follows:

Subtract operation [7], so applying such an approach is difficult.

Tr d = {(lprev , [v]) ⇒ (lb0 , [v 0 ]) |∀(lprev , [v]) ∈ (lprev , DInv ).
a

We proposes another approach, in which it duplicates state B1∀(lb , [v 0 ]) ∈ (lb , D1 ).(lprev , [v]) ⇒ (lb , [v 0 ]) ∈ Tr } ∪ {(lb0 , [v]) ⇒in the concrete model and also performs other transformation on(l , [v 0 ]) | ∀(lb , [v]) ∈ (lb , D1 ). ∀(l , [v 0 ]) ∈ Lr . (lb , [v]) ⇒the concrete model. Applying the abstraction function to the trans-(l , [v 0 ]) ∈ Tr }.

a

a

a

formed concrete model produces a new refinement abstract model
where a state mapped from B2 is unreachable (refer in Fig. 7).
The algorithm of Refinement in Fig. 8 consists of three sub algorithms, called duplication of states, duplication of transitions, andremoval of transitions, shown in Fig.9, 10, and 11, respectively.

Definition 3.7 (Transitions to Remove). For a region automaton
Ar = (Lr , lr 0 , Tr , A), B1 = (lb , Dd ), states to duplicate (lb0 , D1 ),and a previous location lprev of a location in a counter example,
transitions to remove of a region automaton is defined as follows:
Tr r = {(lprev , [v]) ⇒ (lb , [v 0 ]) |∀(lprev , [v]) ∈ (lprev , DInv ).
a—4—Lemma 4.1 (Bi-simulation equivalence among timed automata).
Let denote by Ai and Ai+1 a timed automaton before applying i+1th application of Refinement and one after applying i + 1-th application of Refinement, respectively. Ai is bi-simulation equivalent to
Ai+1 .
Proof. 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, Duplica-

Figure 12 Relations among models

tion of Transitions, and Removal of Transition, respectively.
We will prove that Ai is bi-simulation equivalent to Ai+1 by(lprev , [v]) ⇒ (lb , [v 0 ]) ∈ Tr }.
aproving bi-simulation equivalence over the corresponding region

The algorithm of Removal of Transitions removes transitions

automata. For lb , let lb0 be a duplicated state. For a set D1 of regions

only when a set of states reachable from lprev is the same as awhich associates to a location to duplicate, a set of states in Ar willaset (lb , D1 ) of Bad States. Therefore, for every (lprev , [v]) ⇒be (lb , D1 )，and (lb0 , D1 ). Let Tr d and Tr r be a set of transitions(lb , [v 0 ]) ∈ Tr r , (lb , [v 0 ]) ∈ (lb , D1 ) holds. It means that every

be added in Ar and that to be removed in Ar , respectively.

transition in Tr r has its duplication in Tr d .

i) Ar i and Ar1i
Let’s consider Ar i

4. Correctness Proof= (Lr i , lr i 0 , Tr i , Ai ) and Ar1i=

(L1r i , lr1 i 0 , Tr1 i , A1i ). From the assumption, lr i 0 = lr1 i 0 ，Tr i =As mentioned in Section3., the proposed algorithm checks a propW
erty AG e∈E ¬e, where E (⊂ L) of a timed automaton A is a set

Tr1 i ，Ai = A1i and L1r i = Lr i ∪ (lb0 , D1 ) hold.

of error locations of the target system.

transition to the duplicated state set (lb0 , D1 ) in Ar1i . Thus, there isPaper [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 forii) Ar1i and Ar2i
For Ar2i = (L2r i , lr2 i 0 , Tr2 i , A2i ), obviously L2r i = L1r i andWe show that for every [v] ∈ D1 , a state (lb , [v]) and a state

From the theorem, we can derive the following theorem.
Theorem 4.1. For a timed automaton A and a set E of error locations. Let the abstract model and a set of error states of the abstract
model be M̂ and Ê = {h(e) | e ∈ E}, respectively. The following
statement always holds.

(lb0 , [v]) have a bi-simulation equivalence relation. When there exa
ists a transition (lb , [v]) ⇒ (l , [v 0 ]) , as defined in definition 3.6, thecorresponding transition (lb0 , [v]) ⇒ (l , [v 0 ]) is generated. Also,
when there exists a transition (lb0 , [v]) ⇒ (l , [v 0 ]), there must be anaoriginal transition (lb , [v]) ⇒ (l , [v 0 ]). Thus, we proved the firsta_¬ê ⇒ A |= AG

ê∈Ê

_

¬e

(1)

h be M and M̂ , respectively. For a proposition p, if an abstraction
function h satisfies the following for every s ∈ S:
h(s) |= p ⇒ s |= pgoal.
Thus, the concrete bi-simulation equivalence relation ∼ betweene∈E

Proof. Let a concrete model and its abstract model abstracted by

lr1 i ∈ L1r i and lr2 i ∈ L2r i is defined as follows:
lr1 i ∼ lr2 i⇐⇒ lr1 i = lr2 i or
lr2 i is duplication of lr1 i(2)then M̂ |= AG p ⇒ M |= AG p holds from Theorem 1 in Paper [2].
W
W
Here we assume that p = ê∈Ê ¬ê for M̂ , and p = e∈E ¬e
for A . In addition, an abstraction function defined in Definition 3.2
maps each location in A to a state M̂ and the mapping is one-toone mapping. Thus, h(l ) = ê ⇐⇒ l = e holds. As a result,the abstraction function h satisfies the statement 2; Theorem 4.1 isproved.

bi-simulation equivalence between Ar i and Ar1i .

lr2 i 0 = lr1 i 0 ，A2i = A1i hold. Tr2 i = Tr1 i ∪ Tr d also holds.

a proposition p.

M̂ |= AG

The initial statelr i 0 = lr1 i 0 ，and Tr i = Tr1 i . So, there is no(3)

For the initial states, lr1 i 0 ∼ lr2 i 0 holds. A transition set Tr1 i satisfies Tr1 i ⊂ Tr2 i . For each transition in Tr1 i , thus, there is a correa

sponding transition in Tr2 i . Suppose that lr1 i ∼ lr2 i and lr1 i ⇒ lr10i .
aThen there exists a transition lr2 i ⇒ lr20i and lr10i ∼ lr20i . Let consider
converse. For each transition in Tr2 i , there is the corresponding transition in Tr1 i . Please note that for a transition in Tr d , there existsathe original transition. Suppose that lr1 i ∼ lr2 i and lr2 i ⇒ l 20 . Thenathere exists a transition lr1 i ⇒ lr10i and lr10i ∼ lr20i .
Therefore, Ar1i and Ar2i are bi-simulation equivalent.
iii) Ar2i and Ar3i
—5—

Let’s consider Ar3i = (L3r i , lr3 i 0 , Tr3 i , A3i ). Obviously L3r i =cannot be removed because U Rk is reachable from (lk−1 , DInv ).

= Tr1 i \ Tr r also

In such a case, from the inductive assumption, we can obtain the

L2r i , lr3 i 0= lr2 i 0 and A3i= A2i hold.

Tr3 irefined abstract model, in which an abstract state corresponding toholds.
The case when the algorithm in Fig. 11 does not perform any re-0
Rk−1 is reachable but U Rk−1 is not. Let lk−1
and lk0 be dupli-

moval of transitions is trivial. Ar2i is equivalent to Ar3i , thus alsocated locations of Rk−1 in k − 1-th time-Refinement and Rk in

holds the relation ∼.

0
k-th time-Refinement, respectively. Adding transition from lk−1
toOtherwise, in other words, in the case of removal of a transition, from Definition 3.7, each element in Tr r has its duplication in
Tr d . Thus, even if the transition is removed, ∼ is also preserved
between (lprev , [v]) ∈(lprev , DInv ) of Ar2i

lk0 improves the model so that it is reachable to only a state corresponding to Rk .
From (i) and (ii), statement (*) is proved.

and (lprev , [v]) ∈If the counter example is spurious, it is unreachable from Rn−1

(lprev , DInv ) of Ar3i . Thus each state of L2r i and that of L3r i sat-to error state (ln , DInv ) in M . Similarly, in M̂ , it is unreachable
from sˆ0 n−1 toŝn . Thus the lemma is proved.

isfy the relation defined in (3). In a similar way of case ii), Ar2i andAr3i are bi-simulation equivalent.
From the facts i), ii) and iii), we can conclude that Ar i and Ar i
are bi-simulation equivalent.

Theorem 4.2 (Correctness). If a counter example is spurious, at
most n times repetition of Refinement in Fig. 8 yields a spurious CE
free model.

Lemma 4.2. At most n times repetition of Refinement yields the
spurious CE free model, where n is the length of the spurious
counter example.

Proof. From Lemma 4.1, Refinement preserves bi-simulationequivalence. From Lemma 4.2, at most n times repetition of Refinement yields a refined spurious CE free model.

Proof. Let A , Ar and M̂ be a timed automaton, its region automaton and its abstract model, respectively. For a counter exampleT̂ = hŝ0 , ŝ1 , · · · , ŝn i, where ŝn is an abstract state obtained by
reducing the error location, let consider one of the corresponding
sequences t = (l0a1 ,g1 ,r1−→

l1

a2 ,g2 ,r2

−→

···

an ,gn ,rn−→ln ) to T̂ on

A , where ln is error location. Let Ri be a set of reachable i-thstates along with the sequence t, and U Ri be that of unreachable(= (li , DInv ) \ Ri ).
We prove that “for sub-sequence starting from l0 to lk (1 <=k<=n) of t, by applying at most k times repetition of Refinement yields
that it is reachable to an abstract state corresponding to Rk but unreachable to an abstract state corresponding to U Rk .”(*)

Let duplicated location from Ri be li0 . Let the abstract state of li0
be sˆ0 ( = h(li0 )).
ii) k = 1
R0 = (l0 , DInv ) holds. A set of reachable states from (l0 , DInv )through a transition (l0 , a1 , g1 , r1 , l1 ) is in fact R1 from the definition of Ri . Therefore, Refinement duplicates R1 , which is a location l10 and Refinement also removes a transition from l0 to l1 . In theobtained abstract model, it is reachable to only sˆ0 corresponding to
1

R1 , and it is unreachable to a state h(l1 ) corresponding to U R1 .
ii) k >
=2
As inductive assumption, we assume that at most k − 1 times repetition of Refinement yields that it is reachable to an abstract statecorresponding to Rk−1 but unreachable to an abstract state corresponding to U Rk−1 .
Let Rk0 (⊃=Rk ) be a set of reachable states from (lk−1 , DInv ). If

Rk = Rk0 , then in a similar way as k = 1, applying one more
Refinement leads to the goal.
Let consider when Rk ⊂ Rk0 holds. A transition from lk−1 to lk

5. Conclusion
This paper gives a formal description and correctness proof of our
proposed CEGAR algorithm in [8].
The future work will be extension of our algorithm to handle integer variables used in UPPAAL timed automata.
Acknowledgment
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.

References[1] E M. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut:“Counterexample-guided Abstraction Refinement,” In Proc. of the
12th Int. Conf. on Computer Aided Verification, vol.1855, pp.154169, July, 2000.
[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, July, 2002.
[3] E M. Clarke, O. Grumberg, D A. Peled: “Model Checking,” MIT
Press, 2000.
[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, pp.414-425, IEEE Computer Society Press, 1990.
[6] J. Bengtsson, and W .Yi: “Timed Automata: Semantics, Algorithms
and Tools,” In Lectures on Concurrency and Petri Nets, vol.3098,
pp.87-124, 2004.
[7] 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, 2002
[8] T. Nagaoka, K. Okano, and S. Kusumoto: “Abstraction of Extended
Timed Automata for UPPAAL Based on Counterexample-Guided
Abstraction Refinement Loop (in Japanese),” IEICE Technical Report, Vol.107，No.176，pp.77-82，2007.

—6—