Model Checking Bounded Continuous-time
Extended Linear Duration Invariants
Jie An and Miaomiao Zhang*

Naijun Zhan*

School of Software Engineering,
Tongji University, Shanghai, China{1510796,miaomiao}@tongji.edu.cn

State Key Lab. of Comp. Sci., Institute of Software,
CAS & Uni. of CAS, Beijing, China
znj@ios.ac.cn

Xiaoshan Li

Wang Yi

Faculty of Science and Technology,
University of Macau, Macau, China
xsl@umac.mo

Department of Information Technology,
Uppsala University, Uppsala, Sweden
wang.yi@it.uu.se

ABSTRACT

1

Extended Linear Duration Invariants (ELDI), an important subset of Duration Calculus, extends well-studied Linear
Duration Invariants with logical connectives and the chopmodality. It is known that the model checking problem of ELDI is undecidable with both the standard continuous-time anddiscrete-time semantics [12, 13], but it turns out to be decidable if only bounded execution fragments of timed automata
are concerned in the context of the discrete-time semantics[36]. In this paper, we prove that this problem is still decidable
in the continuous-time semantics, although it is well-known
that model-checking Duration Calculus with the continuoustime semantics is much more complicated than the one withthe discrete-time semantics. This is achieved by reduction to
the validity of Quantified Linear Real Arithmetic (QLRA).
Some examples are provided to illustrate the efficiency of ourapproach.

Duration Calculus (DC) is an Interval Temporal Logic due
to Zhou, Hoare and Ravn [18]. It extends Interval Temporal
Logic [15] with the notion of duration, the integral of state
expression over the reference interval. It is designed for specifying and reasoning about real-time and embedded systems
at a high abstract level [14], and has been successfully andwidely applied in practice [23, 33].
Although the powerful expressiveness of DC is desirable
for requirement specification and analysis, it is a burden forautomatic verification as satisfiability, validity and model
checking of DC are undecidable [34], unless the use of chop(the only modality in DC), and/or negation, and/or the considered models are severely constrained [10, 11, 16, 23, 24, 28,
30, 34, 35].
In [35],of DC formulas of the form 𝑏 ≤ ℓ ≤∫︀∑︀ a subset𝑒 ⇒𝑠∈𝑆 𝑐𝑠 𝑠 ≤ 𝑀 , called Linear Duration Invariants∫︀(LDI), was identified, in which a given interval [𝑡, 𝑡′ ], 𝑠stands for the accumulated time for the presence of state 𝑠over [𝑡, 𝑡′ ], and ℓ for the length of the interval, i.e., 𝑡′ − 𝑡. So,
an LDI formula says that if the length of the interval satisfies
the constraint 𝑏 ≤ ℓ ≤ 𝑒, then over the time interval the
durations∫︀of the state expressions should satisfy the constraint∑︀𝑐𝑠 ≤ 𝑀 . LDI is indeed expressive, for instance, in𝑠𝑠∈𝑆the gas burner example [33], the safety requirement that “theproportion of leak time is no more than one-twentieth of theelapsed time for any time interval∫︀ over one minute”, can beeasily specified as ℓ ≥ 60 ⇒ 20 Leak ≤ ℓ.
In [35], it was proved that the model checking problem
of LDI against real-time automata is decidable. Real-time
automata is a specific kind of timed automata with a single
clock which is reset at each transition. Following this work,in [3, 20, 21], the authors investigated the model-checking of
LDI against more expressive models such as timed automata[1] and hybrid automata [17]. Some more efficient algorithms
for mode-checking LDI against timed automata based on

KEYWORDS
Model Checking, Duration Calculus, ELDI, Timed Automata,Quantified Linear Real Arithmetic.
* The corresponding authors.

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are notmade or distributed for profit or commercial advantage and that copies bear
this notice and the full citation on the first page. Copyrights for componentsof this work owned by others than the author(s) must be honored. Abstractingwith credit is permitted. To copy otherwise, or republish, to post on servers or
to redistribute to lists, requires prior specific permission and/or a fee. Request
permissions from permissions@acm.org.
HSCC ’18, April 11–13, 2018, Porto, Portugal© 2018 Copyright held by the owner/author(s). Publication rights licensed to
the Association for Computing Machinery.
ACM ISBN 978-1-4503-5642-8/18/04. . . $15.00
https://doi.org/10.1145/3178126.3178147

INTRODUCTION

graph search were proposed in [30, 31], and the results were
further extended to the networks of timed automata [32].
An interesting problem is whether it is possible to find alarger subset of DC whose model-checking problem is still
decidable. It is natural to investigate the extension of LDI
with Boolean connectives and chop modality, i.e., ELDI. Unfortunately, the satisfiability and validity of ELDI both are
undecidable in the discrete-time and continuous-time (densetime) settings according to the results in [34]. In [12, 13],
Fränzle and Hansen further proved that the model-checking
problem of ELDI against finite state machines also turns out tobe undecidable both in the discrete time and continuous time
settings. Therefore, they proposed an approximation semantics for ELDI, called doubly situation based semantics, andshowed its model-checking is decidable in the discrete time
setting with the complexity of cubic in the number of states ofthe model and linear in the size of the formula. However, further observation indicates that such approximation semantics
is too coarse to be useful in practice [12]. So, they refined thesemantics to another approximation semantics called counting semantics and reduced the model-checking problem of
ELDI to Presburger Arithmetic with the complexity of 3-fold
exponential [13]. In addition, according to their approach,
one can only prove/disprove those formulas that can be approximated to be true/false over the given model represented
by a Kripke structure, while no conclusion can be drawn inother cases. Therefore, the low efficiency and approximation
semantics hinder the application of their approach. Motivatedby their work, as an alternative, in [36] Zu et al. proved thatmodel-checking bounded ELDI against timed automata in thestandard discrete-time semantics is decidable by providing
an efficient model-checking algorithm with the complexityof singly exponential in the size of formulas and quadratic in
the number of states of the considered model, as a bounded
ELDI formula Φ is of the form 𝑏 ≤ ℓ ≤ 𝑒 ⇒ 𝜑, thus checking
whether 𝒜 |= Φ is reduced to check whether any executionof 𝒜, whose length is within [𝑏, 𝑒], satisfies 𝜑, where 𝒜 is a
timed automaton and 𝑒 is bounded.
In this paper, we investigate the model-checking problem
of bounded ELDI against timed automata in the standard
continuous-time semantics. We prove that it is still decidable.
The basic idea is that for a given timed automaton 𝒜 and abounded ELDI formula Φ, we first find the set Θ of all execution fragments of 𝒜 whose length is in between the lower
and upper bounds from the zone graph of 𝒜, and the numberof such paths is finite. Then, for each path in Θ, we construct a Quantified Linear Real Arithmetic (QLRA) formula bytaking Φ into account. Finally, we exploit REDLOG [8], acomputer algebra tool based on quantifier elimination [29], tosolve the derived QLRA formulas. Although the complexityof REDLOG is doubly exponential in the number of variablesin the worst case, REDLOG can handle QLRA formulas quite

efficiently in practice, as virtual substitution [9] can be applied to formulas that contain only polynomials with degree
no more than 4. Our experiments indicate the efficiency andscalability of our approach.
Related work. In [6, 7], the authors considered the verification and synthesis of a class of linear hybrid automata (LHA)
called reasonable LHA and their composition against different kinds of properties like safety and bounded reachability,
defined by Bounded Time Logic (BTL), and proved that they
are decidable, yet with different complexity. In general, timed
automata is a proper subset of LHA, but not comparable withreasonable LHA. In addition, bounded continuous-time ELDI
is not comparable to BTL. Certainly, the general solution
used in [6, 7] is similar to ours used in this paper, both by
reduction to the decision problem of linear arithmetic, but
their technical details are completely different.
The rest of the paper is organized as follows. Section 2
recalls some basic notions of timed automata, zones and ELDI. Section 3 explains how to find all execution fragmentswith the bounded length for a given timed automaton from its
zone graph. The algorithm of constructing a QLRA formulaaccording to a given ELDI formula and an execution fragment
is presented in Section 4. Section 5 is devoted to solving thederived QLRA formulas by quantifier elimination, following
by the complexity analysis. After presenting the implementation and experiments in Section 6, we draw a conclusion in
Section 7.

2

PRELIMINARIESIn this section, we first review timed automata (TA) as amodeling language for real-time systems and zone graph as
the symbolic representation of states of TA, then recall ELDI,
a subset of DC, as a specification logic for real-time systems.
For convenience, we fix a set of propositions 𝒫 throughout
this paper.

2.1

Timed automata

A timed automaton (TA) [1] is a finite-state automaton whichis equipped with a set of clocks, and each location is equippedwith a set of propositions from 𝒫 that hold at the location. Let
𝑋 represent the set of clocks and ∆(𝑋) be the set of clock
constraints on 𝑋, which are conjunctions of the formulasof the form 𝑥 ≤ 𝑐 or 𝑐 ≤ 𝑥, where 𝑥 ∈ 𝑋 and 𝑐 ∈ N.
Additionally, we assume that all TA are strongly non-Zeno[1], i.e., there is a non-zero constant 𝜖 ∈ R+ such that every
control cycle takes at least 𝜖 time units.
Definition 2.1 (Timed Automaton). A TA is a tuple 𝒜 =(𝐿, 𝑋, 𝐸, Σ, 𝑙0 , Λ, 𝐼), where 𝐿 is a finite set of locations, 𝑋
is a finite set of clocks, 𝐸 ⊆ 𝐿 × Σ × ∆(𝑋) × 2𝑋 × 𝐿 is atransition relation, Σ is a set of actions, 𝑙0 ∈ 𝐿 is the initial22.2

location, Λ is a mapping that assigns a subset of 𝒫 to eachlocation 𝑙 indicating all propositions in Λ(𝑙) hold in 𝑙, and 𝐼
is a mapping that assigns each location 𝑙 ∈ 𝐿 with a clock
constraint 𝐼(𝑙) ∈ ∆(𝑋), called invariant. Furthermore, aninvariant in TA must be downwards closed.

ELDI with the set 𝒫 of state variables consists of three syntactic categories, which are state expressions 𝑆, linear duration
formulas (LDFs) 𝒟, and ELDI formulas 𝜑. The BNFs forthem are given as follows:

A clock valuation is a function v : 𝑋 → R≥0 . We denotethe set of all clock valuations by ℋ. Hence a state of a TA
𝒜 is a pair (𝑙, v) ∈ 𝐿 × ℋ consisting of a location and aclock valuation. Every subset 𝜆 ⊆ 𝑋 induces a reset function
Reset𝜆 : ℋ → ℋ defined by{︃0,
if 𝑥 ∈ 𝜆Reset𝜆 v(𝑥) =v(𝑥), if 𝑥 ∈
/𝜆

𝛿0

𝛿1

𝛿2

::= 𝒟 | ¬𝜑 | 𝜑1 ∨ 𝜑2 | 𝜑1 ; 𝜑2where 𝑃 ∈ 𝒫 stands for a state variable, interpreted as a
Boolean function over time, 𝑐𝑖 s and 𝑐 are real numbers, andΩ is a finite set of indices.
∫︀
As the convention of DC, ℓ is defined as 1, denoting
the length of the reference interval. The Boolean value true,
denoted by ⊤, is defined by ℓ ≥ 0, falling in ELDI. Obviously, each ELDI formula can be represented by the form𝑏 ≤ ℓ ≤ 𝑒 ⇒ 𝜑, where 𝑏 ∈ R≥0 , 𝑒 ∈ R≥0 ∪ {∞}, and 𝜑 isdefined as above. In this paper, we only focus on the casewhen 𝑒 is bounded, i.e., in R≥0 , and will represent an ELDI
of this form by Φ, Ψ, · · ·, possibly with superscript and subscript in the sequel. Therefore, we also call ELDI with such
restriction bounded ELDI.

(1) A run 𝑟 of 𝒜 is an infinite sequence of the form
𝑎2

𝜑

::=

𝑖∈Ω

Definition 2.2 (Run and Behaviour). Let 𝒜 be a TA.
𝑎1

𝒟

0 | 𝑃 | ¬𝑆 | 𝑆1 ∨ 𝑆2
∑︁ ∫︀
::=
𝑐𝑖 𝑆𝑖 ≤ 𝑐

𝑆

We use 1 to denote the unit vector(1,. . . ,1) and 0 for zero
vector. There are two kinds of steps of a TA: discrete step𝑎and time-delay step. A discrete step is of the form (𝑙, v) −→′(𝑙′ , v′ ), if there exists (𝑙, 𝑎, 𝑔, 𝜆, 𝑙 ) ∈ 𝐸 such that v satisfies
𝑔 and v′ = Reset𝜆 (v), where 𝑎 ∈ Σ. A time-delay step is of𝑡
the form (𝑙, v) →− (𝑙, v + 𝑡1), such that for any 𝑡′ ∈ [0, 𝑡],′
v + 𝑡 1 satisfies 𝐼(𝑙), where 𝑡 ∈ R≥0 .

𝑎0Extended linear duration invariants

Definition 2.3 (Interpretation ℐ𝛽 of ELDI). Given a TA 𝒜
and one of its behaviours 𝛽, define an interpretation ℐ𝛽 of
ELDI with continuous-time semantics as follows:state expressions: given a time point 𝑡 ∈ R≥0 ∪ {0}ℐ𝛽 (0)(𝑡) = 0⎧and ℐ𝛽 (1)(𝑡) = 1;⎪
⎨1 if 𝑡𝑖 ≤ 𝑡 < 𝑡𝑖+1 ∧ 𝑃 ∈ 𝑙𝑖
ℐ𝛽 (𝑃 )(𝑡) =for some 𝑖 > 0 ;⎪⎩0 otherwiseℐ𝛽 (¬𝑆)(𝑡) = 1 − ℐ𝛽 (𝑆)(𝑡);ℐ𝛽 (𝑆1 ∨ 𝑆2 )(𝑡) = max{ℐ𝛽 (𝑆1 )(𝑡), ℐ𝛽 (𝑆2 )(𝑡)}.

𝑟 : (𝑙0 , v0 ) −→ (𝑙1 , v1 ) −→ (𝑙2 , v2 ) −→ · · ·where (𝑙0 , v0 ) is the initial state, and 𝛿𝑖 is the time 𝒜
staying in the location 𝑙𝑖 . If 𝑙𝑖 = 𝑙𝑖+1 and 𝑎𝑖 is an empty
action, the step is a time-delay step and v𝑖+1 = v+𝛿𝑖 1;otherwise, the step is a discrete step with 𝛿𝑖 = 0 andv𝑖+1 = Reset𝜆 (vi ), for 𝑖 ≥ 0.
(2) A behaviour 𝛽 corresponding to the run, is the infinite
sequence of timed locations
𝛽 : (𝑙0 , 𝑡0 )(𝑙1 , 𝑡1 ) · · · (𝑙𝑘 , 𝑡𝑘 ) · · ·durations: given an∫︀ interval [𝑡1 , 𝑡2 ], where ∫︀𝑡1 , 𝑡2 ∈ R≥0 ∪{0} and 𝑡1 ≤ 𝑡2 , 𝑆 is interpreted by ℐ𝛽 ( 𝑆)([𝑡1 , 𝑡2 ]) =∫︀ 𝑡2
ℐ (𝑆)(𝑡)𝑑𝑡.
𝑡1 𝛽that satisfies the following conditions: (1) 𝑡0 = 0; (2)for any 𝑇 ∈ R+ , there is some 𝑖 ≥ 0 such that 𝑡𝑖 ≥ 𝑇 ;(3) 𝑡𝑖 is the instant when 𝒜 enters 𝑙𝑖 , which implies
𝛿𝑖 = 𝑡𝑖+1 − 𝑡𝑖 , and 𝒜 stays in 𝑙𝑖 for 𝛿𝑖 time units.

formulas: given an interval [𝑡1 , 𝑡2 ], an ELDI formula 𝜑is interpreted by∫︀∑︀ℐ𝛽 , [𝑡1 , 𝑡2 ] |= 𝑖∈Ω 𝑐𝑖 𝑆𝑖 ≤ 𝑐 ∫︀∑︀
iff 𝑖∈Ω 𝑐𝑖 ℐ𝛽 ( 𝑆𝑖 )([𝑡1 , 𝑡2 ]) ≤ 𝑐;
ℐ𝛽 , [𝑡1 , 𝑡2 ] |= ¬𝜑 iff ℐ𝛽 , [𝑡1 , 𝑡2 ] ̸|= 𝜑;ℐ𝛽 , [𝑡1 , 𝑡2 ] |= 𝜑1 ∨𝜑2 iff ℐ𝛽 , [𝑡1 , 𝑡2 ] |= 𝜑1 or ℐ𝛽 , [𝑡1 , 𝑡2 ]|= 𝜑2 ;ℐ𝛽 , [𝑡1 , 𝑡2 ] |= 𝜑1 ; 𝜑2 iff ℐ𝛽 , [𝑡1 , 𝑡] |= 𝜑1 and ℐ𝛽 , [𝑡, 𝑡2 ] |=𝜑2 for some 𝑡 ∈ [𝑡1 , 𝑡2 ].

A zone is a clock constraint [2]. For a location, a zone is
the maximal set of clock valuations satisfying the constraint.
In a zone-graph, zones are used to denote symbolic states.
Zones and their representations based on Difference Bounded
Matrices (DBMs) are the standard data structures which havebeen implemented in several verification tools for TA, e.g.,
UPPAAL [19]. Operations over zones are well defined in[2]. Note that zone provides a more efficient representationof symbolic states than region graph [1], therefore, modelchecking algorithms for TA based on zone is more efficientthan those based on region graph.

2.3

Quantified linear real arithmetic

Quantified linear real arithmetic (QLRA) is a theory of firstorder logic, with the specific signature ⟨R, 0, +, =, <⟩, i.e.,3

in which all terms are linear. Thus, formulas of QLRA are
defined according to the following syntax:

Algorithm 1: PEF(ZoneG(𝒜), 𝑏, 𝑒) /* Finding all possible execution fragments satisfying the length bound */::= 𝑐0 + 𝑐1 𝑥1 + · · · + 𝑐𝑛 𝑥𝑛 ◃ 0 | ¬𝜑 | 𝜑1 ∧ 𝜑2 | ∀𝑥.𝜑

input : ZoneG(𝒜), the zone graph of 𝒜; [𝑏, 𝑒], an interval
output : Θ, the set of possible execution fragments whose
lengths are within [𝑏, 𝑒]
1 begin2
Θ := ∅ ;3
foreach 𝑧 ∈ 𝑍 do
4
𝜌 := 𝜀 ;5
STK.push(𝑧) ;/* STK is a stack, storing all zones
to be explored*/6
while STK ̸= ∅ do7
currentZ := STK.pop;
8
if ↑∈ currentZ.𝜏 then9currentZ := currentZ ↑ ;𝜑where 𝑐0 , 𝑐1 , . . . , 𝑐𝑛 ∈ R, ◃ ∈ {=, <}. QLRA is interpreted
in the standard way. Other notations of first-order logic andreal arithmetic are defined as usual.

3

FINDING ALL POSSIBLE BOUNDEDEXECUTION FRAGMENTS

In this section, we consider given a TA 𝒜 and an interval[𝑏, 𝑒] with 𝑏, 𝑒 ∈ R≥0 and 𝑏 ≤ 𝑒, how to find all execution
fragments of 𝒜 whose lengths are in between 𝑏 and 𝑒.
As discussed in [2], ZoneG(𝒜) is a transition graph derived
from 𝒜, can be represented by ⟨𝑍, 𝑧0 , ↦→⟩, where∙ Every 𝑧 ∈ 𝑍 stands for a zone, which is a pair (𝑙, ∆(𝑙)),where 𝑙 ∈ 𝒜.𝐿, and ∆(𝑙) is a timing constraint on∆(𝒜.𝑋)1 , denoting a symbolic state of 𝒜, i.e., a set ofclock valuations satisfying ∆(𝑙).
∙ 𝑧0 = (𝑙0 , ∧𝑥∈𝒜.𝑋 𝑥 = 0), is the initial zone.

10
11

𝑔,𝑎,𝜆

∙ ↦→ = ↑ ∪∪𝑎∈Σ −−−→, where– (𝑙1 , ∆(𝑙1 )) ↑ (𝑙2 , ∆(𝑙2 )) iff 𝑙1 = 𝑙2 ∧ ∆(𝑙2 ) = {𝑢 +𝑑 ∈ 𝐼(𝑙1 ) | 𝑢 ∈ ∆(𝑙1 ) ∧ 𝑑 ∈ R+ }. ↑ stands for adelay transition.

12
13
14

/* 𝑡 is an additional clock added
to the DBMs, reset at the
beginning of 𝜌*/
if currentZ ∧ (𝑏 ≤ 𝑡 < 𝑒) ̸= ∅ then
𝜌 := 𝜌 ∘ ⟨currentZ⟩; Θ := Θ ∪ {𝜌};if Post𝑎 (currentZ) ̸= ∅ thenforeach 𝑧 ′ ∈ Post𝑎 (currentZ) do
STK.push(𝑧 ′ );
else

15

𝑔,𝑎,𝜆

– (𝑙1 , ∆(𝑙1 )) −−−→ (𝑙2 , ∆(𝑙2 )) iff (𝑙1 , 𝑔, 𝑎, 𝜆, 𝑙2 ) ∈𝜌 := remove(𝜌, currentZ);
while Post𝑎 (Lastzone(𝜌)) have been
popped out do
𝜌 := remove(𝜌, Lastzone(𝜌));

16

𝑔,𝑎,𝜆

𝒜.𝐸 ∧ ∆(𝑙2 ) = {𝑢[𝜆] | 𝑢 ∈ ∆(𝑙1 ) ∧ 𝑔(𝑢)}. −−−→
stands for a possible discrete transition over the zone
graph derived from 𝒜.
Given a transition 𝜏 ∈↦→, 𝜏.preZ and 𝜏.postZ respectively denote the pre- and post-zone of the transition. Given a
discrete transition 𝜏 , 𝜏.𝑔, 𝜏.𝑎 and 𝜏.𝜆 denote its guard, action and the set of reset clocks, respectively. Given a zone 𝑧,
we use 𝑧.𝜏 to stand for the set of transitions outgoing from𝑧, and Post𝑎 (𝑧) for the set of zones which can be reachedfrom 𝑧 via a discrete transition, i.e., {𝑧 ′ | (𝑧, 𝑔, 𝑎, 𝜆, 𝑧 ′ ) ∈↦→for some 𝑔 ∈ ∆(𝑋), 𝑎 ∈ Σ, and 𝜆 ⊆ 𝑋}.
Given a TA 𝒜, Algorithm 1 presents a procedure for finding all possible execution fragments of 𝒜 whose lengths arewithin the given interval [𝑏, 𝑒]. The basic idea of Algorithm 1
is as follows:∙ Firstly, according to the descriptions of zone in [2, 26,27], we construct a zone graph of 𝒜 with 𝑘-normalization,
denoted by ZoneG(𝒜), the resulting zone graph. As
𝒜 has no time difference constraints as guards, thus
ZoneG(𝒜) is sound and complete w.r.t. the standard
operational semantics of 𝒜 as discussed in the previous section. Moreover, its transition relation is finite[26, 27].

17
18
19
20
21
22
23

else if currentZ ∧ (𝑡 < 𝑏) ̸= ∅ then
𝜌 := 𝜌 ∘ ⟨currentZ⟩;
if Post𝑎 (currentZ) ̸= ∅ thenforeach 𝑧 ′ ∈ Post𝑎 (currentZ) do
STK.push(𝑧 ′ );
else

24

𝜌 := remove(𝜌, currentZ);
while Post𝑎 (Lastzone(𝜌)) have been
popped out do
𝜌 := remove(𝜌, Lastzone(𝜌));

25
26
27
28
29
30
31
32

33

1 Unlike Δ(𝑋), 𝑐 ≤ 𝑥 − 𝑦 and 𝑥 − 𝑦 ≤ 𝑐 are allowed in Δ(𝑙), where 𝑥, 𝑦

are clock variables and 𝑐 is a natural number.
4else if currentZ ∧ (𝑡 ≥ 𝑒) ̸= ∅ then
𝜌 := 𝜌 ∘ ⟨currentZ⟩; Θ := Θ ∪ {𝜌};
𝜌 := remove(𝜌, currentZ) ;while Post𝑎 (Lastzone(𝜌)) have been popped
out do𝜌 := remove(𝜌, Lastzone(𝜌));return Θ𝜌′ start from (𝑙1 , ∆(𝑙1 )). Obviously, it is doable by line 3. Because 𝜌 is a real execution fragment of ZoneG(𝒜), the second
zone (𝑙2 , ∆(𝑙2 )) in 𝜌 must be a successor of (𝑙1 , ∆(𝑙1 )), andthe length of (𝑙1 , ∆(𝑙1 )), (𝑙2 , ∆(𝑙2 )) is less than 𝑒, so 𝜌′ canbe extended by appending (𝑙2 , ∆(𝑙2 )) at the end from line
10-27. We can repeat the above procedure until (𝑙𝑛 , ∆(𝑙𝑛 )) isappended to the end of 𝜌′ . Clearly, from line 10-14 and line
28-29, 𝜌′ ∈ Θ.
∙ Starting from each symbolic state in ZoneG(𝒜), we
find all execution fragments whose lengths are between𝑏 and 𝑒 using depth first search. With an implicit extra
clock 𝑡 added to the DBMs, we can easily determine
whether the length of the current execution fragment 𝜌
can reach the interval [𝑏, 𝑒] through checking whether
currentZ ∧ (𝑏 ≤ 𝑡 ≤ 𝑒) holds. STK is a stack to store
the zones to be explored. The algorithm pushes a zone 𝑧
into STK as long as the length of the derived execution
fragment by appending 𝑍 to the end of the considered
execution fragment is no more than the given upperbound 𝑒, otherwise, the head of STK will be popped.
Suppose the number of the locations of 𝒜 is 𝑁 , then
the number of such execution fragments is at most𝑒
𝑁 1+𝑁 *(1+⌈ 𝜖 ⌉) , where 𝜖 is the least dwelling time ineach control cycle of 𝒜.

4

REDUCTION TO QRLAIn this section, we present a translation from a given possible
execution fragment whose length is within the given interval
and an ELDI formula into a QLRA formula equivalently in thesense that the execution fragment satisfies the ELDI formula
iff the resulting QLRA formula is valid.
Note that for any execution fragment generated by Algorithm 1 which is a sequence of zones, we can remove those zones
without dwelling time, because (𝜑; ℓ = 0) ⇔ (ℓ = 0; 𝜑) ⇔ 𝜑always holds in DC. So, in what follows, we only consider such refined execution fragments, and denote them by
𝑧1 , 𝑧2 , . . . , 𝑧𝑘 . Moreover, for each zone 𝑧𝑖 , we introduce avariable 𝛿𝑖 to indicate the real duration on which the automaton dwells. Thus, we will denote the refined execution fragment as (𝑧1 , 𝛿1 )(𝑧2 , 𝛿2 ), . . . , (𝑧𝑘 , 𝛿𝑘 ).
Given the ELDI formula (𝑏 ≤ ℓ ≤ 𝑒 ⇒ 𝜑) and a refined
execution fragment 𝜌 = (𝑧1 , 𝛿1 ), (𝑧2 , 𝛿2 ), . . . , (𝑧𝑘 , 𝛿𝑘 ), theencoded QLRA formula is of the form 𝐿(𝜌) ⇒ 𝐿(𝜑), where𝐿(𝜌) is a QLRA formula translated from 𝜌, which entails∑︀𝑘𝑏 ≤𝑖=1 𝛿𝑖 ≤ 𝑒, and 𝐿(𝜑) is obtained from 𝜑. We will
explain the details of the translation below.

T HEOREM 3.1 (C ORRECTNESS OF A LGORITHM 1). For
any TA 𝒜 and [𝑏, 𝑒], Algorithm 1 is correct, i.e.,
Termination: the algorithm terminates;
Soundness: if 𝜌 ∈ Θ, then 𝜌 is a real execution fragmentof zones in ZoneG(𝒜) with length in [𝑏, 𝑒]; andCompleteness: if 𝜌 is a real execution fragment of zones
in ZoneG(𝒜) with length in [𝑏, 𝑒], then 𝜌 ∈ Θ.
P ROOF. For termination, we only need to prove the while
loop terminates as it is obvious that the outermost for loop
and the three innermost for loops terminate. For a given zone
𝑧, suppose there is an execution fragment 𝜌 starting from 𝑧
with 𝑁 * (1 + ⌈ 𝑒𝜖 ⌉) transitions, whose length is within [𝑏, 𝑒],where 𝑁 is the number of zones. By Pigeonhole principle,
there is a zone 𝑧 ′ with more than 1 + ⌈ 𝑒𝜖 ⌉ occurrences in 𝜌,
which implies there are ⌈ 𝑒𝜖 ⌉ control cycles in 𝜌 at least. Hence,the execution time of 𝜌 is more than 𝑒 from the assumptionthat each control cycle has 𝜖 dwelling time at least. It follows
that any execution fragment starting from 𝑧 has 𝑁 * (1 + ⌈ 𝑒𝜖 ⌉)transitions at most if its length is within [𝑏, 𝑒], and therefore,𝑒
all such execution fragments can be found in 𝑁 𝑁 *(1+⌈ 𝜖 ⌉)iterations at most. After finding out all such execution fragments, no zone can be pushed in STK any more, but at least
one zone is popped out from STK in each iteration (see lines
10-32). This implies that the while loop must terminate.
For soundness, suppose 𝜌 ∈ Θ. Obviously, 𝜌 is an execution fragment of ZoneG(𝒜) by Algorithm 1. Additionally,
from line 10-32, it follows that 𝜌’s length is within [𝑏, 𝑒],because on the one hand, 𝜌’s length cannot be less than 𝑏as 𝜌 ̸∈ Θ otherwise; on the other hand, 𝜌’s length cannot
be greater than 𝑒, as the last zone in 𝜌 cannot be appended
otherwise according to line 28-32.
For completeness, suppose 𝜌 = (𝑙1 , ∆(𝑙1 )), ..., (𝑙𝑛 , ∆(𝑙𝑛 ))is a real execution fragment of ZoneG(𝒜) whose length iswithin [𝑏, 𝑒]. Thus, we can construct a 𝜌′ ∈ Θ as follows. Let

Deriving timing constraints from refined execution fragments: Given an execution fragment 𝜌 = (𝑧1 , 𝛿1 ), (𝑧2 , 𝛿2 ),. . . , (𝑧𝑘 , 𝛿𝑘 ) and initial value x0 = (𝑥01 , · · · , 𝑥0𝑚 ) (suppose
𝑋 = {𝑥1 , . . . , 𝑥𝑚 }), Algorithm 2 derives a QLRA formula
to stand for the timing constraint on the dwelling times 𝛿𝑖 s
and the initial value x0 derived from 𝜌. Essentially, the constraint on the dwelling times 𝛿𝑖 s is derived by considering thefollowing three aspects:∙ each 𝛿𝑖 should be non-negative;∙ their sum should be within the length interval of con∑︀𝑘sidered execution fragments, i.e., 𝑏 ≤ 𝑖=1 𝛿𝑖 ≤ 𝑒;
∙ the constraint derived from the corresponding zone bytaking the initial values of clocks into account.
Encoding ELDI formula: Given an execution fragment 𝜌 =(𝑧1 , 𝛿1 ), . . . , (𝑧𝑛 , 𝛿𝑛 ) and an ELDI formula 𝜑, the encoding
procedure is done by the structure of 𝜑 as follows:∙ If 𝜑 is an atomic formula of the form 𝑏 ≤ ℓ ≤ 𝑒 ⇒𝒟, we mainly focus on how to encode
𝒟. ∫︀Suppose∫︀𝒟 contains 𝑑 duration expressions 𝑆1 , . . . , 𝑆𝑑 . We
use 𝑒𝑖𝑗 to denote the duration that 𝑆𝑖 holds at 𝑧𝑗 , for5

Termination: the algorithm terminates;
Soundness: if 𝜌 |= 𝜑 then LF(𝜑, 𝜌, x0 ) is satisfiable (valid);

Algorithm 2: LP(𝜌, x0 )input : 𝜌, a refined execution fragment (𝑧1 , 𝛿1 ), . . . , (𝑧𝑘 , 𝛿𝑘 );x0 , the initial value of clocks at the beginning of 𝜌.
output : Γ, the timing constraint derived from the execution
fragment.
1 begin2𝑧1′ = 𝑧1 [𝑥01 + 𝛿1 /𝑥1 , · · · , 𝑥0𝑚 + 𝛿1 /𝑥𝑚 ] ;3foreach 𝑖 ∈ {2, . . . , 𝑘} do4foreach 𝑗 ∈ {1, . . . , 𝑚} do
5
if 𝑥𝑗 ∈ 𝑎𝑖 .𝜆 then/* 𝑎𝑖 is the transition from𝑧𝑖−1 to 𝑧𝑖*/
6
𝑒𝑗 := 𝛿𝑖 ;/* 𝑥𝑗 should be reset
*/
7
8

9
10
11

Completeness: if LF(𝜑, 𝜌, x0 ) is satisfiable (valid), then 𝜌 |=𝜑.

P ROOF. Regarding termination, it can be simply done byinduction on the structure of 𝜑. Regarding soundness andcompleteness, we still proceed by induction on the structureof 𝜑 as follows:∙ The basic case, i.e., 𝜑 is a formulaof∫︀ the form 𝑏 ≤∑︀ℓ ≤ 𝑒 ⇒ 𝒟, where 𝐷 =𝑐𝑖 ∫︀𝑆𝑖 ≤ 𝑐. Then𝑖∈Ω∑︀ℐ𝜌 , [𝜌.𝑏, 𝜌.𝑒] |= 𝑏 ≤ ℓ ≤ 𝑒 ⇒ 𝑖∈Ω∫︀ 𝑐𝑖 𝑆𝑖 ≤ 𝑐 iff 𝑏 ≤∑︀𝜌.𝑒 − 𝜌.𝑏 ≤ 𝑒 ⇒𝑐ℐ(𝑆𝑖 )([𝜌.𝑏, 𝜌.𝑒]) ≤ 𝑐,𝑖𝜌𝑖∈Ωwhere 𝜌.𝑏 and 𝜌.𝑒 stands for the starting and ending
points of 𝜌. Obviously,

else
𝑒𝑗 := 𝑧𝑖−1 .𝑥𝑗 + 𝛿𝑖 ;/* 𝑧𝑖−1 .𝑥𝑗 stands for the valueof clock 𝑥𝑗 at the previouszone*/∀𝛿1 , · · · , 𝛿𝑛 , 𝒬.
(︂
)︂
LP(𝜌,
∫︀
∫︀
∑︀𝑛x0 )∑︀𝑛(1)
⇒ 𝒟[ 𝑖=1 𝑒𝑖1 / 𝑆1 , · · · , 𝑖=1 𝑒𝑖𝑑 / 𝑆𝑑 ]𝑧𝑖′ = 𝑧𝑖 [𝑒1 /𝑥1 , · · · , 𝑒𝑚 /𝑥𝑚 ];∑︀Γ = ∧𝑘𝑖=1 (𝑧𝑖′ ∧ 𝛿𝑖 ≥ 0) ∧ 𝑏 ≤ 𝑘𝑖=1 𝛿𝑖 ≤ 𝑒;return Γ ;is unsatisfiable implies 𝜌 ̸|= 𝜑 (soundness), and that(1) holds implies 𝜌 |= 𝜑 (completeness) according to
Algorithm 2 and Algorithm 3.
∙ 𝜑 = ¬𝜑1
For soundness, suppose LF(𝜌, ¬𝜑1 ) is unsatisfiable,i.e.,¬LF(𝜑1 , 𝜌, x0 ) is unsatisfiable by Algorithm 3, which
implies LF(𝜑1 , 𝜌, x0 ) is valid. By the induction hypothesis, we have 𝜌 |= 𝜑1 . Therefore, 𝜌 ̸|= ¬𝜑1 .
For completeness, suppose LF(¬𝜑1 , 𝜌, x0 ) is valid, which
derives LF(𝜑1 , 𝜌, x0 ) is unsatisfiable by Algorithm 3.
By the induction hypothesis, we have 𝜌 ̸|= 𝜑1 . Hence,𝜌 |= ¬𝜑1 .
∙ 𝜑 = 𝜑1 ∨ 𝜑2
For soundness, suppose LF(𝜑1 ∨ 𝜑2 , 𝜌, x0 ) is unsatisfiable, i.e., LF(𝜑1 , 𝜌, x0 ) ∨ LF(𝜑2 , 𝜌, x0 ) is unsatisfiable by Algorithm 3, which implies LF(𝜑1 , 𝜌, x0 ) andLF(𝜑2 , 𝜌, x0 ) both are unsatisfiable. By the induction
hypothesis, it follows that 𝜌 ̸|= 𝜑1 and 𝜌 ̸|= 𝜑2 . Therefore, 𝜌 ̸|= 𝜑1 ∨ 𝜑2 .
For completeness, suppose LF(𝜑1 ∨ 𝜑2 , 𝜌, x0 ) is valid,
which implies ¬LF(𝜑1 , 𝜌, x0 ) is unsatisfiable or ¬LF(
𝜑2 , 𝜌, x0 ) is unsatisfiable by Algorithm 3. By the induction hypothesis, we have either 𝜌 ̸|= ¬𝜑1 or 𝜌 ̸|= 𝜑2 ,hence 𝜌 |= 𝜑1 ∨ 𝜑2 .
∙ 𝜑 = 𝜑1 ; 𝜑2
It is clear that 𝜌 |= 𝜑1 ; 𝜑2 iff that 𝜌 can be split into
two parts 𝜌1 and 𝜌2 such that 𝜌 = 𝜌1 ∘ 𝜌2 , and 𝜌1 |=𝜑1 and 𝜌2 |= 𝜑2 , iff there exists 0 ≤ 𝑖 ≤ 𝑛 suchthat zone 𝑧𝑖 can be split two parts, i.e., (𝑧𝑖 , 𝛿𝑖1 ) and(𝑧𝑖 , 𝛿𝑖2 ) with 𝜌1 = (𝑧1 , 𝛿1 ), · · · , (𝑧𝑖 , 𝛿𝑖1 ) |= 𝜑1 and𝜌2 = (𝑧𝑖 , 𝛿𝑖2 ), · · · , (𝑧𝑛 , 𝛿𝑛 ) |= 𝜑1 with 𝛿𝑖 = 𝛿𝑖1 + 𝛿𝑖2 ,where 𝛿𝑖1 and 𝛿𝑖2 are fresh variables, which is exactly

𝑖 = 1, . . . , 𝑑 and 𝑗 = 1, . . . , 𝑛. Clearly, if 𝑧𝑗 satisfies
𝑆𝑖 , then 𝑒𝑖𝑗 is 𝛿𝑗 , otherwise 0.
the total duration∑︀Thus,𝑛of 𝑆𝑖 holding on 𝜌 should be 𝑗=1 𝑒𝑖𝑗 . Hence, we just∑︀𝑛need to replace each 𝑆𝑖 with 𝑗=1 𝑒𝑖𝑗 in 𝒟. Therefore,
the translated QLRA formula isLP(𝜌, 0) ⇒ (𝒟[

𝑛
∑︁
𝑖=1

𝑛
∑︁
∫︀
∫︀
𝑒𝑖1 / 𝑆1 , · · · ,𝑒𝑖𝑑 / 𝑆𝑑 ]),𝑖=1

where LP(𝜌, 0) stands for the QLRA formula translated from 𝜌 by applying Algorithm 2 with initial clock
values 0, and 𝜑[𝑒1 /𝑒2 ] stands for replacing each occurrence of 𝑒2 by 𝑒1 in 𝜑.
∙ When 𝜑 = ¬𝜑1 , 𝜑1 ∧ 𝜑2 , 𝜑1 ∨ 𝜑2 , it is easy to obtainby revoking the procedure recursively.
∙ If 𝜑 = 𝜑1 ; 𝜑2 , then we consider the 𝑛 + 2 cases where
the chop point is taken respectively before 𝑧1 , at 𝑧1 ,. . ., at 𝑧𝑛 , after 𝑧𝑛 . Subsequently, we recursively recall
the translation procedure to the resulted corresponding
sub-problems.
∙ Finally, quantify the resulted formula with the respective quantifications to the corresponding introduced
fresh variables (line 20).
The above procedure is implemented by Algorithm 3, and thereturned formula is a closed QLRA formula.
T HEOREM 4.1 (C ORRECTNESS OF A LGORITHM 3). Algorithm 3 is correct, i.e.,65equivalent to∀𝛿1 , · · · , ∀𝛿𝑛 , 𝒬.
⎛⎞
LF(𝜑1 , ⟨(𝑧1 , 𝛿1 ), · · · , (𝑧𝑖 , 𝛿𝑖1 )⟩, x0 )⎜ ∧ LF(⟨(𝜑2 , 𝑧𝑖 , 𝛿𝑖2 ), · · · , (𝑧𝑛 , 𝛿𝑛 )⟩,
⎟
⎜
⎟
∑︀𝑖−1
⎝
⎠
x0 +
𝛿𝑗 + 𝛿𝑖1 )In this section, we further discuss how to solve the resulted
QLRA formulas and the complexity of our approach.

5.1

𝑗=1

∧ 𝛿𝑖 = 𝛿𝑖1 + 𝛿𝑖2
by Algorithm 3 and the induction hypothesis.



T HEOREM 5.1. Given a TA 𝒜 and a bounded ELDI formula Φ, 𝒜 |= Φ iff ∧𝜌∈PEF(ZoneG(𝒜),𝑏,𝑒) LF(Φ, 𝜌, 0) is valid.

input : 𝜌 = (𝑧1 , 𝛿1 ), (𝑧2 , 𝛿2 ), . . . , (𝑧𝑛 , 𝛿𝑛 ), the underlined
execution fragment;
x0 , the initial value of clocks at the beginning of 𝜌;𝜑, the considered ELDI formula.
output : Γ, the derived QLRA formula.
1 begin2
𝒬 := 𝜀 ;/* 𝒬 records existential
quantifications over introduced
fresh variables*/
3
case 𝜑 := 𝑏 ≤ ℓ ≤ 𝑒 ⇒ 𝒟
4foreach 𝑖 ∈ {1, . . . , 𝑛} do5foreach 𝑗 ∈ {1, . . . , 𝑑} do
6
if 𝑧𝑖 |= 𝑆𝑗 then7
𝑒𝑖𝑗 := 𝛿𝑖 ;8else
9𝑒𝑖𝑗 := 0

11
12
13
14
15
16
17
18

20

C OROLLARY 5.2. Given a timed automaton 𝒜 and an
ELDI formula Φ, 𝒜, [𝑏, 𝑒] |= Φ is decidable.
Tarski’s original QE algorithm for real arithmetic is nonelementary [29]. But in the 1970s, Collins invented a newalgorithm for QE based on cylindrical algebraic decomposition (CAD) [5], which is double exponential in the numberof variables. CAD has been implemented in many computer
algebra tools such as REDLOG [8] and QEPCAD [4]. Particularly, all formulas of QLRA are linear, therefore the QE of
QLRA can be achieved more efficiently by virtual substitution due to Weinspfenning [9], which has been implemented
in REDLOG, recently in Z3, although the worst case is still
double exponential.

case 𝜑 := 𝜑1 ∧ 𝜑2
Γ := LF(𝜑1 , 𝜌, x0 ) ∧ LF(𝜑2 , 𝜌, x0 ) ;5.2

Complexity

As discussed above, model checking ELDI against boundedbehaviours of timed automata consists of three procedures:∙ The first one is PEF to find out all execution fragments
whose length is within the bounded interval [𝑏, 𝑒] for agiven TA 𝒜. The number of such execution fragments is𝑒
at most 𝑁 1+𝑁 *(1+⌈ 𝜖 ⌉) as we discussed before, where
𝑁 is the number of the zones generated from 𝒜 and 𝜖is the least dwelling time in every control cycle of 𝒜.
𝑒This step can be done in 𝑂(𝑁 𝑁 *(1+⌈ 𝜖 ⌉) ).
∙ The second one is LF, which translates whether a given execution fragment 𝜌 satisfies a considered ELDI formula Φ into a QLRA formula. The Algorithm
LF itself can be done in the linear of the size of Φ,
but the size of the generated QLRA formula could be𝑂((𝑁 (1 + ⌈ 𝑒𝜖 ⌉))𝑑 * |Φ|) in the worst case, where 𝑑 isthe number of nested chops. In addition, we need tocase 𝜑 := 𝜑1 ∨ 𝜑2
Γ := LF(𝜑1 , 𝜌, x0 ) ∨ LF(𝜑2 , 𝜌, x0 ) ;⎞LF(𝜑1 , ((𝑧1 , 𝛿1 ), · · · , (𝑧𝑖 , 𝛿𝑖1 )), x0 )⎟LF(𝜑2 , ((𝑧𝑖 , 𝛿𝑖2 ), · · · , (𝑧𝑛 , 𝛿𝑛 )),
⎟
∑︀𝑖−1
⎠
x0 + 𝑗=1 𝛿𝑗 + 𝛿𝑖1 )
𝛿𝑖 = 𝛿𝑖1 + 𝛿𝑖2∧;
𝒬 := 𝒬, ∃𝛿11 , ∃𝛿12 , · · · , ∃𝛿𝑛1 , ∃𝛿𝑛2 ;/* 𝛿11 , 𝛿12 , . . . , 𝛿𝑛1 , 𝛿𝑛2 are fresh
variables

According to Tarski’s result, the satisfiability and validity of
QLRA both are decidable [29], as QLRA admits the propertyof quantifier elimination (QE). So, an immediate result ofTheorem 5.1 is thatcase 𝜑 := ¬𝜑1
Γ := ¬LF(𝜑1 , 𝜌, x0 );⋁︀𝑛+1 ⎜
⎜ ∧
𝑖=0 ⎝

19

P ROOF. Directly by Theorem 3.1 and Theorem 4.1.

Γ := LP(𝜌, x0 ) ⇒
∫︀
∫︀
∑︀
∑︀𝑛
(𝒟[ 𝑛
𝑖=1 𝑒𝑖1 / 𝑆1 , · · · ,𝑖=1 𝑒𝑖𝑑 / 𝑆𝑑 ]) ;case 𝜑 := 𝜑1 ; 𝜑2Γ :=⎛Solving derived QLRA formulas

By Theorem 3.1 and Theorem 4.1, given a TA 𝒜, and a bounded ELDI formula Φ with lower bound 𝑏 and upper bound 𝑒,
model-checking whether Φ is satisfied by 𝒜 is reduced towhether a QLRA formula is valid, i.e.,

Algorithm 3: LF(𝜑, 𝜌, x0 )10

SOLVING DERIVED QLRA FORMULAS
AND COMPLEXITY ANALYSIS*/

return ∀𝛿1 , · · · , ∀𝛿𝑛 , 𝒬.Γ ;7

introduce 𝑑 * 𝑀 fresh variables and their corresponding
quantifications, where 𝑀 is the number of zones in abounded observation interval, 𝑁 * (1 + ⌈ 𝑒𝜖 ⌉) at most.
∙ The last one is a QE tool. Here we adopt REDLOG,
whose complexity is double exponential in the num𝑑𝑁 *(1+⌈ 𝑒 ⌉)𝜖ber of variables, i.e., 𝑂(22) to check whether
each of such execution fragments satisfies the considered ELDI formula Φ.
∙ So, the total complexity to check whether 𝒜 |= Φ is𝑑𝑁 *(1+⌈ 𝑒 ⌉)𝑒𝜖). Moreover, it is well𝑂(𝑁 𝑁 *(1+⌈ 𝜖 ⌉) * 22
known that 𝑁 , the number of zones of ZoneG(𝒜), is
exponential in 𝑛, the number of the locations of 𝒜 [2],in the worst case. So, the complexity of our approachis 3-fold exponential in the size of 𝒜 and 2-fold exponential in the number of nested chops in Φ.

The following case studies are used to illustrate the efficiency of our approach in practice, although it has a quite
high theoretical complexity. The experiments are conducted
on a laptop with Inter Core i3-5005U at 2.0GHz and 4GB
DDR3L-1600MHz RAM.
Example 6.1. In this example, we consider the anomalous
behaviour of priority-driven systems given in [22].
The simple system contains four independent jobs, which
are scheduled on two identical processors 𝑃1 and 𝑃2 in apriority-driven manner. 𝑃1 and 𝑃2 maintain a common priority order of jobs 𝐽1 >𝐽2 >𝐽3 >𝐽4 . These jobs may be preempted, but never be migrated, which means that once it begins
to be executed on a processor, the job has to be executed onthat processor until completion. The release times (𝑟), deadlines (𝑑), and execution times of the jobs are listed in Fig. 2.
𝐽1 , 𝐽2 , 𝐽4 are released at 0, while 𝐽3 is released at 4. The
execution times of 𝐽1 , 𝐽3 , 𝐽4 are fixed, while 𝐽2 ’s is varied in[2, 6]. In addition, 𝐽1 is required to be executed on 𝑃1 , 𝐽2 isrequired to be executed on 𝑃2 , while 𝐽3 and 𝐽4 can be executed on either of 𝑃1 and 𝑃2 . The property which should besatisfied by 𝑃2 on [0, 20] can be represented by the following
ELDI formula:
∫︀
∫︀
∫︀

Although the theoretical complexity of our approach isquite high as analyzed above, in practice, the worst cases
happen with quite low possibility. We believe that REDLOG
can handle QLRA formulas in polynomial time in their sizes
in most cases. The below experiments will justify this.

6

20 ≤ ℓ ≤ 20 ⇒ [(2 ≤ run𝐽2 ≤ 6 ∧ run𝐽2 − 1 = 0)
∫︀
∫︀
∫︀
∫︀
; (( run𝐽3 = 0 ∨ run𝐽3 = 8) ∧ ( run𝐽4 = 0 ∨ run𝐽4 = 10)∧∫︀∫︀
(0 < run𝐽3 + run𝐽4 ≤ 18))].

IMPLEMENTATION AND
EXPERIMENTS

Based on the DBM library of UPPAAL, we developed a prototypical tool for our approach on Linux with two input files:
the first is a .xml file to represent the timed automaton under consideration in UPPAAL format, and the other contains
the ELDI formula to be verified. Our tool outputs a text file,which represents the generated QLRA formula as the inputof REDLOG (Reduce), the QE tool we used. REDLOG will
return true or false to the problem whether the ELDI formula
is satisfied by the timed automaton on all bounded execution
fragments. Besides, our tool also provides the function tocheck whether a given bounded execution fragment satisfies
the ELDI formula. Therefore, on the one hand, the size of the

The tool verifies the formula in 2.4 seconds, and returns
false. This implies that some jobs cannot catch the deadline
on [0, 20], a counterexample is provided in Fig. 3.
0

5

P1

J1

P2

J2

J4

J2

A
`

Reduce

Θ
true

J3 4

counterexample

J4 0

false
{ζ}

J1 0
J2 0

ζk

Figure 1: Overall structure.

10
10
15
20

J3

2

+

r d [e , e ]

QE

QLRA
φ

J4

(a)

P2

5
[2, 6]
8
10

16

J1

P1
P2

20

15

J3

6

J4
20

(b)

J1

P1

−

10

J2

J4
3

J3

J4

(c)

21

Figure 3: A counterexample
Example 6.2. Now consider an example of final testingof integrated circuits, which is a simplified version of a realworld problem reported in [25]. In this simplified version, alljobs are clustered into two product types 𝐴 and 𝐵. Both of
𝐴 and 𝐵 jobs are processed in two stages, i.e., testing
and burn in. 𝐴 and 𝐵 jobs are grouped into 5 and 2 lots
respectively. In testing stage, all 𝐴 and 𝐵 lots are processed serially on several parallel machines, and it takes 3
time units to handle each 𝐴 lot, and 4 time units to handle
each 𝐵 lot by one machine. In burn in stage, all 𝐴 and
𝐵 lots are processed in a batch manner on several parallelmachines, and it takes 10 time units to finish a batch by one

Figure 2: Job description.

generated QLRA formula could decrease dramatically, which
can scale up our approach very much; on the other hand, it cantell which execution fragment is a counterexample as well,when model-checking the problem is done by enumerating
all possible execution paths. The overall structure of our tool
is depicted as Fig. 1.
8

machine. The maximum batch size for a machine is 5. For
simplicity, here we assume there are two machines on eachstage. So, we introduce two integer variables m test ∈ [0, 2]
and m burn ∈ [0, 2] to stand for how many machines havebeen used at testing and burn in stages, respectively.
At testing, no machine can be allocated to 𝐵 product (dually 𝐴 product) unless all 𝐴 jobs (dually 𝐵 jobs) have been
finished in case it has been allocated to 𝐴 product (dually
𝐵 product). Additionally, any type product can switch fromtesting to burn in immediately whenever all its lots
have been processed at testing. Thus, 𝐴 and 𝐵 products
can be modelled by TA PA and PB in Fig. 4.(a) and Fig. 4.(b)correspondingly.

schedule to meet these requirements within 36 to 40 timeunits, i.e., whether the following formula holds.
36 ≤ ℓ ≤ 40 ⇒
∫︀
⎛ ∫︀
⎞
∫︀(PA.wait testing, *) + ∫︀(PA.testing, *)+⎠⎝ (PA.wait burn in, *) + (PA.burn in, *) ≤ 30∫︀∫︀∧[9 ≤ (PA.testing, *) ≤ 15; (PA.burn in, *) = 10]
∫︀
⎞
⎛ ∫︀
∫︀(*, PB.wait testing) + ∫︀(*, PB.testing)+⎠
burn in) + (*,∫︀PB.burn in) ≤ 36
∧ ⎝ (*, PB.wait∫︀∧[4 ≤ (*, PB.testing) ≤ 8; (*, PB.burn in) = 10]

where (PA.𝑙, *) stands for a state expression, which meansthat in PA×PB , PA stays in location 𝑙 at time 𝑡 if (PA.𝑙, *)(𝑡) =1, (*, PB.𝑙) can be understood symmetrically.
It takes 126 minutes totally to check the above property
with our tool, which finds several feasible schedules by solving the resulting QLRA formula. For example, in Fig. 5, thepath 00 → 10 → 11 → 14 → 54 → 55 → 65 → 67 → 87with chop points at 54 is a feasible schedule.

(a)

(b)

Figure 4: (a) PA: TA for product A; (b) PB: TA for product B.
Figure 5: PA × PB, the product of PA and PB

PA has nine locations 0, . . . , 8. 0 stands for waiting fortesting, 1 for one machine allocated to test 𝐴 product, 2, 3, 4
for both of the two machines allocated to test 𝐴 product, butwith different scheduling policies. In 2, one machine has 5
lots and the other has no jobs; in 3, one machine has 4 lots
and the other has 1 lot; in 4, one machine has 3 lots and theother has 2 lots. 5 for waiting for burning, 6, 7 for 𝐴 lots
under burn respectively with one machine and two machines,
8 for completion. The above procedure can be repeated. PB
can be understood similarly. Note that there are only twoscheduling policies in PB at testing when both of the twomachines are allocated to it. 𝑥 and 𝑦 are two clock variables.
The product automaton of PA and PB is shown in Fig. 5 .
The timing constraints on the products 𝐴 and 𝐵 are given
as follows: The deadlines for 𝐴 and 𝐵 are 30 and 36, respectively. Now, the question is wether we can find a feasible

Considering the size of the example, the execution timeis acceptable. The zone graph of the product automaton has
more than 660 zones which are the beginning zones of thesearch process. What’s more, the loops of the product automaton increase the number of the paths and the path length
dramatically. The size of the generated file storing QLRA
formulas is 3.1GB and it was divided into 187 files as inputs
for REDLOG due to the limit of the memory size.
Note that virtual substitution has been implemented in thelatest release of Z3. Z3 takes 0.24 seconds and 114 minutes
respectively to solve the resulting QLRA formulas in Example
6.1 and Example 6.2. This indicates that the efficiencies ofZ3 and REDLOG are nearly same on solving such formulas.
9

7

CONCLUSION[9] A. Dolzmann, T. Sturm, and V. Weispfenning. 1998. A new approach
for automatic theorem proving in real geometry. J. of AutomatedReasoning 21, 3 (1998), 357–380.
[10] M. Fränzle. 2004. Model-checking dense-time Duration Calculus.
Formal Aspects of Computing 16, 2 (2004), 121–139.
[11] M. Fränzle and M. R. Hansen. 2007. Deciding an interval logic withaccumulated durations. In TACAS 2007. 201–215.
[12] M. Fränzle and M. R. Hansen. 2008. Efficient model checking for
Duration Calculus based on branching-time approximations. In SEFM
2008. 63–72.
[13] M. Fränzle and M. R. Hansen. 2009. Efficient model checking forduration calculus. International Journal of Software and Informatics 3,
2-3 (2009), 171–196.
[14] V. Goranko, A. Montanari, and G. Sciavicco. 2004. A road map of interval temporal logics and duration calculi. J. of Applied Non-Classical
Logics 14, 1-2 (2004), 9–54.
[15] J. Y. Halpern, Z. Manna, and B. C. Moszkowski. 1983. A hardware
semantics based on temporal intervals. In ICALP 1983. 278–291.
[16] M. R. Hansen. 1994. Model-checking discrete Duration Calculus.
Formal Aspects of Computing 6, 1 (1994), 826–845.
[17] T. A. Henzinger. 1996. The theory of hybrid automata. In LICS 1996.
278–292.
[18] C. Zhou. C. A. R. Hoare and A. P. Ravn. 1991. A calculus of durations.
Inf. Proc. Let. 40, 5 (1991), 269–276.
[19] K. G. Larsen, P. Pettersson, and Y. Wang. 1997. Uppaal in a nutshell.
STTT 1, 1 (1997), 134–152.
[20] X. Li. and D. V. Huang. 1996. Checking linear duration invariants bylinear programming. In ASIAN 1996. 321–332.
[21] X. Li, D. V. Huang, and T. Zheng. 1997. Checking hybrid automata forlinear duration invariants. In ASIAN 1997. 166–180.
[22] J. Liu. 2000. Real-Time Systems. Prentice Hall.
[23] R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. 2008. Modelchecking Duration Calculus: a practical approach. Formal Aspects ofComputing 20, 4 (2008), 481–505.
[24] P. K. Pandya. 2001. Specifying and deciding quantified discrete-time
duration calculus formulae using DCVALID. In RT-TOOLS 2001.
[25] W. L. Pearn, S. H. Chung, A. Y. Chen, and M. H. Yang. 2004. A casestudy on the multistage IC final testing scheduling problem with reentry.
International J. of Production Economics 88, 3 (2004), 257 – 267.
[26] P. Pettersson. 1999. Modelling and Verification of Real-Time Systems
Using Timed Automata: Theory and Practice. PhD thesis. Uppsala
University.
[27] T. G. Rokicki. 1993. Representing and Modeling Digital Circuits. PhD
thesis. Stanford University.
[28] B. Sharma, P. K. Pandya, and S. Chakraborty. 2005. Bounded validity
checking of interval duration logic. In TACAS 2005. 301–316.
[29] A. Tarski. 1951. A Decision Method for Elementary Algebra andGeometry. University of California Press, Berkeley.
[30] P. Thai and D. Hung. 2004. Verifying linear duration constraints of
timed automata. In ICTAC 2004. 295–309.
[31] M. Zhang, D. Hung, and Z. Liu. 2008. Verification of LDIs by model
checking CTL properties. In ICTAC 2008. 395–409.
[32] M. Zhang, Z. Liu, and N. Zhan. 2009. Model checking linear duration
invariants of networks of automata. In FSEN 2009. 244–259.
[33] C. Zhou and M. R. Hansen. 2004. Duration Calculus: A Formal
Approach to Real-Time Systems. Springer.
[34] C. Zhou, M. R. Hansen, and P. Sestoft. 1993. Decidability and undecidability results for duration calculus. In STACS 1993. 58–68.
[35] C. Zhou, J. Zhang, L. Yang, and X. Li. 1994. Linear duration invariants.
In FTRTFT 1994. 86–109.
[36] Q. Zu, M. Zhang, J. Zhu, and N. Zhan. 2013. Bounded model-checkingof discrete duration calculus. In HSCC 2013. 213–222.

In this paper, we investigate the model-checking of timed automata against bounded ELDI in the context of the continuoustime semantics. This is achieved through the following steps:
firstly, we compute all execution fragments of a given timed
automaton 𝒜 whose length is within the given bounded interval according to 𝒜’s zone graph; secondly, we encode whether
each execution fragment obtained in the first step satisfies thegiven bounded ELDI formula Φ into a QLRA formula; finally,
we invoke REDLOG, a computer algebra tool, or Z3, an SMT
solver, to solve the resulting QLRA formula. The complexityof our approach is triple exponential in the number of 𝒜’s locations and double exponential in the number of nested chopsin Φ in the worst case. But in practice, it is very efficient as in
REDLOG and Z3, virtual substitution can be applied to QLRA formulas. We have implemented a prototypical tool, andsome case studies are provided to illustrate our approach2 .

8

ACKNOWLEDGMENTSFirst of all, we thank the anonymous referees for their constructive comments, which improve this paper so much.
The first and fourth authors are partly supported by NSFC61472279, the second author is partly supported by 973 Program under grant No. 2014CB340701, by NSFC-61625206
and NSFC-61732001, by CDZ project CAP (GZ 1023), andby the CAS/SAFEA International Partnership Program for
Creative Research Teams, the third author is partly support
by Macao FDCT 103/2015/A3, UM MYRG2017-00141-FST
and NSFC-61672435.

REFERENCES[1] R. Alur and D. L. Dill. 1994. A theory of timed automata. TCS 126(2)(1994), 183–235.
[2] J. Bengtsson and Y. Wang. 2004. Timed Automata: Semantics, Algorithms and Tools. In Lectures on Concurrency and Petri Nets: Advancesin Petri Nets. 87–124.
[3] V. A. Braberman and D. V. Huang. 1998. On checking timed automata
for linear duration invariants. In RTSS 1998. 264 – 273.
[4] C. W. Brown. 2003. QEPCAD B: A program for computing withsemi-algebraic sets using CADs. ACM SIGSAM Bulletin 37, 4 (2003),
97–108.
[5] G. Collins. 1975. Hauptvortrag: Quantifier elimination for real closed
fields by cylindrical algebraic decomposition. In 2nd GI Conference on
Automata Theory and Formal Languages. 134–183.
[6] W. Damm, M. Horbach, and V. Sofronie-Stokkermans. 2015. Decidability of Verification of Safety Properties of Spatial Families of Linear
Hybrid Automata. In FroCoS 2015. 186–202.
[7] W. Damm, C. Ihlemann, and V. Sofronie-Stokkermans. 2011. Decidability and complexity for the verification of safety properties of reasonablelinear hybrid automata. In HSCC 2011. 73–82.
[8] A. Dolzmann, A. Seidl, and T. Sturm. 2006. Redlog User Manual(Edition 3.1, for Redlog Version 3.06 (Reduce 3.8) ed.).

2 https://github.com/Leslieaj/VCELDI

10