Master Thesis

Title

Model Abstraction of Timed Automata Based on
Counterexample-Guided Abstraction Refinement Loop

Supervisor
Prof. Shinji KUSUMOTO

byTakeshi NAGAOKA

February 8, 2008

Department of Computer Science
Graduate School of Information Science and Technology
Osaka University

Master Thesis

Model Abstraction of Timed Automata Based on Counterexample-Guided Abstraction
Refinement Loop
Takeshi NAGAOKA

Abstract
Recently, for high-reliable information systems, it is strongly desirable to use model
checking techniques. Well-known state explosion, however, might occur in model checking of large systems. In particular, in model checking of the real time systems, the numberof states of models increases exponentially with the number of clock variables. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques are proposed. Some of them are based on CounterExample-Guided
Abstraction Refinement (CEGAR) loop technique suggested by E. Clarke et al..
The paper proposes a concrete abstraction technique for timed automata used in model
checking of real time systems, and evaluates its efficiency. The proposed technique isalso based on CEGAR, in which we use a counter example as a guide to refine the model
which is abstracted excessively. Although, in general, the refinement operation is applied
to abstract models, the method modifies the original timed automata, and next generates
refined abstract models from the modified automata.
Experimental results show the abstraction algorithm can reduce the total memory consumption by at most 80 percent compared to applying model checking without abstraction.

Keywords
Model Checking, Timed Automaton, Model Abstraction, CEGAR

Contents
1 Introduction

1

2 Preliminaries

3

2.1

Timed Automaton . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

2.2

Region Automaton . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

2.3

DBM (Difference Bound Matrix) . . . . . . . . . . . . . . . . . . . . . .

5

2.4

General CEGAR Algorithm . . . . . . . . . . . . . . . . . . . . . . . .

5

3 Proposing CEGAR Algorithm

7

3.1

Abstract Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8

3.2

Initial Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

3.3

Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

3.4

Refinement of Abstract Model . . . . . . . . . . . . . . . . . . . . . . .

11

3.5

Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

14

4 Correctness Proof

20

5 A tool based on the algorithm

25

6 Experimental Results

26

6.1

Aims of Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

6.2

Results of Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

6.2.1

Fischer’s mutual execution protocol . . . . . . . . . . . . . . . .

26

6.2.2

Gearbox Controller . . . . . . . . . . . . . . . . . . . . . . . . .

27

6.3

Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

27

6.4

Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

7 Conclusion

30

Acknowledgements

31

References

32iList of Figures
1

General CEGAR Algorithm . . . . . . . . . . . . . . . . . . . . . . . .

6

2

Our Proposed Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . .

7

3

Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

94

Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10

5Reach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10

6Counter Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12

7

Refined Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

128

Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

9Duplication of States . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

10Duplication of Transitions . . . . . . . . . . . . . . . . . . . . . . . . .

13

11

Removal of Transitions . . . . . . . . . . . . . . . . . . . . . . . . . . .

14

12Light Switch model . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

16

13

Parallel composed model . . . . . . . . . . . . . . . . . . . . . . . . . .

16

14

Initial abstract model . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17

15First refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17

16

Second refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

18

17

Timed automaton generated in the final loop . . . . . . . . . . . . . . . .

18

18

Abstract model generated in the final loop . . . . . . . . . . . . . . . . .

19

19

Relations among models . . . . . . . . . . . . . . . . . . . . . . . . . .

21ii

List of Tables
1

Result of Fischer’s mutual execution protocol . . . . . . . . . . . . . . .

27

2

Result of Gear Box Controller . . . . . . . . . . . . . . . . . . . . . . .

28

iii

1 Introduction
In recent years, there is more and more demand for applying model checking to designof dependable systems. Model checking proves that a given system satisfies specifications
by searching a finite transition system exhaustively which describes the system’s whole
behavior. There is, however, a limitation in scalability including a state explosion. In
order to improve the scalability, model abstraction technique becomes important[1, 2, 3].
In verification of real time systems, a timed automaton is used[8, 9], which can describe real time behavior of system . For a timed automaton, real-valued clock constraints
are assigned to a state of finite automaton (called location). Therefore, it has an infinite
state space which is represented in a product of discrete state space made by locations
and continuous state space made by clock variables. In traditional model 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 apply model checking to a finite model. However, thesize of the finite model increases exponentially with clock variables; thus an abstraction
technique is needed.
Paper[1] proposed a well-organized abstraction algorithm called CEGAR (Counter
Example-Guided Abstraction Refinement). The algorithm is used for abstraction of finite
models[1, 2], hybrid systems[3], timed automata[14, 15], and other models. In the CEGAR algorithm, we use a counter example produced by a model checker as a guide torefine models which is abstracted excessively. A General CEGAR algorithm consists ofseveral steps. First, it abstracts the original model (the obtained model is called abstract
model) and performs model checking on the abstract model. Next, if a counter 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.
This paper proposes a model abstraction technique for timed automata based on the
CEGAR algorithm. In general, most CEGAR based algorithms[1, 2, 3, 14, 15] obtainrefined 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.
In this paper, we give formal descriptions of our algorithms. Also we prove correctness of our algorithms by proving that the transformation preserves bi-simulation equiva-

1

lence and that the refined abstract model is the spurious CE free.
As related works, papers[14, 15] proposed CEGAR based abstraction techniques fortimed automata. The technique of [14] intends SAT based model checking, and refines
propositions which represent models to remove a spurious counter example. The technique of [15] limits the model to PLC automata, a sub class of timed automaton. Althoughthese techniques mainly refine the abstract models by adding clock variables which haveremoved by abstraction, our refinement method modifies the original timed automata andproduces the spurious CE free model from the modified 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. Sec. 4 proves the correctness of the algorithm. Sec.
6 gives experimental results. Sec. 7 concludes the paper.

2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 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 the same as the ordinal inequality.

Definition 2.2 (Clock constraints on C). Clock constraints c(C) on a finite set C of clocks
is defined as follows:
A differential inequality in on C is a element of c(C).
Let in1 and in2 be elements of c(C), in1 ∧ in2 is also a element 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;
T ⊂ 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,g,r

A transition t = (l1 , a, g, r, l2 ) ∈ T is denoted by l1 −→ l2 .
A map ν : C → R≥0 is called a clock assignment. We 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 for r ∈ 2C . By N , a set of whole ν is denoted.
3

Definition 2.4 (Semantics of Timed Automaton). For a given timed automaton A =(A, L, l0 , C, I, T ), let a set of 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(ν)),∀d0 ≤ d I(l1 )(ν + d0 )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 isdenoted.
2.2 Region Automaton
For a given timed automaton A , we can introduce a corresponding clock region
CR(A )[5, 6]. 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 denoted.
For [u] ∈ CR(A ), g([u]) and I([u]) represent that any point in [u] satisfies a guard g andinvariant 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 0 , [v]) iff (l , u) ⇒ (l , u0 ) ∈ T (A ) for d ∈ R≥0ad∧(l , u0 ) ⇒ (l 0 , v) ∈ T (A ) for a ∈ A
a∧ u ∈ [u] ∧ v ∈ [v].
There is bi-simulation equivalence between a timed automaton A and its region automaton Ar [4].
4

2.3 DBM (Difference Bound Matrix)
In [9, 13], a data structure DBM is introduced to represent a convex space in |C|-dimensional Euclidean space, where C is a set of clock variables. DBM is a set ofdifferential inequalities on two clock variables, and represents a state space which satisfies
all inequalities over it (the state space is called a zone). DBM represents these set of
inequalities as a |C0 | × |C0 | matrix, where C0 = C ∪ { 0 }, and 0 is a special variablewhich means a constant value 0. A (i, j)-th entry (Di j ) of the matrix means a differential
inequality of xi − xj for xi , xj ∈ C0 . Suppose there is an inequality xi − xj ¹ n for¹∈ { < . ≤ }, the (i, j)-th entry Di j is represented by (n, ¹). Also, when xi − xj is
unbounded, the entry Di j is represented by ∞. In addition, the upper bound and lower
bound of xi itself are indicated by D0,i and Di,0 respectively.
As an example of DBM, let’s consider a zone which satisfies following constraint.
x − 0 < 20 ∧ y − 0 ≤ 20 ∧ x − y ≤ −10 ∧ y − x ≤ 10 ∧ 0 − z < 5.
When we represent this zone as DBM, variables 0，x，y ，z are numbered with 0，1，2，
3 respectively in the matrix. DBM which represents the zone of the constraint is given by(1).



(0, ≤)(0, ≤)(0, ≤)

(20, <) (0, ≤) (−10, ≤)D=(20, ≤) (10, ≤) (0, ≤)∞∞∞(5, <)




∞ 
.

∞ 
(0, ≤)(1)

DBM is also represented as a set of some elements in the clock region CR(A ). Therefore a state set of states 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[9] 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 is a minimum set of differential
inequalities which can represents DBM D [9]. Such a set is denoted by c(D). c(D) canbe obtained by reduction operations on DBM. A set of every region which satisfies aninvariant I(l ) of location l is denoted by (l , DInv ).
2.4 General CEGAR Algorithm
Model abstraction sometimes over-approximates an original model, which causes spurious counter examples which are not actually counter examples in the original model.
5Figure 1: General CEGAR Algorithm

Paper[1] gives an algorithm called CEGAR (Counterexample-Guided Abstraction Refinement) shown in Figure 1.
In the algorithm, at the first step (called Initial Abstraction), it over-approximates theoriginal model. Next, we perform model checking to the abstract model. In this step,
if the model checker proofs the model satisfies a given specification, the original model
also satisfies the specification, because the abstract model is an over-approximation of theoriginal model. If the model checker proofs the model does not satisfy the specification,
however, we have to check a counter example produced by it whether it is spurious counterexample or not in the next step (called Simulation). In the Simulation step, if we find thecounter example is valid, we report it to the user and stop the loop. Otherwise, we haveto refine the abstract model to eliminate the spurious counter example, and repeat thesesteps until valid output is obtained.

6

Figure 2: Our Proposed Algorithm

3 Proposing CEGAR Algorithm
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̂ . If a counterexample 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 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 shallrefine 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.
∨
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 isno path to locations in E from the initial state. Please note that any counter example ofsuch 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.

73.1 Abstract Model
Definition 3.1 defines the abstraction function h on Lr of a region 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 thelocation 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̂ ofa 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.
Definition 3.3 gives an abstract model M̂ of a given timed automaton A using theabstraction function h defined in Definition 3.2.
Definition 3.3 (Abstract Model). An abstract model M̂ = (Ŝ, ŝ0 , →)
ˆ of a given timed
automaton A = (A, L, l0 , C, I, T ) using the abstraction function h defined in Definition
3.2 is defined as follows:• Ŝ = {h(l ) | l ∈ L)},• sˆ0 = h(l0 ),• →ˆ = {(lˆ1 , a, lˆ2 ) | (l1 , a, g, r, l2 ) ∈ T }.
Definition 3.4 (Counter Example). A counter example on M̂ is a sequence of states of Ŝ.
A counter example T̂ of length n is represented in T̂ = hŝ0 , · · · , ŝn i.

8

Abstraction
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̂
Figure 3: Abstraction
A set T of a run sequences on A obtained by concertizing a counter example T̂ =hŝ0 , · · · , ŝn i, is defined as follows:
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 )}.
3.2 Initial Abstraction
Initial Abstraction generates an abstract model M̂ from a timed automaton A =(A, L, l0 , C, I, T ) 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. When the algorithm in Fig. 4
returns false, the counter example T̂ is judged as a spurious counter example.

9

Simulation
a1 ,g1 ,r1

a2 ,g2 ,r2

an ,gn ,rn

Inputs A , (l0 −→ l1 −→ · · · −→ ln (ln = e))
R0 := (l0 , D0 ) {D0 = {0C }}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
Figure 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)
Figure 5: Reach10

3.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 CE free model for a given CE). When acounter example is judged as a spurious counter example, there is a Bad State l̂b which has
a corresponding state set B1 = (lb , D1 ) reachable from the initial state but unreachable tolnext , 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.
In general, refinement algorithm should divide state l̂b into more than two states asstate B1 and state B2 are mapped into differential states. Dividing of a state space ofa timed automaton usually needs Subtraction operation of DBM. However, DBM is not
closed under Subtract operation[13], so applying such an approach is difficult.
We proposes another approach, in which it duplicates state B1 in the concrete modeland also performs other transformation on the concrete model. Applying the abstraction
function to the transformed 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, and removal of transitions, shown in Fig.9, 10,
and 11, respectively.
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 duplication of a location lb be
lb0 . A set of states to duplicate, of a region automaton is defined as (lb0 , D1 ).
Duplication of transition duplicates the following kinds of transitions: “transitions
from lprev to lb ,” and “ transitions not only from lb but also enable from (lb , D1 ).”Definition 3.6 (Transitions to Duplicate). For a region automaton Ar = (A, Lr , lr 0 , Tr ),B1 = (lb , D1 ), states to duplicate (lb0 , D1 ), and a previous location lprev of a location lb ina counter example, transitions to duplicate of a region automaton is defined as follows:
Tr d = {(lprev , [v]) ⇒ (lb0 , [v 0 ]) |a∀(lprev , [v]) ∈ (lprev , DInv ).∀(lb , [v 0 ]) ∈ (lb , D1 ).(lprev , [v]) ⇒ (lb , [v 0 ]) ∈ Tr }a∪ {(lb0 , [v]) ⇒ (l , [v 0 ]) |∀(lb , [v]) ∈ (lb , D1 ). ∀(l , [v 0 ]) ∈ Lr .(lb , [v]) ⇒ (l , [v 0 ]) ∈ Tr }.
a

a

11

Figure 6: Counter Example

Figure 7: Refined Model

12

Refinement
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}
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
Figure 8: Refinement

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 )}{Duplicate a transition eb to a BadState}
foreach (l1 , a0 , g 0 , r0 , l2 ) ∈ T such that l1 = lb do
if Reach( A , (lb , Db ), (l1 , a0 , g 0 , r0 , l2 )) 6= ∅ thenT := T ∪ {(lb0 , a0 , g 0 , r0 , l2 )}{duplicate transitions from lb only enable from ((lb0 , Db ).)}
end ifend forFigure 10: Duplication of Transitions

13

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 ) = htrue, truei then{when R = B, relation(R, B1 ) returns h true, truei.}
T := T \ {(l , a, g, r, lb )}end ifFigure 11: Removal of Transitions
Definition 3.7 (Transitions to Remove). For a region automaton Ar = (A, Lr , lr 0 , Tr ),B1 = (lb , Dd ), states to duplicate (lb0 , D1 ), and a previous location lprev of a location in acounter example, transitions to remove of a region automaton is defined as follows:
Tr r = {(lprev , [v]) ⇒ (lb , [v 0 ]) |∀(lprev , [v]) ∈ (lprev , DInv ).(lprev , [v]) ⇒ (lb , [v 0 ]) ∈ Tr }aa.
The algorithm of Removal of Transitions removes transitions only when a set of states
reachable from lprev is the same as a set (lb , D1 ) of Bad States. Therefore, for everya(lprev , [v]) ⇒ (lb , [v 0 ]) ∈ Tr r , (lb , [v 0 ]) ∈ (lb , D1 ) holds. It means that every transition in
Tr r has its duplication in Tr d .
3.5 Example
We give an example of applying our abstraction method to Light Switch model[9].
The model is shown in Fig12, and it is composed of a switch model (left side of the figure)and a user model (right side of the model). Hereafter we assume locations (dim, idle) and(bright, idle) of the two models as error locations.
In order to apply our method to these models, first, we have to produce a parallel
composition of the models. Figure13 shows the composition. The property which wewant to check is:AG¬((dim, idle) ∨ (bright, idle)).

14

(2)

When we check the property (2) on the model of Fig13 using the model checker UPPAAL[10,11, 12], it outputs a result of “valid”. This means the model of Fig13 satisfies the property(2).
Here, we show an example of applying our abstraction method to the model.
As a first step, we produce an initial abstract model from the parallel composition. In
this step, we apply Initial Abstraction in which we remove clock variables x and y fromthe composition. Figure14 shows the initial abstract model.
Next, we perform model checking on the abstract model, and the model checker outputs a counter example h(of f, idle), (dim, relax), (bright, idle)i. This counter example
corresponds to a path from (of f, idle) to (bright, idle) in the original automaton.
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 conditionx ≤ 10 ∧ y > 10. Therefore, we can conclude that the counter example is spurious.
In the refinement step, first, we duplicate the location (dim, relax) on the timed automaton. (a duplicate of (dim, relax) is denoted by (dim, relax0 )). Please note that
we duplicate states only reachable from the initial state, and the reachable state space of(dim, relax) always satisfies x = y. Consequently, we have to add an invariant x = y to
the duplicated location (dim, relax0 ). Also, we duplicate transitions from (dim, relax)
except that being unable from the state space which satisfies x = y. Next, we remove atransition between (bright, idle) and (dim, relax). We can remove the transition because
there is a corresponding transition (bright, idle) to (dim, relax0 ). Figure15 represents therefinement guided by this counter example. Finally, we produce a refined abstract modelfrom the refined timed automaton.
After the refinement, we perform model checking again, and we obtain another counterexample h(of f, idle), (dim, t), (of f, study), (dim, idle)i. For this counter example, Simulation decides it is spurious, and the refinement is performed in the same way. Figure16
depicts the second refinement.
The additional model checking proves that the model satisfy the property. The timed
automaton and abstract model generated in the final loop are presented in Fig17 and Fig18
respectively.

15

Figure 12: Light Switch model

Figure 13: Parallel composed model

16

Figure 14: Initial abstract model

Figure 15: First refinement

17Figure 16: Second refinement

Figure 17: Timed automaton generated in the final loop18

Figure 18: Abstract model generated in the final loop19

4 Correctness Proof
As mentioned in Section 3, 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.
Paper [2] gives a theorem on a conservative class of abstractions which attempts topreserve 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.
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.
M̂ |= AG∨¬ê ⇒ A |= AG

∨

¬e

(3)

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:
h(s) |= p ⇒ s |= p(4)then M̂ |= AG p ⇒ M |= AG p holds from Theorem 1 in Paper [2].
∨∨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̂ andthe mapping is one-to-one mapping. Thus, h(l ) = ê ⇐⇒ l = e holds. As a result, theabstraction function h satisfies the statement 4; Theorem 4.1 is proved.
Lemma 4.1 (Bi-simulation equivalence among timed automata). Let denote by Ai andAi+1 a timed automaton before applying i + 1-th 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, Duplication of Transitions, andRemoval of Transition, respectively.
20

Figure 19: Relations among models

We will prove that Ai is bi-simulation equivalent to Ai+1 by proving bi-simulationequivalence over the corresponding region automata. For lb , let lb0 be a duplicated state.
For a set D1 of regions which associates to a location to duplicate, a set of states in Ar
will be (lb , D1 )，and (lb0 , D1 ). Let Tr d and Tr r be a set of transitions be added in Ar andthat to be removed in Ar , respectively.
i) Ar i and Ar1i
Let’s consider Ar i = (Lr i , lr i 0 , Tr i , Ai ) and Ar1i = (L1r i , lr1 i 0 , Tr1 i , A1i ). From theassumption, lr i 0 = lr1 i 0 ，Tr i = Tr1 i ，Ai = A1i and L1r i = Lr i ∪ (lb0 , D1 ) hold.
The initial statelr i 0 = lr1 i 0 ，and Tr i = Tr1 i . So, there is no transition to the duplicated state set (lb0 , D1 ) in Ar1i . Thus, there is bi-simulation equivalence between Ar i andAr1i .
ii) Ar1i and Ar2i
For Ar2i = (L2r i , lr2 i 0 , Tr2 i , A2i ), obviously L2r i = L1r i and lr2 i 0 = lr1 i 0 ，A2i = A1i
hold. Tr2 i = Tr1 i ∪ Tr d also holds.

21

We show that for every [v] ∈ D1 , a state (lb , [v]) and a state (lb0 , [v]) have a bia

simulation equivalence relation. When there exists a transition (lb , [v]) ⇒ (l , [v 0 ]) , asdefined in definition 3.6, the corresponding transition (lb0 , [v]) ⇒ (l , [v 0 ]) is generated.
aAlso, when there exists a transition (lb0 , [v]) ⇒ (l , [v 0 ]), there must be an original transia

tion (lb , [v]) ⇒ (l , [v 0 ]). Thus, we proved the first goal.
Thus, the concrete bi-simulation equivalence relation ∼ between 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(5)

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 corresponding transition in Tr2 i . Suppose thataalr1 i ∼ lr2 i and lr1 i ⇒ lr10i . Then 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 exists the original transition. Suppose thataalr1 i ∼ lr2 i and lr2 i ⇒ l 20 . Then there exists a transition lr1 i ⇒ lr10i and lr10i ∼ lr20i .
Therefore, Ar1i and Ar2i are bi-simulation equivalent.
iii) Ar2i and Ar3i
Let’s consider Ar3i = (L3r i , lr3 i 0 , Tr3 i , A3i ). Obviously L3r i = L2r i , lr3 i 0 = lr2 i 0 andA3i = A2i hold. Tr3 i = Tr1 i \ Tr r also holds.
The case when the algorithm in Fig. 11 does not perform any removal of transitions
is trivial. Ar2i is equivalent to Ar3i , thus also holds the relation ∼.
Otherwise, 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 and (lprev , [v]) ∈ (lprev , DInv )of Ar3i . Thus each state of L2r i and that of L3r i satisfy the relation defined in (5). In asimilar way of case ii), Ar2i and Ar3i are bi-simulation equivalent.
From the facts i), ii) and iii), we can conclude that Ar i and Ar i are bi-simulationequivalent.
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.
22

Proof. Let A , Ar and M̂ be a timed automaton, its region automaton and its abstract
model, respectively. For a counter example T̂ = hŝ0 , ŝ1 , · · · , ŝn i, where ŝn is an abstractstate obtained by reducing the error location, let consider one of the corresponding sea1 ,g1 ,r1

a2 ,g2 ,r2

an ,gn ,rnquences t = (l0 −→ l1 −→ · · · −→ ln ) to T̂ on A , where ln is error location.
Let Ri be a set of reachable i-th states 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 statecorresponding to Rk but unreachable to an abstract state corresponding to U Rk .”Let duplicated location from Ri be l 0 . Let the abstract state of l 0 be sˆ0 ( = h(l 0 )).
i

i

i

(*)

i

i) 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
the obtained abstract model, it is reachable to only sˆ0 corresponding to R1 , and it is1

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 state corresponding 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 asimilar 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 cannot be removed because U Rk is reachable from (lk−1 , DInv ). In such a case, from the inductive assumption,
we can obtain the refined abstract model, in which an abstract state corresponding to Rk−10
is reachable but U Rk−1 is not. Let lk−1
and lk0 be duplicated locations of Rk−1 in k − 1-thtime-Refinement and Rk in k-th time-Refinement, respectively. Adding transition from0lk−1
to lk0 improves the model so that it is reachable to only a state corresponding to Rk .

From (i) and (ii), statement (*) is proved.
If the counter example is spurious, it is unreachable from Rn−1 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.
23

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.
Proof. From Lemma 4.1, Refinement preserves bi-simulation equivalence. From Lemma
4.2, at most n times repetition of Refinement yields a refined spurious CE free model.

24

5 A tool based on the algorithm
In [20], a tool for evaluating the proposed abstraction is implemented. The inputs ofthe tool are an UPPAAL model file written in xml format and also a query file which
describes specifications, and it outputs the result of model checking. In the tool, the algorithms of Initial Abstraction, Simulation, and Abstraction Refinement are implemented,
and it performs model checking by calling a model checking command in UPPAAL, ‘verifyta’. When a given model does not satisfy a given specification, Execution of this command produces a counter example as a file. In the tool, to interpret the output file, it calls
a command ‘tracer’ provided by UPPAAL parser library.
The tool is implemented in Java, and details of it are presented in [20]25

6 Experimental Results
This section shows experimental results of applying the proposed abstraction to someexamples using the tool, and also evaluates effectiveness of the abstraction mainly fromthe view points of space consumption. The experiments are executed in the following
environment.
OS:

Fedora 7

CPU:

AMD Athlon(tm) 64 Processor 3400+ 2.2GHz

Memory:930MB

UPPAAL :version 4.0.6

Eclipse:version 3.3.1.1

JDK:

version 1.5.0 14

6.1 Aims of Experiments
In the experiments, we evaluate how the proposing abstraction saves memory consumption. Specifically, we compare memory consumption in performing UPPAAL model
checking with the proposing abstraction with that without it.
6.2 Results of Experiments
Here, results of applying to examples “Fischer’s mutual execution protocol”[11, 18],
and “Gearbox Controller”[19] are presented. In [20], other results are shown.
6.2.1 Fischer’s mutual execution protocol
The model of Fischer’s mutual execution protocol is composed of several numberof same processes. The experiments are executed on the models of 2 processes to 8
processes, and a requirement specification is that more than two processes do not stay inthe critical section at the same time. Table 1 shows results of these experiments.
The columns of ‘original’ and ‘composition’ represent results of performing model
checking to the original model and parallel composition of it, respectively, and they are
the result without abstraction. Also, the columns of ‘abstract’ represent results of applying

26

Table 1: Result of Fischer’s mutual execution protocol
original

composition

abstractionProclocation

clock

time

mem

time

mem

time

mem

loop

dup

2

16

2

0.10

2.81

0.10

2.82

0.74

2.82

5

10

3

64

3

0.10

2.81

0.10

2.81

2.44

2.82

13

30

4

256

4

0.10

2.81

0.20

5.51

10.9

21.6

25

60

5

1024

5

0.10

2.81

0.81

51.0

69.4

48.1

41

100

6

4096

6

0.10

2.81

5.26

125

662

95.0

61

150

7

16384

7

0.30

37.2

57.8

427

12571

293

85

210

8

65536

8

1.11

38.4

N/A

N/A

N/A

N/A

N/A

N/A

abstraction. The columns of ‘time’ represent total execution time (sec), and those of‘mem’ represent the maximum memory consumption during model checking (MB). The
columns of ‘loop’, ‘dup’ represent a count of loop, and a number of duplicated location,
respectively. In the experiment for the eight processes, results are not obtained because‘verifyta’ cannot handle the model which has more than 216 locations.
The results of this experiments show the proposed abstraction can reduce the memory
consumption from applying model checking without abstraction in the cases of more than
five processes. In particular, in the case of seven processes, it can reduce it about 30
percent.
6.2.2 Gearbox Controller
The model of Gearbox Controller is composed of five processes, and has five clock
variables. Paper[19] gives 14 requirement specifications to verify for the model, and the
proposed abstraction method can verify 5 specifications of them (specifications (7) to (11)in [19]). Table 2 shows results of experiments. The column of ‘spec’ means a specification
verified in its experiment.
The results of the second experiment show more effectiveness of the abstraction. For
all specifications, the abstraction reduces the memory consumption more than 80 percent.
6.3 Discussion
Let consider results of our algorithm (see abstraction columns of in Table 1 and Table2). In Fischer’s mutual execution protocol, the size of memory which the tool consumes is27

Table 2: Result of Gear Box Controller
original

composition

abstraction

spec

time

mem

time

mem

time

mem

loop

dup

(7)

0.10

2.82

0.82

50.0

5.51

8.71

3

8

(8)

0.10

2.81

0.81

50.0

5.35

8.71

3

8

(9)

0.10

2.78

0.81

50.0

7.47

8.67

5

18

(10)

0.10

2.81

0.82

50.0

7.63

8.84

5

49

(11)

0.10

2.82

0.81

50.0

7.30

8.67

5

22

about 70% of that of parallel composite version (parallel), whereas in Gearbox Controller,
The rate becomes about 20%.
The reason why the memory reduction rate of Fischer’s mutual execution protocol islower than that of GearBox Controller are (1) state explosion caused by parallel composition and (2) the number of clock guards is very small; the guard expression x > k, x ≤ konly exists on the transition to Critical Session location.
In such a case, normalization operation [9] for DBM reduces the size of clock state
space, consequently, UPPAAL can effectively reduce memory size. On the other hand,
Gearbox Controller uses a lot of clock constraints, which increases the size of total state
space.
Unfortunately, without parallel composition scheme (original) has the best results.
Our approach needs parallel composition which increases the memory size (see columns‘original’ and ‘composition’ in Table 1 and Table 2). In the original version, the size isvery small, because UPPAAL creates the total state space on-the-fly from parallel procedure presentation and also it uses Partial Order Reduction[16] techniques to reduce thesize of total state space, especially in Fischer’s mutual execution protocol.
6.4 Complexity
Here, the computational complexity and space complexity of our algorithm (Initial
Abstraction, Simulation and Refinement) are given.
For A = (L, l0 , T, I, C, A)，let n = |C|.
Initial Abstraction

From the algorithm of Fig3, the computational complexity is O(|L|+|T |) and the space complexity is also O(|L| + |T |)28

Simulation Let a length of counter example be l. In the algorithm Reach in Fig5,
operational functions up and and are used. The computational complexity of up and andare O(n) and O(n2 ), respectively. Therefore, the computational complexity of Reachis O(n2 ). Also, because a new DBM is generated in the algorithm Reach, the spacecomplexity is O(n2 ) . Because the algorithm Reach is called l times in Simulation, its
computational complexity and space complexity are O(l×n2 ) and O(l×n2 ), respectively.
Abstraction Refinement

The computational complexity of the algorithms Duplicate

State, DuplicateT ransition, RemoveT ransition is O(n3 ), O(|T |), O(n2 ). Therefore
that of the algorithm Refinement becomes O(n3 + |T |). Also, the space complexity ofthese algorithms are O(n2 ), O(|T |), and O(1). Thus, that of the algorithm Refinement isO(n2 + |T |).

29

7 Conclusion
This paper proposes a model abstraction technique for timed automata based on the
CEGAR algorithm. In general, most CEGAR based algorithmsobtain refined abstract
models from the previous abstract models by modifying some transformations. In ouralgorithm, however, the refined model is obtained indirectly; we transform the original
timed automaton preserving the equivalence and from it we generate an abstract modelby eliminating clock attributes.
This paper gives formal descriptions of our algorithms, and also correctness proofof our algorithms by proving that the transformation preserves bi-simulation equivalence
and that the refined abstract model is the spurious CE free.
The future work will be extensions of our algorithm. First, we want to handle integer
variables used in UPPAAL timed automata[10, 11, 12]. To abstract the state space overinteger variables, we are considering applying predicate abstraction[7] to it. Second, wewant to extend a range of specification formula for model checking.
In addition, we are considering that when we refine an abstract model, we apply a
Subtraction operation[13] to divide a bad state into a reachable state and unreachable one
instead of duplicating it, and also compare its efficiency with the method proposed in thispaper.

30

Acknowledgements
This work could be achieved owing to a great deal of helps of many individuals.
First, I would like to thank my supervisor Professor Shinji Kusumoto of Osaka University, for his continuous support, encouragement and guidance of the work.
I would like to express my sincere gratitude to Associate Professor Kozo Okano of Osaka University for his adequate guidance, valuable suggestions and discussions throughout this work.
I’m grateful to Assistant Professor Yoshiki Higo of Osaka University for his helpfulcomments and suggestions.
I’m thankful to Mr. Hironori Ashikari, an undergraduate student of Osaka University,
for his valuable help in this work especially Section 6.
Finally, I would like to thank the all members of Kusumoto Laboratory of Osaka
University for their helpful advice.

31

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.154-169, July, 2000.
[2] E M. Clarke, A. Gupta, J. Kukula, and O. Strichman: “SAT based AbstractionRefinement 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, A. Fehnker, Z. Han, J Ouaknine, O. Stursberg, and M. Theobald:“Abstraction and Counterexample-guided Refinement in Model Checking of Hybrid
Systems,” In Int. Journal of Foundations of Computer Science, vol.4, No.4, 2003.
[4] E M. Clarke, O. Grumberg, and D A. Peled: “Model Checking,” MIT Press, 2000.
[5] R. Alur: “Techniques for Automatic Verification of Real-Time Systems,” PhD thesis,
Stanford University, 1991.
[6] R. Alur, C. Courcoubetis, and D. L. Dill: “Model-checking for real-time systems,”
In Proc. of the 5th Annual Symposium on Logic in Computer Science, pp.414-425,
IEEE Computer Society Press, 1990.
[7] 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.
[8] R. Alur: “TimedAutomata,” In Proc. of the 11th Int. Conf. on Computer Aided
Verification, vol.1633, pp.688, July, 1999.
[9] J. Bengtsson, and W .Yi: “Timed Automata: Semantics, Algorithms and Tools,” In
Lectures on Concurrency and Petri Nets, vol.3098, pp.87-124, 2004.
[10] UPPAAL
http://www.uppaal.com/[11] G. Behrmann, A. David, and K G. Larsen: “A Tutorial on UPPAAL,” In Proc. of the
4th Int. School on Formal Methods for the Design of Computer, Communication,and Software Systems, vol.3185, pp200-236, 200432

[12] K G. Larsen, P. Pettersson, and W. Yi: In Springer International Journal of Software
Tools for Technology Transfer, vol.1(1-2), pp.134-152, 1997.
[13] A. David, J. Hakansson, K G. Larsen, and P. pettersson: “Model Checking Timed
Automata with Priorities using DBM Subtraction,” In Proc. of the 4th Int. Conf. on
Formal Modelling and Analysis of Timed Systems, pp.128-142, 2002
[14] S. Kemper, and A. Platzer: “SAT-based Abstraction Refinement for Real-time Systems,” In Third International Workshop on Formal Aspects of Component Software,
2006.
[15] 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.
[16] J. Bengtsson, B. Jonsson, J. Lilius and W. Yi: “Partial Order Reductions for Timed
Systems,” In Proc. of the 9th Int. Conf. on Concurrency Theory, vol.1466, pp.41-49,
1998.
[17] J. Hakansson, and P. Pettersson: “Partial Order Reduction for Verification of RealTime Components,” In Proc. of the 5th Int. Conf of Formal Modelling and Analysis
of Timed Systems, vol.4763, pp211-226, 2007.
[18] J. Bengtsson, K G. Larsen, F. Larsson, P. Pettersson, and W. Yi: “UPPAAL - a
Tool Suite for Automatic Verification of Real-Time Systems,” Hybrid Systems 1995,
pp232-243.
[19] 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 theConstraction and Analysis of Systems, vol.1384, pp.281-297, 1998.
[20] H. Ashikari: “Implement of Model Abstraction of Timed Automata Based on
Counterexample-Guided Abstraction Refinement Loop and its Evaluation on Effectiveness,” Bachelor Thesis, School of Engineering Science, Osaka University, Feb,
2008.

33

[21] 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.
[22] T. Nagaoka, K. Okano, and S. Kusumoto: “Abstraction of Timed Automata Based on
Counterexample-Guided Abstraction Refinement Loop,” IEICE Technical Report,
vol.107, to appear，2008.

34