1

Language Inclusion Checking of Timed
Automata with Non-Zenoness
Xinyu Wang, Jun Sun, Ting Wang, and Shengchao Qin
Abstract—Given a timed automaton P modeling an implementation and a timed automaton S as a specification, the problem oflanguage inclusion checking is to decide whether the language of P is a subset of that of S . It is known to be undecidable. The problem
gets more complicated if non-Zenoness is taken into consideration. A run is Zeno if it permits infinitely many actions within finite time.
Otherwise it is non-Zeno. Zeno runs might present in both P and S . It is necessary to check whether a run is Zeno or not so as to avoid
presenting Zeno runs as counterexamples of language inclusion checking. In this work, we propose a zone-based semi-algorithm for
language inclusion checking with non-Zenoness. It is further improved with simulation reduction based on LU-simulation. Though ourapproach is not guaranteed to terminate, we show that it does in many cases through empirical study. Our approach has been
incorporated into the PAT model checker, and applied to multiple systems to show its usefulness.

Index Terms—Timed Automata, Language Inclusion, Non-Zenoness.

F

1

I NTRODUCTION

T

IMED automata, introduced by Alur and Dill in [3], haveemerged as one of the most popular models to specify andanalyze real-time systems. It has been shown that the reachability
problem for timed automata is decidable through the constructionof region graphs [3]. Efficient methods based on zone abstraction
for checking both safety and liveness properties have later beendeveloped [25], [34]. Zone abstraction, which constructs zone
graphs, is an effective technique for model checking timed automata and it has been employed by many tools including the
popular U PPAAL [25]. Verification tools for timed automata basedmodels have proven to be successful [10], [13], [25], [37].
Nonetheless, researchers have also identified several issues
associated with timed automata based system verification [3], [14].
One of them is that the language inclusion checking problem isundecidable. In order to avoid this undecidability, a number ofdeterminizable subclasses of timed automata have been identified,e.g., event-clock timed automata [4], [28], and integer resets
timed automata [31]. In addition, it has been shown [26] theproblem of checking whether the language of a timed automaton
is a subset of that of a timed automaton with a single clock is
decidable. Another issue is related to the notion of Zeno runs.
An infinite run is non-Zeno if and only if it takes an unboundedamount of time; otherwise it is Zeno. Zeno runs are infeasible
in reality and thus must be pruned during system analysis. Thatis, it is necessary to check whether a run is Zeno or not so as
to avoid presenting Zeno runs as counterexamples. In particular,
liveness properties are usually meaningless unless non-Zenoness••••

Xinyu Wang is with College of Computer Science, Zhejiang University,
P.R. China. E-mail: wangxinyu@zju.edu.cn
The corresponding author Ting Wang is with College of Computer Science, Zhejiang University of Technology, P.R. China. E-mail: wangting@zjut.edu.cn
Jun Sun is with ISTD, Singapore University of Technology and Design,
Singapore. E-mail: sunjun@sutd.edu.sg
Shengchao Qin is with Teesside University, UK. E-mail: S.Qin@tees.ac.uk

is assumed; and safety properties cannot be trusted since Zeno
runs may conceal deadlocks, etc. Furthermore, the reason why
non-Zenoness checking is particularly challenging is that zone
graphs are too abstract to directly infer time progress and hence
non-Zenoness. For instance, given an infinite path in the zone
graph, it is infeasible to tell whether there are infinitely manytransitions that bound some clock x from above, but only finitely
many transitions that reset x and, thus, the total time elapsed isbounded. A number of approaches have been proposed to solve
the Zenoness checking problem in [22], [23], [34], [35]. The
state-of-the-art approach is based on constructing guessing zone
graphes which enrich zone graphs with additional information for
Zenoness checking [22], [23].
In this work, we investigate the language inclusion checking
problem of timed automata with non-Zenoness. That is, we define
the language of a timed (safety) automaton to be the set of finite
timed words obtained from runs which can be extended to an
infinite non-Zeno run. That is, we consider a finite timed word
non-Zeno if it can only occur as a part of Zeno infinite runs. We
develop a zone-based approach which, given a timed automaton
P modeling an implementation and a timed automaton S as a
specification, checks whether the language of P is a subset of thatof S . Language inclusion checking can be often converted to areachability problem on the product of P and the determinizationof S , where a state of the product is composed of a state of P
and a set of states from S . In our approach, we develop a semialgorithm which determinizes S and constructs the product on-thefly, where zones are used as a symbolic representation. Due to thecomplication of Zeno runs, the states of the product are enrichedwith additional labels so that only a part of a non-Zeno run in
P (which has no corresponding non-Zeno run in S ) is output asa counterexample. Furthermore, simulation reduction, based on
simulation relation between the product states obtained throughLU-simulation [6], is incorporated, which often contributes to thetermination of our semi-algorithm.
Our approach has been implemented in the PAT model
checker [32]. It can be applied to arbitrary timed automata,2though it may not always terminate. To show that our approach
can be useful in practice, we investigate when our approachis terminating empirically. Firstly, we prove that, if S satisfies
a clock boundedness condition defined in [5], our approach isguaranteed to terminate. Secondly, using a large set of randomly
generated timed automata, we show that our approach often
terminates. Lastly, we apply our approach to multiple benchmark
systems to investigate its scalability.
Related Work This work is related to the line of work on language
inclusion checking for timed automata. The work in [3] is thefirst study on the problem. It shows that timed automata are notclosed under complement, which is an obstacle in automaticallycomparing the languages of two timed automata. This conclusion leads to work on identifying determinizable subclasses of
timed automata, with reduced expressiveness. Several subclassesof timed automata have been identified, e.g., event-clock timed
automata [4], [28], timed automata with integer resets [31] andstrongly non-Zeno timed automata [5]. In addition, it has beenshown [26] that although timed automata with one clock are notdeterminizable, the problem of checking whether the language ofa timed automaton is a subset of that of a timed automaton with asingle clock is decidable.
Our work is inspired by [5], in which the authors present anapproach for deciding when a timed automaton is determinizable.
The idea is to check whether the timed automaton satisfies aclock boundedness condition. The authors show that the conditionis satisfied by event-clock timed automata, timed automata withinteger resets and strongly non-Zeno timed automata. Using region
construction, it is shown in [5] that an equivalent deterministic
timed automaton can be constructed if the given timed automaton
satisfies the clock boundedness condition. The work is closely
related to [2], in which the authors proposed a zone-based approach for determinizing timed automata with one clock. Our work
combines [2], [5] and extends them with simulation reduction soas to provide an approach which could be useful for arbitrary
timed automata in practice.
In addition, a game-based approach for determinizing timed
automata has been proposed in [9], [24]. This approach produces
an equivalent deterministic timed automaton or a deterministic
over-approximation, which allows one to enlarge the set of timed
automata that can be automatically determinized compared to theone in [5]. In comparison, our approach could determinize timed
automata which fail the boundedness condition in [5], and cancover the examples shown in [9]. The work is remotely related
to work in [20]. In particular, it has been shown that under
digitization with the definition of weakly monotonic timed words,
whether the language of a closed timed automaton is included in
the language of an open timed automaton is decidable [20].
This work is closely related to our previous work in [38],which proposes a semi-algorithm for language inclusion checkingof timed automata without non-Zenoness. We adopt the ideaof constructing an abstract product of the implementation andspecification in this work and extend it to investigate language
inclusion checking with non-Zenoness. Though some of the usedtechniques are similar, we target two different problems. To thebest of our knowledge, the language inclusion checking problem
with non-Zenoness for timed automata has been rarely addressed.
In [27], the authors showed that the refinement checking problemof safety MTL, a real-time extension of linear temporal logic, isdecidable. Their approach is to translate a safety MTL formula intoa single-clock timed automaton based on the non-Zeno semantics.
The refinement checking problem of safety MTL is then reduced
to the language inclusion checking problem between two singleclock timed automata.
This work is related to the line of work on non-Zenoness
checking. In [34], it has been shown that every run in a timed
automaton is non-Zeno if for each structural loop of the timed
automaton (i.e., a loop in the timed automaton itself, not theunderlying transition system), there exists a clock c such that c
is reset during the loop and c is bounded from below in a guardof a transition during the loop. A weaker condition is identified
in [12] (e.g., instead of checking all structural loops, only someloops are checked). Given a network of timed automata, it implies
that every run is non-Zeno if the product automaton satisfies
the condition. Sufficient conditions which guarantee absence ofZeno runs in a network without constructing the product havebeen identified [12]. Effectively, the work in [12] weakens therequirements imposed in [34].
The analysis in [12] is able to assert absence of Zeno runs
for a larger class of specifications, but it assumes a simple timed
automaton model. In [18], the authors show that the analysis
is not sound when U PPAAL extensions such as non-Zero clock
assignments and broadcast channels are considered, and that synchronisation can be better exploited to improve precision. Besides,
they extend the analysis to cases where urgent and committed
locations, urgent channels, parameters and selections are used in
the model.
However, preventing Zeno runs altogether by construction
would be too restrictive for users [18]. Rather, methods should
be provided to check whether a run is Zeno or not and discard
the Zeno runs in the process of verification. In [34], [35], theauthors showed that every timed automaton can be transformed
into a strongly non-Zeno one, for which, the emptiness problem
can be solved easily. The price to pay is an extra clock. It has
been shown that adding one clock may result in an exponentiallylarger zone graph [23]. The proposed remedy is the guessing-zonegraph approach. In addition, this work is related to the work on
non-Zeno real-time game strategy [15], which however is notbased on zone abstraction.
Organization The remainders of the article are organized asfollows. Section 2 reviews the relevant background. Section 3
shows how to reduce the language inclusion checking problem toa reachability problem in the concrete semantics. Section 4 thenshows how to reduce the language inclusion checking problem
to a reachability problem with zone abstraction. Section 5 thenpresents details on how the language inclusion problem is solved.
Section 6 reports the experimental results. Section 7 concludes.

2

P RELIMINARY

In this section, we review some relevant background on labeledtransition systems (LTS), timed automata and define our problem.
2.1

Labeled Transition Systems

An LTS is a tuple L = (S, Init, Σ, T ), where S is a set ofstates; Init ⊆ S is a set of initial states; Σ is an alphabet; andT ⊆ S × Σ × S is a labeled transition relation. L is deterministic
if and only if (s, e, s0 ) ∈ T and (s, e, s00 ) ∈ T imply s0 = s00 .
A run of L is a finite sequence of alternating states and events
hs0 , e1 , s1 , e2 , · · · , en , sn i such that (si , ei+1 , si+1 ) ∈ T for all

30 ≤ i ≤ n − 1. We say the run starts with s0 and ends with sn .
A state s0 is reachable from s if and only if there is a run startingwith s and ending with s0 . A state is always reachable from itself.
A run is rooted if it starts with a state in Init. A state is reachable
if there is a rooted run which ends at the state. Given the above
run, the sequence tr = he1 , e2 , · · · , en i is called a trace. We saythat sn is reachable from s0 via trace tr.
Let F ⊆ S be a set of target states. Given two states s0 ands1 in S , we say that s0 is simulated by s1 with respect to F if
s0 ∈ F implies that s1 ∈ F ; and for any e ∈ Σ, (s0 , e, s00 ) ∈ T
implies there exists (s1 , e, s01 ) ∈ T such that s00 is simulated by
s01 . In order to check whether a state in F is reachable, if weknow that s0 is simulated by s1 with respect to F and F is notreachable from s1 , F is also not reachable from s0 , and hence s0
can be skipped during system exploration if s1 has been exploredalready. This is known as simulation reduction [16].
2.2Timed Automata

Timed automata were originally introduced as finite-state timed
Büchi automata [3], i.e., finite automata equipped with realvalued clock variables and Büchi accepting condition. The Büchi
accepting condition is used to enforce progress, i.e., a run is
accepting if and only if it visits some accepting state infinitely
often. Later, timed safety automata were introduced in [21] which
adopt an intuitive notion of progress. That is, instead of having
accepting states, each state in timed safety automata is associated with a local timing constraint called a state invariant. An
automaton can stay at a state as long as the valuation of the clocks
satisfies the state invariant. The expressiveness of timed safetyautomata is strictly less than that of timed Büchi automata [30].
In the following, we focus on timed safety automata as they aresupported by the popular tools like U PPAAL [25] and are often
used in practice. Hereafter, they are referred to as timed automata
following common practice.
Let R+ be the set of non-negative real numbers. Given a setof clocks C , we define Φ(C) as the set of clock constraints.
Each clock constraint is inductively defined as follows:δ := true|x ∼ n|δ1 ∧ δ2 |¬δ1 where ∼∈ {=, ≤, ≥, <, >}; x isa clock in C and n is an integer constant1 . The set of downward
constraints obtained with ∼∈ {≤, <} and without negation ¬ isdenoted as Φ≤,< (C). A clock valuation v for a set of clocks C
is a function which assigns a real value to each clock. A clock
valuation v satisfies a clock constraint δ , written as v ∈ δ , if andonly if δ evaluates to be true using the clock values given by v .
A clock constraint can be viewed as the set of clock valuations
which satisfy the constraint. For d ∈ R+ , let v + d denote theclock valuation v 0 such that v 0 (c) = v(c) + d for all c ∈ C . For
X ⊆ C , let clock resetting notion [X := 0]v denote the valuationv 0 such that v 0 (c) = v(c) for all c ∈ C ∧ c ∈/ X , and v 0 (x) = 0
for all x ∈ X . We write C = 0 to be the clock valuation where
each clock c ∈ C reads 0.
Definition 1: A timed automaton is a tuple (S, Init, Σ, C, L, T )where S is a finite set of locations; Init ⊆ S is a set of
initial locations; Σ is an alphabet; C is a finite set of clocks;
L : S → Φ≤,< (C) labels each state with an invariant;
T ⊆ S × Σ × Φ(C) × 2C × S is a labeled transition relation.
1. We do not consider diagonal constraints in this work. Notice that due tothe negation, a clock constraint may not be convex.

Intuitively, a transition (s, e, δ, X, s0 ) ∈ T can be fired if δ issatisfied. After event e occurs, clocks in X are set to zero. An
example timed automaton is shown at the top of Fig. 1.
Definition 2: Let A = (S, Init, Σ, C, L, T ) be a timed automaton. The concrete semantics of A is an infinite-state LTS
C(A) = (Sc , Initc , R+ ∪ Σ, Tc ) such that Sc is a set of concrete
states of A, each of which is a pair (s, v) where s ∈ S is a locationand v is a clock valuation; Initc = {(s, C = 0)|s ∈ Init} isa set of initial concrete states; and Tc is the smallest transition
relation satisfying the following conditions:••((s, v), t, (s, v + t)) ∈ Tc if v + t ∈ L(s);or, ((s, v), e, (s0 , [X := 0]v)) ∈ Tc if there is a transition(s, e, g, X, s0 ) ∈ T such that v ∈ g and [X := 0]v ∈L(s0 ).

A timed automaton A is deterministic if and only if C(A) is
deterministic. Otherwise, A is non-deterministic. A (finite or
infinite) run of C(A) is of the form

π = h(s0 , v0 ), x1 , (s1 , v1 ), x2 , · · · , (si , vi ), xi , · · · iwhere ((si , vi ), xi , (si+1 , vi+1 )) ∈ Tc for all i. Note that xi iseither an event in Σ or a number in R+ . The duration of therun is the accumulated delay: Σd∈{xi |xi ∈R+ } d. An infinite run is
non-Zeno if its duration is unbounded. A finite run is non-Zeno
if and only if it is a prefix of some non-Zeno infinite run. Thatis, a finite run is Zeno if it cannot be extended to an infinite nonZeno run. Given the above run π , we can obtain a timed word:h(D1 , e1 ), (D2 , e2 ), · · · , (Di , ei ), · · · i such that e1 is the firstevent in the sequence hx1 , x2 , · · · i and D1 is the accumulateddelay before e1 occurs; and e2 is the second event in the sequenceand D2 is the accumulated delay before e2 occurs and so on. We
define L(A, (s, v)) to be the set of finite timed words obtained
from the set of all non-Zeno finite runs starting with (s, v). The
language of A, written as L(A), is defined as {x|∃s ∈ Init. x ∈L(A, (s, C = 0))}. Two timed automata are equivalent if they
define the same language.
The language inclusion checking problem with non-Zenonessis the problem of checking whether L(P) ⊆ L(Q), given a
timed automaton P and a timed automaton Q. In the rest of thearticle, we fix two timed automata with the same alphabet P =(Sp , Initp , Σ, Cp , Lp , Tp ) and Q = (Sq , Initq , Σ, Cq , Lq , Tq )such that Sp , Sq , Cp and Cq are pair-wise disjoint. We remarkthat in practice, P and Q are often composed of several timed
automata executing in parallel, i.e., a network of timed automata.
We skip the details on parallel composition of timed automata andremark our approach applies to networks of timed automata.
2.3

Zone Abstraction

Given a timed automaton A, zone abstraction is a technique forbuilding an abstraction of C(A) called a zone graph. Zone abstraction has been employed by many tools including U PPAAL [25]. A
zone is the conjunction of multiple primitive constraints over a setof clocks. Technically speaking, a zone is the maximal set of clock
valuations satisfying the constraint. A zone is empty if and only
if the constraint is unsatisfiable. In the following, we use zones
and clock constraints interchangeably as the latter is the syntactic
representation of the former.
The following zone operations are relevant in this work. Givena zone δ , we use δ ↑ to denote the zone reached by delaying an

4

S1

e1,x ≥ 1e2,x ≤ 1,{x}S2A
S1,x ≥ 0e1
e2

S2,x ≥ 1

ZG(A)Fig. 1. A sample zone grapharbitrary amount of time from zone δ ; we write [X := 0]δ todenote the zone obtained by resetting clocks in X to be 0. Givena set of clocks X , let δ[X] denote the projection of δ on X .

3

C HECKING WITH C ONCRETE S EMANTICS

In the following, we define an approach to solve the language
inclusion checking problem in the concrete semantics. Note that
it is only aimed to help understanding the approach in the next
section as obviously the concrete semantics is too big an LTS andcannot be constructed explicitly.
The problem of checking whether L(P) ⊆ L(Q) can beconverted to a reachability problem on the product of C(P) andthe determinization of C(Q). In the following, we formally define
these two operations: determinization and computing the product.
Definition 4: Given an LTS L = (S, Init, Σ, T ), the determinization of L is an LTS det(L) = (S 0 , {Init}, Σ, T 0 ) such that••

Definition 3: Let A = (S, Init, Σ, C, L, T ) be a timed
automaton. Its zone graph, denoted as ZG(A), is an LTS(Sz , Initz , Σ, Tz ) such that•••Sz is a set of nodes, each of which is a pair (s, δ) suchthat s ∈ S is a locationand δ is a zone;
V
Initz = {(init, ( c∈C c = 0)↑ ∧L(init))|init ∈ Init}
is a set of initial nodes;
Tz is the smallest labeled transition relation such that((s1 , δ1 ), e, (s2 , δ2 )) ∈ Tz if there exists a transition(s1 , e, δ, X, s2 ) ∈ T and δ1 ∧ δ 6= f alse and [X :=0](δ1 ∧ δ) ∧ L(s2 ) 6= f alse and δ2 = ([X := 0](δ1 ∧δ) ∧ L(s2 ))↑ ∧ L(s2 ).

An example zone graph is shown at the bottom of Fig. 1. The
following establishes the relation between ZG(A) and C(A).
Proposition 1 [39]: Let A = (S, Init, Σ, C, L, T ) be a timed
automaton and ZG(A) = (Sz , Initz , Σ, Tz ) be the zone graph.
(s, v) is a reachable state of C(A) if and only if there exists areachable state (s0 , δ) of ZG(A) such that s = s0 and v ∈ δ . 
The above proposition can be proved by an induction, i.e., it istrue for any initial state of C(A) and it is preserved throughevery transition in C(A). It implies that zone abstraction preserves
certain reachability properties (e.g., whether certain location isreachable or not). Unfortunately, zone abstraction is too abstract sothat it is impossible to decide if a path in the zone graph ZG(A)corresponds to a non-Zeno run of A [36]. The state-of-the-art
approach for solving this problem is to construct a guessing zone
graph, which enriches ZG(A) with additional information forchecking non-Zenoness [23]. We present the details of guessingzone graphes when they are relevant in Section 5.1.
We remark that the number of zones in ZG(A) is in general infinite. A number of normalization operators have been
defined [11], [29] to normalize the zones so that that the numberof zones is finite. For instance, the idea of maximum ceiling normalization [29] is to transform zones that may contain arbitrarily
large constants to a unique representation of a class of zones
whose constants are bounded by certain fixed constant, e.g., themaximum clock ceiling in A. In the following, we assume thatzone normalization is not applied unless it is stated otherwise.

S 0 = PS is the set of all sets of states in S ;T 0 is the smallest relation such that (X, e, Y ) ∈ T 0 if
Y = {y ∈ S|∃x ∈ X. (x, e, y) ∈ T }.

By definition, det(L) is deterministic. It is easy to show that L
and det(L) have the same set of traces. We remark that det(L)
could have exponentially more states than L.
Definition 5: Given two LTSs Li = (Si , Initi , Σi , Ti ) where i ∈{1, 2}, the product of L1 and L2 , denoted as L1 ⊗ L2 , is an LTS(S, Init, Σ, T ) such that S = S1 × S2 ; Init = Init1 × Init2 ;Σ = Σ1 ∪ Σ2 ; and T is the smallest transition relation such that•••((s1 , s2 ), e, (s01 , s2 )) ∈ T if (s1 , e, s01 ) ∈ T1 and e 6∈ Σ2 ;((s1 , s2 ), e, (s1 , s02 )) ∈ T if (s2 , e, s02 ) ∈ T2 and e 6∈ Σ1 ;((s1 , s2 ), e, (s01 , s02 )) ∈ T if (s1 , e, s01 ) ∈ T1 and(s2 , e, s02 ) ∈ T2 ;Next, we show how to check language inclusion with nonZenoness based on C(P) ⊗ det(C(Q)). Note that a state inC(P) ⊗ det(C(Q)) is of the form (s, X) where s is a state inC(P) and X is a set of states in C(Q). Intuitively, s and X can bereached via the same timed word respectively in C(P) and C(Q).
Without the assumption of non-Zenoness, it is sufficient to check
whether there is a reachable state (s, X) in the product such that
X is an empty set (i.e., there is a timed word which is possible in
P but not in Q). With the assumption of non-Zenoness, we needto check whether there is a non-Zeno run from s in P and there isa non-Zeno run from any state in X in Q. For simplicity, we saythat s is non-Zeno if and only if there is a non-Zeno run startingwith s; and a set of states is non-Zeno if and only if it contains
a non-Zeno state. Notice that by this definition, an empty set ofstates is Zeno.
Given a state (s, X) in C(P) ⊗ det(C(Q)), we need to
distinguish three cases in order to check language inclusion with
non-Zenoness.
••

Case 1: s is non-Zeno and X is non-Zeno, i.e., there
exists a non-Zeno run starting with s in P and and a nonZeno run starting with X in Q. In this case, the language
inclusion is not violated at this state.
Case 2: s is non-Zeno and X is Zeno, i.e., there exists a
non-Zeno run starting with s in P and there is no nonZeno run starting with any state in X in Q. Thus, the trace
reaching s is a trace of C(P) but not a trace of C(Q) andthe language inclusion may be violated.

5•

Case 3: s is Zeno, i.e., there is no non-Zeno run startingwith s in P . Thus, the runs starting with s are no longer
relevant for the language inclusion checking.

s1

x ≥ 3, es3

Theorem 1: L(P) ⊆ L(Q) if and only if there is no reachable
state (s, X) in C(P) ⊗ det(C(Q)) with an incoming edge labeledwith an event e ∈ Σ and s is non-Zeno and X is Zeno.

s2

x≤3

(a)

s1

x ≥ 3, e

s2

s3
(b)

Fig. 2. Timed automata examples

Proof: By induction, we can show that: (1) for all (s, X) in
C(P) ⊗ det(C(Q)), if s is reachable from an initial state in C(P)through trace tr, X is the set of all states reachable through tr
from any initial state in C(Q); and (2) if tr ends with an evente ∈ Σ, X is the set of all states reachable through a trace tr0 suchthat tr and tr0 result in the same timed word. Next, we prove thetheorem in both directions by contradiction.
(if) We first show that if L(P) ⊆ L(Q) does not hold, there exists(s, X) which satisfies the condition. By definition, if L(P) ⊆L(Q) does not hold, there is a timed word tw in L(P) but notin L(Q). By definition, there must be a trace tr of C(P) fromwhich we can obtain tw. Assume that after trace tr, we reachstate (s, X) in C(P) ⊗ det(C(Q)). By definition, s must be nonZeno. By (2) above, X contains all states reachable through a trace
tr0 such that tr and tr0 result in tw. By assumption, tw is not in
L(Q), therefore X must be Zeno.
(only if) We show that if there is a reachable configuration(s, X) satisfying the condition, L(P) ⊆ L(Q) does not hold. By
assumption, (s, X) must be reachable via a trace tr ending withan event e ∈ Σ. Since s is non-Zeno, the timed word obtained
from tr is in L(P). Since X is Zeno, the timed word obtained
from tr is not in L(Q) by (2). Thus L(P) ⊆ L(Q) does nothold.


invariant L(s), we construct a timed automaton A0 as follows.
Firstly, any outgoing transition (s, e, δ, X, s0 ) from s is changedto (s, e, δ ∧ L(s), X, s0 ). Secondly, for any incoming transition(s0 , e, δ, X, s) of s, for any clock constraint of the form x ∼ n
where ∼∈ {≤, <} in L(s), if x ∈/ X , conjunct δ with x ∼ n.
For instance, given the timed automaton in Fig. 2(a), we construct
the one in Fig. 2(b). The state invariant x ≤ 3 of state s3 is added
to the transition from s2 to s3 and the transition from s3 to s1 .
By a simple induction, it can be shown that the set of finite timed
words that can be obtained from A0 is the same as that of A.
Notice that because A0 has no state invariants (i.e., time canalways elapse unboundedly at any state), every run of A0 is nonZeno by definition. For instance, for the example shown in Fig. 2,
after the transformation, the timed automaton can idle at state s3
forever. As a result, this transformation does not preserve L(A),i.e., all Zeno runs in A become non-Zeno in A0 and a timed word
which is obtained only from Zeno runs in A is in L(A0 ) but notin L(A). This is not an issue as non-Zenoness is always checkedbased on the original timed automata, as we show in Section 5. In
the remainder of the section, we assume that all timed automata
are without state invariants unless otherwise stated.
4.2

In the following, we refer to a state (s, X) in C(P) ⊗ det(C(Q))
with an incoming edge labeled with an event e ∈ Σ where s is
non-Zeno and X is Zeno as a witness state, as it is a witnessof violation of language inclusion, by the above theorem. The
problem of language inclusion checking is thus reduced to the
problem checking whether a witness state is reachable.

4

L ANGUAGE I NCLUSION C HECKING WITH Z ONESIn this section, we present how to construct an abstraction ofC(P) ⊗ det(C(Q)) based on zone abstraction, based on which
we solve the language inclusion checking problem. As discussed
above, language inclusion checking requires constructing the
product of P and the determinization of Q. Determinizing timed
automata in general is undecidable [3]. In the following, we
describe an approach which can be applied to arbitrary timed
automata. Though it is not guaranteed to terminate, we show that
it is useful in the setting of language inclusion checking. The
approach is presented in two parts in the following: 1) unfolding
the original timed automaton into an infinite timed tree; and 2)
building the product of P and the determinization of the timed
tree generated from Q based on zones.
4.1

Removing State Invariant

In order to simplify the presentation in the remaining of thesection, we first transform P and Q to a form without stateinvariants. The idea is to move the state invariants to transition
guards. Given a timed automaton A and any state s with state

Unfolding

The idea of unfolding the original timed automaton into an infinite
timed tree is adopted from [5]. The reason for the unfolding is thatthe infinite timed tree has the input-determinacy property, withwhich we can determinize this tree during the construction of the
product.
In the following, we first show how to construct an unfoldingof Q which is equivalent to Q through an example. Given thetimed automaton Q in Fig. 3(a), Fig. 3(c) shows the infinite timed
tree after unfolding Q. A fresh clock is introduced at every leveland used to replace the original clocks, i.e., x and y are replacedby clocks from a set Z = hz0 , z1 , z2 , · · · i. At level 0, we areat state q0 and introduce a clock z0 . Since clock x and clock y
start at the same time as z0 , we can use z0 to replace x and yin the transition guard from q0 at level 0 to the nodes at level 1.
Because at level 0, the reading of clock z0 is relevant to the futuresystem behavior (i.e., there is a transition guard whose truth value
depends on z0 ), we say that z0 is active at this node. In the tree,
we label every node with a pair (q, A) where q is a location and
A is a set of active clocks.
Two transitions from the level 0 node leads to the node of level
1, corresponding to the transitions from location q0 to location q0
and q1 in Fig. 3(a). The clock constraint x < 5 is rewritten toz0 < 5 using the active clock z0 from the source node. A freshclock z1 is introduced along the transitions. Notice that the nodewith location q0 at level 1 is labelled with a set of two active
clocks. z1 is active at location q0 at level 1 since it can be used
to replace clock x which is reset along the transition, whereas z0
is active because it is used to replace clock y which is not reset6q0

x < 5, a
{x}

{z0}

q0

L0
a, {z1}z0<5, a, {z1}

{z0}

q0
a, {z1}z0<5, a, {z1}aq1

y < 20, a{x}{z1, z0} q0x < 5, a
{x}

a
{x}

q1

L1
z0<20, a, {z2}z1<5, a, {z2}(a) a timed automaton Q

q0

{z0}

{z1, z0} q0z1<5, a, {z2}a, {z2}{z2, z0} q0q1{z1, z0}

z0<20, a, {z2}a, {z2}q1{z1, z0}z2<5, a, {z3}{z2, z0}

q1

L2

z2<5, a, {z3}z0<20, a, {z3}q1 {z1, z0} q1{z2, z0} q0{z2, z0}
z0<20, a, {z3}z0<20, a, {z3}z0<20, a, {z3}q1

y < 20, a{z3, z0} q0a, {z3}q1{z2, z0}q1

L3{z3, z0}{z3, z0} q0a, {z3}q1 {z2, z0} q1 {z1, z0} q1{z3, z0}(b) a timed automaton Q’(d) unfolding Q’(c) unfolding Q

Fig. 3. Unfolding timed automata into infinite timed trees

along the transition. The set of active clocks of the node withlocation q1 at level 1 is a singleton z0 since both of the clocks x
and y are not reset along the transition. Here z1 is not active as its
reading is irrelevant to future transitions from q1 . Following thesame construction, we build the tree level by level.
In the following, we define the unfolding of Q formally. Let
Z = hz0 , z1 , z2 , · · · i be an infinite sequence of fresh clocks. The
unfolding Q is an infinite timed tree, which can be viewed as atimed automaton Q∞ = (S∞ , Init∞ , Σ, Z, T∞ ) with infinitely
many locations. Furthermore, we assume that Q∞ is associatedwith a function level such that level(n) is the level of node n in
the tree for all n ∈ S∞ . A state n in S∞ is in the form of (q, A)
where q ∈ Sq and A is a set of clocks in Z . Given any state n,
we define a function fn : Cq 7→ Z which maps ordinary clocks in
Cq to active clocks in Z . In an abuse of notations, given a clock
constraint δ on Cq , we write fn (δ) to denote the clock constraint
obtained by replacing clocks in Cq with those in Z according to
fn . The initial states Init∞ and transition relation T∞ are theminimum set satisfying the following.
••

For any q ∈ Initq , there is a level-0 node n = (q, {z0 })in Init∞ with level(n) = 0, fn (c) = z0 for all c ∈ Cq .
For each node n = (q, A) at level i and for each transition(q, e, δ, X, q 0 ) ∈ Tq , we add a node n0 = (q 0 , A0 ) at leveli+1 where A0 is the minimum set satisfying the following
conditions: (1) if c ∈ Cq \ X , then fn0 (c) = fn (c) andfn0 (c) is contained in A0 ; (2) if c ∈ X , fn0 (c) = zi+1 andzi+1 is contained in A0 ; (3) level(n0 ) = i+1. Afterwards,
we add a transition (n, e, fn (δ), {zi+1 }, n0 ) to T∞ .

Note that transitions at the same level have the same set ofresetting clocks, which contains exactly one clock. Given a noden = (q, A) in the tree, observe that not every clock x in A
is active. Hereafter, we assume that inactive clocks are always
removed. The infinite timed trees constructed this way may or
may not be finitely-branching. For instance, the tree in Fig. 3(c)is finitely-branching, as there are at most 4 branches from one
level to the next. Furthermore, the number of clocks at eachlevel is bounded by 3. Another example is shown in Fig. 3(d),which is obtained by unfolding the timed automaton shown in
Fig. 3(b). More and more branches are generated during thelevel-by-level construction. As a result, the number of clocks

becomes unbounded. These observations are closely linked to thetermination of the language inclusion checking algorithm which is
introduced later.
4.3

Constructing the Abstract ProductFollowing the result in [5], it can be shown that the set of finite
timed words obtained from Q and from Q∞ are equivalent. In
the following, we define a zone graph for the product of P and
determinization of Q∞ , referred to as the abstract product, basedon which we solve the language inclusion checking problem.
The abstract product is an LTS Z∞ = (S, Init, Σ, T ). A statein Z∞ is of the form (sp , Xq , δ) such that sp ∈ Sp ; Xq is a setof nodes in Q∞ ; and δ is a clock constraint constituted by clocks
in Cp and Q∞ . Recall that a node of S∞ is of the form (sq , A)
where sq ∈ Sq and A is a set of active clocks. Given a set ofnodes Xq of S∞ , we write Act(Xq ) to denote the set of all active
clocks, i.e., {c|∃(sq , A) ∈ Xq . c ∈ A}. δ constraints all clocks in
Act(Xq ). We remark that a state in Z∞ encodes a set of states inC(P) ⊗ det(C(Q)). The set of initial states Init is defined as thefollowing: {(sp , Init∞ , (Cp ∪Act(Init∞ ) = 0)↑ )|sp ∈ Initp }.
Next, we define T by showing how to generate successorsof a given abstract configuration (sp , Xq , δ), which is illustrated
in Fig. 4. For every event e ∈ Σ, let T∞ (e, Xq ) be the set oftransitions in T∞ which start with a state in Xq and are labeledwith event e. Notice that the guard conditions of transitions in
T∞ (e, Xq ) may not be mutually exclusive. We define a set of
constraints Cons(e, Xq ) such that each element in Cons(e, Xq )is a constraint which conjuncts, for each transition in T∞ (e, Xq ),either the transition guard or its negation. Notice that elements
in Cons(e, Xq ) are by definition mutually exclusive. Given(sp , Xq , δ) and a transition (sp , e, gp , Xp , s0p ) in P , for eachg ∈ Cons(e, Xq ) we generate a successor (s0p , Xq0 , δ 0 ) such thatthe following conditions are satisfied.
••

For any state (sq , A) ∈ Xq and any transition((sq , A), e, gq , Yq , (s0q , A0 )) ∈ T∞ (e, Xq ), (s0q , A0 ) ∈Xq0 if and only if δ ∧ gp ∧ g ∧ gq is not false.
All states in Xq are at the same level and thus all transitions in T∞ (e, Xq ) have the same resetting clock. Let y
be that clock and δ 0 = ([{y} ∪ Xp := 0](δ ∧ g ∧ gp ))↑ .

(b) a timed automaton Q’(d) unfolding Q’(c) unfolding Q

7(sp, Xq={..., (sq, A), ...}, δ)
gp, e, Xp

gq, e, Yq...

(sp, Xq={..., (sq, A), ...}, δ)
gp, e, Xp...

T∞(e, Xq )sp, Xq={..., (sq, A), ...}, δg, e, {y}δ˄gp˄g, e, Xp∪{y}

...

...

...

g∈Cons(e, Xq )...

sp', Xq', δ'

q0
a

q1

(a) a timed au

Fig. 4. Generating successors

The transition from (sp , Xq , δ) to (s0p , Xq0 , δ 0 ) is labeledwith e.

abstract configuration of level 4 in the figure (named pq ), theconstraint neg in Cons(a, Xq ) is: z0 ≥ 20. Conjuncted with theguard condition x < 10 and the constraint in node pq , it is not
We illustrate the above construction using the example infalse and there is a successor generated for neg as the node pq 0
Fig. 5, where Fig. 5(a) is P and Fig. 5(b) is the infinite, {(q0, that{z0})}the Xq at this node ison the left-bottom of the figure.p0Note
x < 10, a
timed tree Q∞ . The only initial state0≤x=z
p0 of the{x}abstract product empty. As a result, the problem of0checking
whetherx<10 ˄ z0the≥5, aset ofis (p0 , {(q0 , {z0 })}, 0 ≤ x = z0 ), as shown at the top of{x, toz1} checking
x<10
˄
z
<5,
a
timed words of P is a subset0 of that of Q is reduced{x, z1}
timed automaton
Fig. 5(c). As shown in Fig. 5(b),(a)there
are two Ptransitions fromwhether Zr contains a state (sp , Xq , δ) where Xq is empty.
p0, {(q0, {z1, z0}), (q1, {z0})}p0, {(q1, {z0})}
node (q0 , {z0 }) labeled with event a, which are contained in
Language inclusion
checking
with
non-Zenonessis more
0≤x=z
˄
0≤z
-x<5
˄
0≤z
-z
<5
0≤x
˄ 5≤z0com˄ 5≤z0-x<10
1001
T∞ (a, {(q0 , {z0 })}). Oneofthetransitions
has
the
guard
z
<
5
0
{z0}
q0
plicated because even if Xq is not empty, it might be that there are
and the other one has the guard ‘true’. The
set
Cons(a,X)qx<10 ˄ z1≥5 ˄ z0<20, ax<10 ˄ z1<5clock˄ z0<20,aa, {z1}
only
Zenovaluationsatisfying{x,runsz2} from Xq in Q with the{x,z0<5, a, {zz1}0 < 5 and z0 ≥ 5. Taking
contains the following constraints:z2}
δ . Recall that a state (sp , Xq , δ) in Zr encodes
a set of states
the transition form p0 to p0 in P , we generate two potential p0, {(q1, {z1, z0}), (q1, {z2, z0})}p0, {(q, {z2, z0})}0, {z2, z0}), (q1, {z1, z0}), (q11,renaming).
By
Theorem{z1,constraintsz0} q0
q1 X ), as shown of C(P) ⊗ det(C(Q)) (modula clock
successors for each of thein Cons(a,q0≤x=z2 ˄ z1≥5 ˄ z0≥5 ˄ 5≤z1-x<100≤x=z2 ˄ z1≥0 ˄ z0≥0 ˄ 0≤z1-x<5 ˄ 0≤z0-x<10{z0}
in order to check language inclusion,
given a state (sp , Xq , δ)a, {z2}Note˄ 5≤z0-x<15 ˄ 0≤z0-z1<5above. Similarly, we can generate
other states levelzby
level.
˄ 0≤z -z <50<20,
z1<5, a, {z2}in Zr , we need to check if the states encoded as 0(s1p , Xq , δ)that for readability, we additionally label the edges in Fig. 5(c)x<10z2<5 ˄ z0<20, a
include a witness state. Inx<10the ˄following,a ˄functiona, {z2}z2≥5 ˄ z0<20, we
a design
with the corresponding guard condition andthe resetting clocks.
{x,ifz3the
}
{x,
z3}
witness(s
,
X
,
δ,
P,
Q)
which
returns
true
if
and
only
p
q
{z
,
z
}
q
q
q
2 0
1
1 are
The abstract product graphis 0always infinite-stateas, zthere{z}
2 0{z1, z0}
states encoded as (sp , Xq , δ) include a witness state. For instance,
infinitely many clocks. In thefollowing,
we show how to reduce
p0, {(q1, {z2, z0}), (q1, {z3, z0})}p0, {(q0, {z3, z0}), (q1, {z2, z0}), (q1, {zz2<5,a, {z3}z0<20, a, {z3} given the state at the right of level 1 in Fig. 6, function witness
0≤x=z3 ˄ z2≥5 ˄ z0≥5 ˄ 5≤z2-x<100≤x=z3 ˄ z2≥0 ˄ z0≥0 ˄ 0≤z2-x<5 ˄ 0≤z
the number of states by reducing the number of clocks, which isz0<20, a, {z3}would return
true0-x<20
since˄theof states of P is non-Zeno, whereas
˄ 5≤z0≤zset˄ 0≤z0-z2<10
0-z2<10inspired by [5]. Intuitively, given any a,abstractstate (sp , Xq , δ){z3}
the one of Q is Zeno because clock y is bounded from above
{z
,
z
}
q
q
q
3
0
0
1
1
in Z∞ , instead of always using a new clock in Z , we can{z2, z0}{z3, z0}
but never reset afterwards (x<10z0 represents
clocksx and y withx<10
˄ z3≥5 ˄ z0≥20,
ax<10 ˄ z3≥5 ˄ z0<20, areuse a clock which is not zcurrently
active, or equivalently not
3<5, a, {z4}conclude that{x,the{x, z4}z0<20, a, {z4} x = y ). As a result, we can immediately
z4}
in Act(Xq ). We denote the zone graph after renaming as Zr . It is
language inclusion with non-Zenoness is violated.
z0<20, a, {z4}easy to show that Zr and Z∞ are equivalent[5].
a, {z4}, {(q1, {zz0})}p0, {(q1, {z3, pz,0}),, {zInp0order
to3, realizefunction witness(sXq(q, 1δ,P,
Q)
, we p0, {(q0, {z
4, z
0})}
{z4, z0}Fig.
q0 5(c) is shownq1 in Fig. 6.q1 For
The result of renaming
0≤x=z4 ˄ z30≤x
˄ z3to>5 solve˄ z0≥20the˄ 5<z
0≤x=z4 ˄ z3i.e.,≥5 ˄ zgiven
3-x<100≥5 ˄ 5≤z
3-x<10need
underlying
problem,
any
timed
{z
,
z
}
{z
,
z
}
3 0of level 3 in
4 Fig.
0instance, given the configuration on the left5(c),
˄ 20≤z0-x<25 ˄ 10<z0-z3<15˄ 5≤z0-x<20 ˄ 0≤z0-z2<15
automaton A and a set of states of C(A), how do we checkthere are three active clocks z0 , z2 and z3 . We can reuse z1 andwhether there is non-Zeno run from one of the states in thesystematically rename z3 to z1 since
z1 istimed
not treeactive.
(b) infinite
Q∞ Notice that(c) synchronous productset. We solve the problem through constructing a guessing zone
after renaming, the number of clocks may still be infinite, e.g., thegraph [23] based on the original automaton A without removing
tree as shown in Fig. 3(d).
the state invariants.
•

5

L ANGUAGE I NCLUSION WITH N ON -Z ENONESSIn the following, we first show how to check whether the set offinite timed words of P is a subset of that of Q based on Zr andthen show how to solve the language inclusion checking problem
with non-Zenoness.
5.1

Checking Language Inclusion with Non-Zenoness

Given a state (sp , Xq , δ) in Zr , we need to check that for any
timed event that sp can perform, whether Xq can perform the same
timed event. Notice that one of the constraints in Cons(e, Xq )conjuncts the negations of all guards of transitions in T∞ (e, Xq ).
Let us denote the constraint as neg . Given neg , assume thecorresponding successor is (s0p , Xq0 , δ 0 ). It is easy to see that
Xq0 must be empty. If δ 0 is not false, intuitively there exists atime point such that P can perform e whereas Q cannot. This is
illustrated by the example shown in Fig. 6. Given the left-mostDefinition 6: Let A = (S, Init, Σ, C, L, T ) be a timed automaton and (s0 , δ0 ) be an abstract state where s0 ∈ S and δ0 is aclock constraint. The guessing zone graph with respect to (s0 , δ0 ),denoted as GZG(A, s0 , δ0 ), is an LTS (Sg , Initg , Σ × Φ(C) ×
2C , Tg ) such that a state in Sg is of the form (s0 , δ 0 , Y ) where(s0 , δ 0 ) is an abstract state and Y ⊆ C ; Initg = {(s0 , δ0 , C)};and Tg is the smallest transition relation satisfying the following
conditions.
••((s1 , δ1 , Y ), e, δ, X, (s2 , δ2 , Y ∪ X)) ∈ Tg if t =(s1 , e, δ, X, s2 ) is a transition in A and there is atransition ((s1 , δ1 ), e, (s2 , δ2 )) in ZG(A) and there areclock valuationsVv ∈ δ1 , v 0 ∈ δ2 and d ∈ R+ suchthat v + d ∈ x∈C−Y x > 0 and v + d ∈ δ and[X := 0](v + d) = v 0 .
((s, δ, Y ), τ, true, ∅, (s, δ, Y 0 )) ∈ Tg where Y 0 = ∅ or
Y 0 = Y where τ is a special invisible event.

8p0, {(q0, {z0})}0≤x=z0x < 10, a{x}p0(a) timed automaton P

L0

{z0}

p0, {(q0, {z1, z0}), (q1, {z0})}0≤x=z1 ˄ 0≤z0-x<5 ˄ 0≤z0-z1<5q0{z1, z0} q0x<10 ˄ z1≥5 ˄ z0<20, a{x, z2}a, {z1}z0<5, a, {z1}

L1

{z0}

z0<20, a, {z2}a, {z2}{z2, z0} q0q1{z2, z0}{z1, z0}z2<5, a, {z3}p0, {(q1, {z2, z0}), (q1, {z3, z0})}0≤x=z3 ˄ z2≥5 ˄ z0≥5 ˄ 5≤z2-x<10˄ 5≤z0-x<20 ˄ 0≤z0-z2<10

z0<20, a, {z3}L3{z3, z0} q0q1{z3, z0}z3<5, a, {z4}a, {z4}L4{z4, z0} q0p0, {(q0, {z3, z0}), (q1, {z2, z0}), (q1, {z3, z0})}0≤x=z3 ˄ z2≥0 ˄ z0≥0 ˄ 0≤z2-x<5 ˄ 0≤z0-x<15˄ 0≤z0-z2<10

x<10 ˄ z3≥5 ˄ z0≥20, a{x, z4}z0<20, a, {z4}L2x<10 ˄ z2<5 ˄ z0<20, a{x, z3}q1{z2, z0}L1p0, {(q0, {z2, z0}), (q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥0 ˄ z0≥0 ˄ 0≤z1-x<5 ˄ 0≤z0-x<10
˄ 0≤z0-z1<5x<10 ˄ z2≥5 ˄ z0<20, a{x, z3}q1

z0<20, a, {z3}a, {z3}p0, {(q1, {z0})}0≤x ˄ 5≤z0 ˄ 5≤z0-x<10

x<10 ˄ z1<5 ˄ z0<20, a{x, z2}p0, {(q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥5 ˄ z0≥5 ˄ 5≤z1-x<10˄ 5≤z0-x<15 ˄ 0≤z0-z1<5q1

z1<5, a, {z2}L2

L0x<10 ˄ z0≥5, a{x, z1}x<10 ˄ z0<5, a{x, z1}x<10 ˄ z3≥5 ˄ z0<20, a{x, z4}

L3

x<10 ˄ z3<5 ˄ z0<20, a{x, z4}z0<20, a, {z4}q1q1{z3, z0}{z4, z0}p0, {(q1, {z3, z0})}0≤x ˄ z3>5 ˄ z0≥20 ˄ 5<z3-x<10˄ 20≤z0-x<25 ˄ 10<z0-z3<15p0, {(q1, {z3, z0}), (q1, {z4, z0})}0≤x=z4 ˄ z3≥5 ˄ z0≥5 ˄ 5≤z3-x<10˄ 5≤z0-x<20 ˄ 0≤z0-z2<15(b) infinite timed tree Q∞

p0, {(q0, {z4, z0}), (q1, {z3, z0}), (q1, {z4, z0})}0≤x=z4 ˄ z3≥0 ˄ z0≥0 ˄ 0≤z3-x<5 ˄ 0≤z0-x<20
˄ 0≤z0-z3<15

L4(c) synchronous productFig. 5. An example of productp0, {(q0, {z0})}0≤x=z0Level 0x<10 ˄ z0≥5, a{x, z1}x<10 ˄ z0<5, a{x, z1}p0, {(q0, {z1, z0}), (q1, {z0})}0≤x=z1 ˄ 0≤z0-x<5 ˄ 0≤z0-z1<5

Level 1x<10 ˄ z1≥5 ˄ z0<20, a{x, z2}

Level 2p0, {(q1, {z0})}0≤x ˄ 5≤z0 ˄ 5≤z0-x<10

x<10 ˄ z1<5 ˄ z0<20, a{x, z2}p0, {(q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥5 ˄ z0≥5 ˄ 5≤z1-x<10˄ 5≤z0-x<15 ˄ 0≤z0-z1<5p0, {(q0, {z2, z0}), (q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥0 ˄ z0≥0 ˄ 0≤z1-x<5 ˄ 0≤z0-x<10
˄ 0≤z0-z1<5x<10 ˄ z2≥5 ˄ z0<20, a{x, z1}p0, {(q1, {z2, z0}), (q1, {z1, z0})}0≤x=z1 ˄ z2≥5 ˄ z0≥5 ˄ 5≤z2-x<10˄ 5≤z0-x<20 ˄ 0≤z0-z2<10

Level 3p0, {(q0, {z1, z0}), (q1, {z2, z0}), (q1, {z1, z0})}0≤x=z1 ˄ z2≥0 ˄ z0≥0 ˄ 0≤z2-x<5 ˄ 0≤z0-x<15˄ 0≤z0-z2<10

x<10 ˄ z3≥5 ˄ z0≥20, a{x, z2}

Node pq
Level 4p0, {(q1, {z1, z0})}0≤x ˄ z1>5 ˄ z0≥20 ˄ 5<z1-x<10˄ 20≤z0-x<25 ˄ 10<z0-z1<15

x<10 ˄ z2<5 ˄ z0<20, a{x, z1}x<10 ˄ z1≥5 ˄ z0<20, a{x, z2}p0, {(q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥5 ˄ z0≥5 ˄ 5≤z1-x<10˄ 5≤z0-x<20 ˄ 0≤z0-z2<15

x<10 ˄ z1<5 ˄ z0<20, a{x, z2}p0, {(q0, {z2, z0}), (q1, {z1, z0}), (q1, {z2, z0})}0≤x=z2 ˄ z1≥0 ˄ z0≥0 ˄ 0≤z1-x<5 ˄ 0≤z0-x<20
˄ 0≤z0-z1<15

x<10 ˄ z0≥20, aNode pq’
p0, { }
0≤x ˄ z1>5 ˄ z0≥20 ˄ 5<z1-x<10˄ 20≤z0-x<25 ˄ 10<z0-z1<15

Fig. 6. From language inclusion checking to reachability analysis

Compared to zone graphs, guessing zone graphes contain extra
states and transition labels which are designed for detecting
Zenoness. Intuitively, there are two reasons why a path in thezone graph disallows time from elapsing unboundedly. Either thepath has infinitely many transitions that bound some clock x fromabove, but only finitely many transitions that reset x and, thus,
the during of any run following the path is bounded. Or, thepath contains transitions that reset x, and always subsequently
transitions that requires x = 0 and thus time cannot elapse atall. The transitions which require x = 0 are called zero-checks.
Guessing zone graphs are designed to handle these two cases
explicitly. In particular, the Y component of a node (s, δ, Y )allows us to infer that the clocks not in Y are strictly positive.
A node of the form (s, δ, ∅) is called clear node, from which
every reachable zero-check is preceded by the reset of the clockthat is checked, and hence nothing prevents time from elapsing inthis node. An infinite path of the guessing zone graph is non-Zeno
if all clocks bounded from above are reset infinitely often and thepath contains a clear node [23]. A path is blocked if there is aclock that is bounded from above infinitely often and reset only
finitely often by the transitions on the path. Otherwise the path iscalled unblocked.
Given the automaton A shown in Fig. 1, Fig. 7 shows
the zone graph ZG(A) along with the guessing zone graph
GZG(A, s1 , x ≥ 0), where self-loop τ -transitions are removed
for readability. An unblock path containing a clear node, i.e., a{z3, z0} q0y < 20, aq1

a, {z3}q1 {z3, z0} L4 {z3, z0} q0a, {z3}q1 {z2, z0} q1 {z1, z0} q1{z3, z0}(b) a timed automaton B(c) unfolding A

Σ1,x ≥ 1

Σ2,x ≤ 1,{x}S2S1,x ≥ 0

S1,x ≥ 0,{x}e2x ≤ 1, e1,e2,{x} x ≥ 1(d) unfolding Bτ

9Algorithm 1: Function nz(s, δ, A, N ZSet, ZSet)

S1,x ≥ 0,ø
x < 10, ap0{x}Input: timed automaton A and an abstract state (s, δ)
Output: true if and only if (s, δ) is non-Zeno
p , {(q , {z })}1: if there exists (s, δ 0 ) in N ZSet such that δ 0 ⊆ δ then0≤x=z
τx>3, z >3, a2:
return true;
S2,x ≥ 1
S2,x ≥ 1,{x}S2,x ≥ 1,ø
{x, z }
3: end if
a4: if there exists (s, δ 0 ) in ZSet such that δ ⊆ δ 0 thenZG(A)GZG(A){x, z }
p , {(s5:, {z })}
return false;
0≤x=zx>0, z >0, az >0, a6:
end
ifFig. 7. A guessing zone graph with self-loop τ -transitions removed 0<x<=3,{x, z }{z }7: construct GZG(A, s, δ);
8: for all (s0 , δ 0 ) in GZG(A, s, δ) doτ
S1
S1,x ≥ 0,{x}S1,x ≥ 0,ø
9:
if (s0 , δ 0 ) is non-Zeno by Theorem 2 thenBe, {x}
10:add (s0 , δ 0 ) into N ZSet;e, {x}e,{x}x = 0, e
11:
else
S2
S3
12:
add (s0 , δ 0 ) into ZSet;τ
S2,x ≥ 0,ø
S2,x ≥ 0,{x}13:
end ifx = 0, e, {x}x = 0,
14:
return true iff it is non-Zeno by Theorem 2;
x = 0, e
S1,x ≥ 0e, {x}
15: end fore1P
x(a)≥Implementation
1 e1

0

0

0

0

0

1

A

0

2

2

0

0

0

1

e
S2,x ≥ 0

ZG(B)
e
e

S3,x ≥ 0τ

S3,x ≥ 0,{x}01S3,x ≥ 0,ø

GZG(B)

Fig. 8. A guessing zone graph with zero checks

non-Zeno path, can be found in this guessing zone graph. Fig. 8
shows a timed automaton with zero-checks, together with thecorresponding zone graph and guessing zone graph (with self-loopτ -transitions removed). Obviously, there are no non-Zeno runs in
automaton B . This is reflected in the guessing zone graph, where
the infinite path in the graph (containing the two states labeledwith S2 , x ≥ 0, {x} and S3 , x ≥ 0, {x} respectively) does notcontain a clear node.
Theorem 2: A node in GZG(A, s, δ) is non-Zeno if andonly if it can reach a strongly connected component (SCC) in
GZG(A, s, δ) which contains a clear node and a path which
visits every node and edge in the SCC is unblocking.
Proof: The proof follows the proof of Theorem 2 in [23].
Intuitively, if a node in GZG(A, s, δ) can reach such an SCC,
there must be an infinite run starting with the node such thatneither reasons why the run disallows time from elapsing unboundedly is possible. Thus, function witness(sp , Xq , δ, P, Q)
can be realized with the following steps. Firstly, we extract theset of states of the implementation as (sp , δ[Cp ]) and build
GZG(P, sp , δ[Cp ]). Secondly, by analyzing GZG(P, sp , δ[Cp ])we answer whether (sp , δ[Cp ]) is non-Zeno. Similarly, we answer
whether (sq , δ[A]) is non-Zeno for every (sq , A) ∈ Xq . If
(sp , δ[Cp ]) is non-Zeno and all (sq , δ[A]) are Zeno, we return
true. The above method is computationally expensive as the worst
case complexity of constructing the guessing zone graph andchecking whether it contains one such SCC is |ZG| · (|C| + 1)2
where |ZG| is the size of the zone graph and |C| is the number ofclocks. In practice, the algorithm can be improved by constructing
only a small part of the guessing zone graph [23].
Furthermore, we can improve the above approach for implementing function witness by caching the states which have been
identified as Zeno or non-Zeno. To see how it works, let us first
implement a function nz(s, δ, A, N ZSet, ZSet) which takes anabstract state (s, δ) and the corresponding timed automaton A
as inputs and returns true if and only if (s, δ) is non-Zeno.
The implementation of the function is shown as Algorithm 1.
We maintain two variables N ZSet and ZSet which are setsof abstract states which are known to be non-Zeno and Zeno
respectively. Given a new abstract state (s, δ), if there is a nonZeno state (s, δ 0 ) in N ZSet such that δ 0 ⊆ δ , (s, δ) is non-Zeno.
Similarly, if there is a state (s, δ 0 ) in ZSet such that δ ⊆ δ 0 ,(s, δ) is Zeno. Otherwise, we construct GZG(A, s, δ) and relyon Theorem 2 to answer whether (s, δ) is non-Zeno or not, while
updating the two sets N ZSet and ZSet accordingly. We further
remark that we only need to keep the maximal elements in N ZSet
and ZSet. That is, any state (s, δ) in N ZSet (or ZSet) can beomitted if there exists a state (s, δ 0 ) such that δ 0 ⊆ δ (or δ ⊆ δ 0 ).
In other words, N ZSet and ZSet are anti-chains [1], [40].
The detailed implementation of witness(sp , Xq , δ, P, Q)
is presented in Algorithm 2. It maintains four global variables:
N ZSetp , N ZSetp , N ZSetq , ZSetq . In particular, N ZSetp(and ZSetp ) is a set of abstract states which are known to be
non-Zeno (and Zeno) in P . Similarly, N ZSetq (and ZSetq ) is aset of abstract states which are known to be non-Zeno (and Zeno)
in Q. The following establishes the correctness of Algorithm 2.
Lemma 1: witness(sp , Xq , δ, P, Q) returns true only if(sp , Xq , δ) contains a witness state of C(P) ⊗ det(C(Q)).
Proof: Given a set of states (s, δ) of C(A), Algorithm 1 returns
true if and only if (s, δ) contains a non-Zeno state By Theorem 2.
Recall that (sp , Xq , δ) encodes a set of states of the form (s, X)
of C(P) ⊗ det(C(Q)). Algorithm 2 returns true only at line 11.
Because of line 5, (sp , Xq , δ) must encode a state (s, X) suchthat s is non-Zeno in C(P), by the correctness of Algorithm 1.
Because of line 6 to 10, by the correctness of Algorithm 1, statesin X must be all Zeno.
Furthermore, because of line 1-3, either (s, X) has anincoming transition labeled with an event in Σ (since alltransitions in Zr are labeled with events) or there is a state(s0 , X 0 ) which does and (s, X) can be reached from (s0 , X 0 ) via
time delay only. In the latter case, X 0 must be Zeno (because ofline 6 to 10) and by the definition of non-Zenoness, s0 must be
non-Zeno. In either case, (sp , Xq , δ) contains a witness state and10

Algorithm 2: Function witness(sp , Xq , δ, P, Q)(only if) If there is a reachable state (sp , Xq , δ) in Zr
such that witness(sp , Xq , δ, P, Q) returns true, by Lemma 1,(sp , Xq , δ) contains a witness state. By Proposition 1, there isa witness state in C(P) ⊗ det(C(Q)). By Theorem 1, L(P) ⊆L(Q) does not hold. Thus, the theorem holds.


Input: P and Q and a state (sp , Xq , δ) of Zr
Output: true iff (sp , Xq , δ) contains a witness state
1: if (sp , Xq , δ) is the initial state of Zr then2:
return false;
3: end if
4: let N ZSetp , N ZSetp , N ZSetq , ZSetq be empty sets;
5.2 Simulation Reduction
5: if nz(sp , δ[Cp ], P, N ZSetp , ZSetp ) is true then
Let Fr be the set states of in Zr such that function witness
6:
for all (sq , A) ∈ Xq do
returns true. We have so far reduced the language inclusion
7:
if nz(sq , δ[A], Q, N ZSetq , ZSetq ) is true then checking problem to the problem of checking whether a state in8:
return false;
Fr is reachable. Next, we improve the reachability analysis by
9:
end ifexploring simulation relation in Zr with respects to Fr .
10:
end forIn the following, we first show that the lower-upper bounds
11:
return true;(hereafter LU-bounds) simulation relation defined in [6] can be
12: end if
extended to a simulation relation in Zr with respects to Fr . We
13: return false;
define two functions L and U . Given a state s in Zr and aclock x ∈ Cp ∪ Z , we perform a depth-first-search to collectthus, the lemma holds.
 all transitions reachable from s without going through a transition
which resets x. Next, we set L(s, x) (resp. U (s, x)) to be theLemma 2: If there is a state (sp , Xq , δ) in Zr containing a maximal constant k such that there exists a constraint x > k or
witness state of C(P) ⊗ det(C(Q)), there is a reachable state x ≥ k (resp. x < k or x ≤ k ) in a guard of those transitions. If(s0p , Xq0 , δ 0 ) in Zr such that witness(s0p , Xq0 , δ 0 , P, Q) returns such a constant does not exist, we set L(s, x) (resp. U (s, x)) to−∞. We remark that L(s, x) is always the same as U (s, x) for atrue.
clock in Z because both guard conditions and their negations are
Proof: If (sp , Xq , δ) contains a witness state (s, X) such used in constructing Zr .
Next, we define a relation between two zones using thethat s is non-Zeno and X is Zeno, the condition at line 1 of
witness(sp , Xq , δ, P, Q) must be false, since (s, X) must has LU-bounds and show that the relation constitutes a simulation
an incoming transition labeled with an event by definition. By relation. Given two clock valuations v and v 0 at a state s andthe correctness of Algorithm 1, the condition at line 5 must be the two functions L and U , we write v 4LU v 0 if for eachtrue. Next, we analyze two cases. If all other states contained in clock c, either v 0 (c) = v(c) or L(s, c) < v 0 (c) < v(c) or(sp , Xq , δ) are witness states, witness(sp , Xq , δ, P, Q) returns U (s, c) < v(c) < v 0 (c). Given two zones δ1 and δ2 , we write
true at line 11. Otherwise, it returns false at line 8 because there δ1 4LU δ2 to denote that for all v1 ∈ δ1 , there is a v2 ∈ δ2 suchis a state (s0 , X 0 ) in (sp , Xq , δ) such that X 0 is not Zeno. In the that v1 4LU v2 . The following shows that 4LU constitutes aformer case, the lemma holds. In the following, we show that in simulation relation.
the latter case, there must be state (s0p , Xq0 , δ 0 ) reachable from
Lemma 3: Let (s, X, δi ) where i ∈ {0, 1} be two states of Zr .
(sp , Xq , δ) such that witness(s0p , Xq0 , δ 0 , P, Q) returns true.
Because X is Zeno and X 0 is not, there must be a state (s, X, δ1 ) simulates (s, X, δ0 ) w.r.t. Fr if δ0 4LU δ1 .
(sq , vq ) ∈ X which is Zeno and a state (sq , vq0 ) ∈ X 0 which
is not Zeno. Thus, there must be a non-Zeno run from (sq , vq0 ) Proof: First we show that (s, X, δ0 ) ∈ Fr implies (s, X, δ1 ) ∈which is infeasible from (sq , vq ). By induction, we can show Fr . (*) If (s, δ0 [Cp ]) is non-Zeno, (s, δ1 [Cp ]) is also non-Zenothat there must be a transition which (sq , vq0 ) can fire after a because δ0 4LU δ1 implies δ0 ⊆ δ1 . (**) By definition,
number of steps whereas (sq , vq ) cannot. Let tr be the first L(sx , c) is always the same as U (sx , c) for any clock c in A,
such transition. By the construction of Z∞ , there must be at which can be seen as the classical maximal bounds discussed
least two states in Zr , one (say M ) is guard by the transition in [8]. Following the result in [8], we conclude that for all
guard of tr and the other guarded by its negation (say N ). (sx , A) ∈ X , if δ0 4LU δ1 , (sx , δ0 [A]) is non-Zeno if and only
As a result, (sq , vq0 ) can only reach M whereas (sq , vq ) can if (sx , δ1 [A]) is. Thus if witness(s, X, δ0 , P, Q) returns true atonly reach N . Furthermore, any concrete state in N reachable line 11, witness(s, X, δ1 , P, Q) must return true by (*) and (**).
Next, we show that if (s, X, δ0 ) transitions to (s0 , X 0 , δ00 )from (sq , vq ) must be Zeno (by definition). Since (sq , vq0 ) is0
an arbitrary state in X , eventually (sp , Xq , δ) would reach a through an event e, there must be a corresponding transition fromstate which contains only witness states. Thus, the lemma holds.  (s, X, δ1 ) to a state (s0 , X 0 , δ10 ) via e and δ00 4LU δ10 . By thedefinition of Zr , if (s, X, δ0 ) transitions to (s0 , X 0 , δ00 ) throughTheorem 3: L(P) ⊆ L(Q) if and only if there is no state an event e, there must be a transition (s, e, gp , Xp , s0 ) in P and(sp , Xq , δ) in Zr such that witness(sp , Xq , δ, P, Q) returns δ00 is ([Y ∪ Xp := 0](δ0 ∧ g ∧ gp ))↑ , where g ∈ Cons(e, X)
and Y is a certain set of clocks. By Lemma 3 of [6], we cantrue.
show that δ0 ∧ g ∧ gp is not false implies δ1 ∧ g ∧ gp is not
Proof: (if) If L(P) ⊆ L(Q) does not hold, by Theorem 1, there false (since δ0 4LU δ1 ) and hence there must be a corresponding
is a witness state in C(P) ⊗ det(C(Q)). By Proposition 1, there transition from (s, X, δ1 ) to a state (s0 , X 00 , [Y ∪ Xp :=is a state in Zr which contains a witness state. By Lemma 2, there 0](δ1 ∧ g ∧ gp )). Next, following [6], we can show thatis a state (sp , Xq , δ) in Zr such that witness(sp , Xq , δ, P, Q) [Y ∪ Xp := 0](δ0 ∧ g ∧ gp ) 4LU [Y ∪ Xp := 0](δ1 ∧ g ∧ gp ).
Lastly, we show that X 00 = X 0 . By definition, X 00 is a set of
returns true.

11

states of S∞ such that for any (s00 , A00 ) ∈ X 00 , there exists a state(s, A) ∈ X and a transition ((s, A), e, gs , Y, (s00 , A00 )) ∈ T∞such that δ1 ∧ gp ∧ g ∧ gs is not false. X 0 is similarly defined.
Since δ0 4LU δ1 , δ1 ∧ gp ∧ g ∧ gs is not false if δ0 ∧ gp ∧ g ∧ gs is
not false. Thus, X 0 ⊆ X 00 . Next, we show that if δ0 ∧ gp ∧ g ∧ gs
is false, then δ1 ∧ gp ∧ g ∧ gs is false and hence every state not in
X 0 is not in X 00 and thus X 0 = X 00 . Thus the lemma holds. With the above lemma, given an abstract state (s, X, δ) of Zr ,we can enlarge the time constraint δ so as to include all clock
valuations which are simulated by some valuations in δ withoutchanging the result of reachability analysis. In the following, we
write LU (δ) to denote the set {v|∃v 0 ∈ δ · v 4LU v 0 }. Noticethat we may not be able to represent this set as a convex time
constraint and there are techniques to get around this problem [6].
We construct an LTS, denoted as ZrLU which replaces each state(s, X, δ) in Zr with (s, X, LU (δ)). We denote the successors ofa state pq in ZrLU as post(pq, ZrLU ). By a simple argument, we
can show that there is a reachable witness state in Zr if and only
if there is a reachable witness state in ZrLU .
5.3

The Algorithm

Lastly, we present an on-the-fly algorithm for the language
inclusion checking with non-Zenoness. Let ZrLU be thetuple (S, Init, Σ, T ) where Init is a set (initp , Inits ,LU ((Cp = 0 ∧ z0 = 0)↑ )). Algorithm 3 constructs ZrLU
on-the-fly while performing reachability analysis with simulation
reduction and non-Zenoness checking. It maintains two data
structures. One is a set working which stores states in S which
are yet to be explored. The other is a set done which contains
states which have already been explored. Initially, working is
set to be Init and done is empty. During the loop from line 3 toline 14, each time a state is removed from working and added
to done. If the state is a witness state, we return false at line 7.
We generate successors of ps at line 9, and they are added into
working so that they are explored later. Lastly, we return true
at line 15 after exploring all states. The following theorem statesthat the algorithm always produces correct results.
Theorem 4: Algorithm 3 returns true if and only if L(P) ⊆ L(S).
Proof Given a state ps in ZrLU , we define distance Dist(ps) ∈N ∪{∞} as the length of the shortest trace for ps to reach a state in
Fr . If no witness state can be reached from ps, Dist(ps) = ∞.
Dist(ps) = 0 if and only if ps is a witness state. Next, welift the function to a set of states. Given a set Y of states of
ZrLU , if Y = ∅ then Dist(Y ) = ∞, otherwise Dist(Y ) =minps∈Y Dist(ps). It can be proven that the loop in Algorithm 3preserves the following two invariants.
••

There exists a witness state ps in working ∪ done if andonly if ps is reachable from some state in Init.
If there is a reachable witness state, Dist(done) >Dist(working).

Algorithm 3 returns false only at line 7. In such a case,a state in Fr is reachable from Init by the first invariant
and thus L(P) ⊆ L(S) does not hold. Algorithm 3 returns
true only when working is empty, which implies that
Dist(done) > Dist(working) is not true. By the second
invariant, L(P) ⊆ L(S) holds. Thus, the theorem holds.


Algorithm 3: Language Inclusion Checking
1: let working := Init;
2: let done := ∅;3: while working 6= ∅ do4:take ps = (sp , Xs , δ) out from working ;5:
add ps into done;
6:
if witness(sp , Xs , δ) returns true then7:
return false;8:
end if9:
for all (s0p , Xs0 , δ 0 ) ∈ post(ps, ZrLU ) do
10:if (s0p , Xs0 , δ 0 ) ∈/ done then11:put (s0p , Xs0 , δ 0 ) into working ;12:
end if13:
end for
14: end while
15: return true;
Next, we establish a sufficient condition for the termination of thealgorithm.
Theorem 5: Let S be the set of states of ZrLU . If S is finite,
Algorithm 3 is terminating.

The above theorem implies that our algorithm always terminates
if the clock boundedness condition defined in [5] is satisfied. The
clock boundedness condition is satisfied if the number of clocks
in Zr is bounded. It has been shown in [5] that if the boundedness
condition is satisfied, Zr and hence ZrLU have a bounded numberof clocks and the set S is finite (assuming that maximum ceilingzone normalization is applied).

6

E VALUATION

Our method has been implemented with 46K lines of C# codeand integrated into the PAT model checker [32]. In our implementation, convex zones are encoded as difference bound matrix(DBM) and zone operations are casted to operations on DBM.
Interested readers are referred to [7], [8] for details on DBM
implementation. Note that in our setting, a zone may not be
convex, e.g., x > 2 ∨ y < 3 (due to negation used in constructing
Zr ), and thus cannot be represented as a single DBM. Such nonconvex zones can be represented either as a difference bound logic
formula, as shown in [4], or as a set of DBMs. In this work,
the latter approach is adopted for efficiency. In the following,
we evaluate our approach in order to show the feasibility of
our algorithm. All experiment data are obtained using a PC withIntel(R) Core(TM) i7-2600 CPU at 3.40 GHz and 8.0 GB RAM.
In the first empirical study, we model and verify benchmark
timed systems using our semi-algorithm and evaluate its performance. The objective is to show our approach is reasonably
scalable (i.e., terminates within a reasonable amount of time) inverifying these systems. The benchmark systems include Fischer’smutual exclusion protocol (Fischer for short), Lynch-Shavit’s
mutual exclusion protocol (Lynch), railway control system (Railway), and CSMA/CD protocol (CSMA). The results are shownin Table 1 where symbol ‘-’ means either the verification time
is more than 2 hours or out-of-memory exception happens. The
systems are all built as networks of timed automata, and thenumber of processes is shown in column ‘System’. The verified
properties are requirements on the systems specified using timed

12

automata (following the timed patterns documented in [17], [19]).
Some of the properties contain one timed automaton with one
clock, while some are networks of timed automata with morethan one clock (i.e., one clock for each timed automaton). In thetable, column ‘|Cq |’ is the number of clocks in the specification.
The systems in the same group, e.g., Lynch*4 and Lynch*5,
have the same specification. Column ‘Det’ shows whether the
specification is deterministic or not. The results of our semialgorithm are shown in column ‘Non-Zenoness with Reduction’,
which is compared with the algorithm without the assumption of
non-Zenoness (column ‘without Non-Zenoness’). In order to show
the efficiency of the simulation reduction, we also present theresults of the algorithm without simulation reduction, as shownin column ‘Non-Zenoness without Reduction’. The number oftransitions includes the transitions when constructing the product,
and the transitions generated in Algorithm 2.
The results in Table 1 show that in all these cases, our semialgorithm terminates, which is partly due to the fact that theproperties people verify these systems against are often not very
complicated. Compared to language inclusion checking without
non-Zenoness, checking with non-Zenoness incurs quite somecomputational over-head, mainly due to the construction (formultiple times) of the guessing zone graphs. Lastly, it is evident
that the simulation reduction is helpful in reducing the number of
explored transitions and consequently the checking time.
In the second empirical study, we investigate how often oursemi-algorithm terminates. We extend the approach on generating
non-deterministic finite automata in [33] to automatically generaterandom timed automata, and then apply our semi-algorithm for
language inclusion checking with non-Zenoness. Without loss ofgenerality, a generated timed automaton has always one initialstate and the alphabet is {0, 1}. In addition, the following parameters are used to control the random generation process: thenumber of state |S|, the number of clocks |C|, a parameter Dt fortransition density and a clock ceiling. We generate k transitions(and hence the transition density for the events in the alphabet isDt = k/(2|S|)) and distribute the transitions randomly amongall |S| states (the two events 0 and 1 are also distributed on thetransitions where the number for event 0 is num = k/2 and theone for event 1 is (k−num)). For instance, if |S| is set to be 6 and
Dt is set to be 1.1, we randomly generate 13 transitions (round off
to the nearest integer). For each transition, the clock constraint andthe resetting clocks are generated randomly according to the clock
ceiling. We remark that if both implementation and specification
models are generated randomly, language inclusion almost always
fails. Thus, in order to have cases where language inclusion does
hold, we generate a separate group of implementation specification
pairs by generating an implementation first, and then randomly
adding 20% transitions to obtain the specification.
The experimental results are shown in Table 2. The column|S| and |C| show the number of states and clocks. For eachdifferent combinations of |S|, |C| and Dt, we compute threenumbers, namely a, b and c respectively. a is the percentage ofthe specification satisfying the clock boundedness condition (andtherefore being determinizable [5]). b is the percentage of cases inwhich Algorithm 3 without non-Zenoness checking terminates. cis the percentage of cases in which Algorithm 3 terminates. The
gap between a and c thus shows the effectiveness of our approachon timed automata which may be non-determinizable. The gap
between b and c show how often non-Zenoness checking helps
to make language inclusion checking terminating. Additionally,it evidences that non-Zenoness is prevalent in language inclusion
checking. We generate 500 random pairs to calculate each number.
It can be observed that in all cases c ≥ b > a. b is always
larger than a because even if the specification may not be deteminzable, since Algorithm 3 is on-the-fly, it may still terminate aslong as a violation of the language inclusion is identified. c is nosmaller than b because as soon as non-Zenoness checking helps
to identify a state containing a witness state, we do not have tocontinue exploring from that state, which may contribute to thetermination.
It can be observed that there is co-relation between transition
density Dt and the terminating percentage, i.e., value of a, b andc. For instance, when Dt ≤ 0.8, the terminating percentage isquite high, which implies that our semi-algorithm often terminates.
In general, the lower the density is, the more likely that ourapproach terminates. In order to have some indication on whether
our semi-algorithm would terminate verifying systems against
common timed property patterns [17], [19] and the benchmark
systems, we calculate the transition density of the common timed
property patterns and the benchmark systems. We find that all themodels have transition densities less than or equal to 1.0 except
the absence pattern (refer to [17] for details on the pattern). Basedon the results presented in Table 2, we conclude that in practice,
our semi-algorithm has a relatively high probability (i.e., ≥ 0.6)
of being terminating.

7

C ONCLUSION

In summary, the contributions of this work are twofold. First, wedevelop a zone-based approach for language inclusion checkingof timed automata with non-Zenoness, which is further combinedwith simulation reduction for better performance. Furthermore,
we investigate when the semi-algorithm is terminating. Secondly,
we implement the semi-algorithm in the PAT framework andapply it to benchmark systems. As far as the authors know, ourimplementation is the first tool which supports language inclusion
checking for timed automata, with non-Zenoness. As for the future
work, we would like to investigate further optimization techniques
so that our approach is more scalable.

ACKNOWLEDGEMENT
This work was supported by National Natural Science Foundationof China (61602412, 61572426, U1509214, 61373033), and theresearch project from Singapore University of Technology and
Design (T2MOE1303).

R EFERENCES
[1]

[2]

[3]
[4]
[5]

P. A. Abdulla, Y.-F. Chen, L. Holk, R. Mayr, and T. Vojnar. Whensimulation meets antichains. In Proceedings of the 16th International
Conference on Tools and Algorithms for the Construction and Analysis
of Systems (TACAS ’10), pages 158–174, 2010.
P. A. Abdulla, J. Ouaknine, K. Quaas, and J. Worrell. Zone-Based
Universality Analysis for Single-Clock Timed Automata. In Proceedingsof International Symposium on Fundamentals of Software Engineering,
pages 98–112, 2007.
R. Alur and D. L. Dill. A Theory of Timed Automata. Theory ofComputer Science, 126(2):183–235, 1994.
R. Alur, L. Fix, and T. A. Henzinger. Event-clock Automata: A Determinizable Class of Timed Automata. Theoretical Computer Science,
211:253–273, 1999.
C. Baier, N. Bertrand, P. Bouyer, and T. Brihaye. When Are Timed
Automata Determinizable? In Proceedings of 36th International Collogquium on Automata, Languages and Programming, pages 43–54,
2009.

13

TABLE 1
Experiments on Language Inclusion Checking with Non-Zenoness
System|Cq |Det

Fischer*5
Fischer*6
Fischer*7
Fischer*4
Fischer*5
Lynch*4
Lynch*5
CSMA*5
Railway*6

1
1
1
2
2
1
1
1
1

Yes
Yes
Yes
No
No
Yes
Yes
Yes
Yes

without Non-Zenonessstatestransitions
time(s)
998
2263
0.1
4410
10144
0.9
20044
47060
6.3
1820
3917
0.4
8456
20142
2.5
903
2150
0.1
3852
11725
0.8
2384
5645
0.7
26731
39589
4.2

Non-Zenoness without Reduction
statestransitions
time(s)
1603
61646
29.9
7065
289698138.3
31307
1378184881.9
3938
12293475.1
21604
795771589.8
2225
13694554.2
16193
1293511519.1
325557631473.4
22005
4818205
1273.7

Non-Zenoness with Reduction
statestransitions
time(s)
1603
45178
14.9
7065
21730373.3
31307
1056986
457.4
3938
85900
49.1
21604
530577450.4
2225
12313530.8
16193
1157550370.2
323004445233.3
22005
2671729686.5

TABLE 2
Experiments on Language Inclusion Checking with Non-Zenoness for Random Timed Automata

[6]

|S|

|C|

4
4
4
6
6
6
8
8
8

1
2
3
1
2
3
1
2
3

a
0.97
0.94
0.96
0.98
0.98
0.98
0.99
0.99
0.99

Dt = 0.6
b
c
0.99
0.99
0.99
0.99
0.99
0.99
1.00
1.00
0.99
0.99
0.99
0.99
1.00
1.00
0.99
1.00
1.00
1.00

a
0.76
0.70
0.73
0.89
0.88
0.90
0.75
0.75
0.73

Dt = 0.8
b
c
0.95
0.96
0.88
0.90
0.86
0.87
0.97
0.98
0.96
0.97
0.96
0.97
0.91
0.91
0.89
0.90
0.89
0.88

a
0.65
0.56
0.57
0.49
0.43
0.41
0.40
0.36
0.35

G. Behrmann, P. Bouyer, K. G. Larsen, and R. Pelánek. Lower and Upper
Bounds in Zone-based Abstractions of Timed Automata. International
Journal on Software Tools for Technology Transfer, 8(3):204–215, 2004.
[7] G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Y. Efficient Timed Reachability Analysis Using Clock Difference Diagrams.
In Proceedings of 11th International Conference on Computer Aided
Verification (CAV 99), page 341353, 1999.
[8] J. Bengtsson and Y. Wang. Timed Automata: Semantics, Algorithms andTools. In Lectures on Concurrency and Petri Nets, pages 87–124, 2004.
[9] N. Bertrand, A. Stainer, T. Jéron, and M. Krichen. A Game Approach to
Determinize Timed Automata. In Proceedings of the 14th International
Conference on Foundations of Software Science and Computational
Structures (FOSSACS ’11), pages 245–259, 2011.
[10] D. Beyer, C. Lewerentz, and A. Noack. Rabbit: A Tool for BDD-based
Verification of Real-Time Systems. In CAV, pages 122–125. Springer,
2003.
[11] P. Bouyer. Forward Analysis of Updatable Timed Automata. Formal
Methods in System Design, 24(3):281–320, 2004.
[12] H. Bowman and R. Gómez. How to Stop Time Stopping. Formal Aspectsof Computing, 18(4):459–493, 2006.
[13] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine.
Kronos: A Model-Checking Tool for Real-Time Systems. In CAV,
volume 1427 of LNCS, pages 546–550. Springer, 1998.
[14] S. Cattani and M. Z. Kwiatkowska. A Refinement-based Process Algebra
for Timed Automata. Formal Aspects of Computing, 17(2):138–159,
2005.
[15] K. Chatterjee and V. S. Prabhu. Synthesis of Memory-efficient Real-timeControllers for Safety Objectives. In HSCC, pages 221–230. ACM, 2011.
[16] D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for Language Inclusion
Using Simulation Preorders. In CAV, pages 255–265, 1991.
[17] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property Specification
Patterns for Finite-State Verification. In Proceedings of the 2nd Workshop
on Formal Methods in Software Practice (FMSP ’98), pages 7–15, 1998.
[18] R. Gómez and H. Bowman. Efficient Detection of Zeno Runs in
Timed Automata. In FORMATS, volume 4763 of LNCS, pages 195–210.
Springer, 2007.
[19] V. Gruhn and R. Laue. Patterns for Timed Property Specifications.
Electronic Notes in Theoretical Computer Science, 153(2):117–133,
2006.
[20] T. A. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital

Dt = 1.0
b
c
0.89
0.89
0.80
0.81
0.74
0.75
0.72
0.72
0.61
0.66
0.58
0.61
0.55
0.63
0.52
0.61
0.49
0.60

a
0.48
0.39
0.41
0.37
0.30
0.29
0.25
0.25
0.20

Dt = 1.1
b
c
0.70
0.70
0.56
0.57
0.55
0.62
0.53
0.61
0.43
0.54
0.40
0.50
0.38
0.49
0.36
0.51
0.31
0.52

a
0.11
0.18
0.10
0.18
0.11
0.14
0.06
0.03
0.03

Dt = 1.3
b
c
0.22
0.27
0.23
0.31
0.17
0.27
0.25
0.32
0.17
0.33
0.18
0.36
0.07
0.25
0.05
0.24
0.05
0.15

Clocks? In Proceedings of 19th International Colloquium on Automata,
Languages and Programming (ICALP ’92), pages 545–558, 1992.
[21] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic
Model Checking for Real-time Systems. Journal of Information andComputation, 111(2):193–244, 1994.
[22] F. Herbreteau and B. Srivathsan. Efficient On-the-Fly Emptiness Checkfor Timed Büchi Automata. In ATVA, pages 218–232, 2010.
[23] F. Herbreteau, B. Srivathsan, and I. Walukiewicz. Efficient Emptiness
Check for Timed Büchi Automata. Formal Methods in System Design,40(2):122–146, 2012.
[24] M. Krichen and S. Tripakis. Conformance Testing for Real-Time
Systems. Formal Methods in System Design, 34(3):238–304, 2009.
[25] K. G. Larsen, P. Petterson, and Y. Wang. UPPAAL in a Nutshell. Journal
on Software Tools for Technology Transfer, 1(1-2):134–152, 1997.
[26] J. Ouaknine and J. Worrell. On The Language Inclusion Problem forTimed Automata: Closing a Decidability Gap. In Proceedings of the
19th Annual IEEE Symposium on Logic in Computer Science, pages 54–
63, 2004.
[27] J. Ouaknine and J. Worrell. Safety metric temporal logic is fully
decidable. In Proceedings of the 12th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems,
TACAS’06, pages 411–425, 2006.
[28] J. Raskin and P. Schobbens. The Logic of Event Clocks - Decidability,
Complexity and Expressiveness. Journal of Automata, Languages, andCombinatories, 4(3):247–286, 1999.
[29] T. G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis,
Stanford Uni., 1993.
[30] A. W. Roscoe. On the Expressive Power of CSP Refinement. Formal
Aspects of Computing, 17(2):93–112, 2005.
[31] P. V. Suman, P. K. Pandya, S. N. Krishna, and L. Manasa. Timed
Automata with Integer Resets: Language Inclusion and Expressiveness.
In Proceedings of 6th International Conference on Formal Modeling andAnalysis of Timed Systems (FORMATS 08), pages 78–92, 2008.
[32] J. Sun, Y. Liu, J. S. Dong, , and J. Pang. PAT: Towards flexible verification
under fairness. In Proceedings of the 21st International Conference on
Computer Aided Verification (CAV ’09), pages 709–714, 2009.
[33] D. Tabakov and M. Y. Vardi. Experimental evaluation of classical automata constructions. In Proceedings of the 12th international conference
on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’05), pages 396–411, 2005.
[34] S. Tripakis. Verifying progress in timed systems. In Proceedings of the14

5th International AMAST Workshop on Formal Methods for Real-Timeand Probabilistic Systems (ARTS ’99), pages 299–314, 1999.
[35] S. Tripakis, S. Yovine, and A. Bouajjani. Checking Timed BüchiAutomata Emptiness Efficiently. FMSD, 26(3):267–292, 2005.
[36] Stavros Tripakis, Sergio Yovine, and Ahmed Bouajjani. Checking timedbüchi automata emptiness efficiently. Formal Methods in System Design,
26(3):267–292, 2005.
[37] F. Wang. Symbolic Verification of Complex Real-Time Systems with
Clock-Restriction Diagram. In Formal Techniques for Networked andDistributed Systems, pages 235–250. Springer, 2002.
[38] T. Wang, J. Sun, Y. Liu, X. Wang, and S. Li. Are timed automata
bad for a specification language? language inclusion checking for timed
automata. In Tools and Algorithms for the Construction and Analysis
of Systems - 20th International Conference, TACAS 2014, Held as Partof the European Joint Conferences on Theory and Practice of Software,
ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, pages
310–325, 2014.
[39] Y. Wang, P. Pettersson, and M. Daniels. Automatic Verification of RealTime Communicating Systems by Constraint Solving. In Proceedingsof the 7th International Conference on Formal Description Techniques,
pages 223–238, 1994.
[40] M. D. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains:
A New Algorithm for Checking Universality of Finite Automata. In
Proceedings of the 18th International Conference on Computer Aided
Verification (CAV ’06), pages 17–30, 2006.