JAIST Repository
https://dspace.jaist.ac.jp/

Title

Nested Timed Automata

Author(s)Li, Guoqiang; Cai, Xiaojuan; Ogawa, Mizuhito;
Yuen, Shoji

Citation

Research report (School of Information Science,
Japan Advanced Institute of Science andTechnology), IS‑RR‑2013‑004: 1‑20

Issue Date

2013‑06‑11

TypeTechnical Report

Text version

publisher

URL

http://hdl.handle.net/10119/11354

RightsDescription

リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）

Japan Advanced Institute of Science and Technology

Nested Timed Automata
Guoqiang Li,

Xiaojuan Cai

School of Software, Shanghai Jiotong University

Mizuhito Ogawa

Japan Advanced Institute of Science and Technology

Shoji Yuen

Graduate School of Information Science, Nagoya University

June, 11, 2013
IS-RR-2013-004

Nested Timed Automata
Guoqiang Li1 , Xiaojuan Cai1 , Mizuhito Ogawa2 , and Shoji Yuen3
1

School of Software, Shanghai Jiao Tong University, China{li.g, cxj}@sjtu.edu.cn
2Japan Advanced Institute of Science and Technology, Japanmizuhito@jaist.ac.jp
3
Graduate School of Information Science, Nagoya University, Japanyuen@is.nagoya-u.ac.jp

Abstract. This paper proposes a new timed model named nested timed
automata (NeTAs). An NeTA is a pushdown system whose stack symbols
are timed automata (TAs). It either behaves as the top TA in the stack,or switches from one TA to another by pushing, popping, or changing the top TA of the stack. Diﬀerent from existing component-based
context-switch models such as recursive timed automata and timed recursive state machines, when time passage happens, all clocks of TAs inthe stack elapse uniformly. We show that the safety property of NeTAs
is decidable by encoding NeTAs to the dense timed pushdown automata. NeTAs provide a natural way to analyze the recursive behaviors ofcomponent-based timed systems with structure retained. We illustrate
this advantage by the deadline analysis of nested interrupts.

1

Introduction

Due to the rapid development of large and complex timed systems, requirements to model and analyze complex real-time frameworks with recursive context switches have been stresses. Diﬃculty comes from two dimensions of inﬁnity,a stack with unbounded number of symbols, and clocks recording dense time.
The inﬁnity raises diﬃculty to guarantee decidability of properties, e.g., safety
properties.
Timed automata (TAs) [1] are a ﬁnite automaton with a ﬁnite set of clocks
that grow uniformly. A typical timed model with context switches is timed pushdown automata (TPDAs) [2], equipped with an unbounded stack, where clocks
are not updated in the stack. This limitation is found unnatural in analyzing
the timed behavior of programs since clock values should be updated in suspension. Recently, a new timed pushdown model, dense timed pushdown automata(DTPDAs) [3] has been proposed, where each symbol in the stack is equippedwith local clocks named “ages”, and all ages in the stack are updated uniformly
for time passage. Reachability problem of DTPDAs is in EXPTIME [3].
This paper proposes a new timed model named nested timed automata (NeTAs). An NeTA is a pushdown system whose stack symbols are TAs. It either
behaves as the top TA in the stack, or switches from one TA to another following

2

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

three kinds of transitions: pushing a new TA, popping the current TA when terminates, or replacing the top TA of the stack. This hierarchical design captures
the dynamic feature of functionally independent component-based structure of
timed systems. The existing models, such as recursive timed automata [4], andtimed recursive state machines [5] do not update clocks in the stack when time
passage happens, while in NeTAs, all clocks elapse uniformly. When a TA ispushed into the stack, a set of fresh local clocks is introduced to the system. In
this respect, NeTAs may have to handle an unbounded number of local clocks.
NeTAs are shown to be encoded to DTPDAs preserving the state reachability.
All transitions of NeTAs are simulated by DTPDAs, and vice versa. We illustratethat NeTAs are adopted to analyze the timely deadline of nested interrupts.
The rest of the paper is organized as follows. Section 2 gives an introductionof TAs and DTPDAs. Section 3 gives the formal deﬁnition and semantics of
NeTAs. Section 4 presents an encoding method from NeTAs to DTPDAs, andproves its correctness. Section 5 illustrates the usages of NeTAs by an application
example. Section 6 gives the related work and Section 7 concludes the paper.

2

Preliminaries

Let R≥0 and N denote the sets of non-negative real numbers and natural
numbers, respectively. We deﬁne Nω := N∪{ω}, where ω is the ﬁrst limit ordinal.
Let I denote the set of intervals. An interval is a set of numbers, written as (a, b),[a, b], [a, b) or (a, b], where a ∈ N and b ∈ Nω . For a number r ∈ R≥0 and aninterval I ∈ I, we use r ∈ I to denote that r belongs to I.
Let X = {x1 , . . . , xn } be a ﬁnite set of clocks. A clock valuation ν : X → R≥0 ,assigns a value to each clock x ∈ X. ν0 represents all clocks in X assigned tozero. Given a clock valuation ν and a time t ∈ R≥0 , (ν + t)(x) = ν(x) + t, forx ∈ X. A clock assignment function ν[y ← b] is deﬁned by ν[y ← b](x) = b if
x = y, and ν(x) otherwise.
2.1

Timed Automata

A timed automaton is an automaton augmented with a ﬁnite set of clocks [1,6]. Time can elapse in a location, while switches are instantaneous.
Since we focus on the safety properties (i.e., emptiness problem of a TA, or
reachability problem of a timed transition system), we omit input symbols for
all concerned automata, following the formalization in [3].
We adopt the TA deﬁnition style from that in [3], which looks diﬀerent fromthe one in [1, 6]. The main diﬀerence is that we do not adopt invariant, a time
constraint assigned to each control location. The reason lies that invariants cause
time lock problems. When context switches back, it may occur that the system
can neither stay in the current control location since the invariant is violated nor
transit to other control location since all constraints on transitions are violated.
Nondeterministic clock updates are also taken from [7] with interval tests as
diagonal free time constraints where decidability results are not aﬀected.

Nested Timed Automata

3

Definition 1 (Timed Automata). A timed automaton is a tuple A = (Q, q0 ,F, X, ∆) ∈ A , where– Q is a finite set of control locations, with the initial location q0 ∈ Q,
– F ⊆ Q is the set of final locations,– X is a finite set of clocks,– ∆ ⊆ Q × O × Q, where O is a set of operations. A transition δ ∈ ∆ is aϕtriplet (q1 , ϕ, q2 ), written as q1 −→ q2 , in which ϕ is either ofLocal ϵ, an empty operation,
Test x ∈ I? where x ∈ X is a clock and I ∈ I is an interval, andAssignment x ← I where x ∈ X and I ∈ I.
Given a TA A ∈ A , we use Q(A), q0 (A), F (A), X(A) and ∆(A) to represent
its set of control locations, initial location, set of ﬁnal locations, set of clocks andset of transitions, respectively. We will use similar notations for other models.
The semantics of timed automata includes progress transitions, for time elapsing within one control location, and discrete transitions, for transference
between two control locations.
Definition 2 (Semantics of TAs). Given a TA A = (Q, q0 , F, X, ∆), a configuration is a pair (q, ν) of a control location q ∈ Q, and a clock valuation ν on
X. The transition relation of the TA is represented as follows,t– Progress transition: (q, ν) −→A (q, ν + t), where t ∈ R≥0 .
ϕϕ– Discrete transition: (q1 , ν1 ) −→A (q2 , ν2 ), if q1 −→ q2 ∈ ∆, and one of thefollowing holds,• Local ϕ = ϵ, then ν1 = ν2 . The empty operation does not modify theclock valuations.
• Test ϕ = x ∈ I?, ν1 = ν2 and ν2 (x) ∈ I holds. The transition can be
performed only if the value of x belongs to I.
• Assignment ϕ = x ← I, ν2 = ν1 [x ← r] where r ∈ I. The clock x is
assigned an arbitrary value in I.
The initial configuration is (q0 , ν0 ). The transition relation is → and we define
t

ϕ

→=→
−A ∪−
→A , and define →∗ to be the reflexive and transitive closure of →.
Remark 1 (Sound Simulation). The TA deﬁnition in Deﬁnition 1 follows thestyle in [3]. In [1], a TA allows a logical connection of several constraint tests,
e.g. x ≤ 15 ∧ y > 20, and several resets operations of diﬀerent clocks during one
discrete transition. Only one test or assignment (a generalization of the reset) isallowed during one discrete transition in the deﬁnition. Since a discrete transition
is followed by a progress transition where time elapses, the main ambiguity of
two deﬁnitions is whether a conjunction of two tests can be checked one by one,
between which the time elapses. It is shown that TA with our deﬁnition soundly
simulates the timed traces in the original deﬁnition, as follows,x∈[a,+∞)?

tt[a,+∞)?

For ≥ or >, c −−−−−−−→A c′ →− A c′ is safely converted to c −→A c −−−−−→A
c , for some conﬁgurations c and c′ .
′4Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuentx∈[0,a]?

x∈[0,a]?

t

For ≤ or <, c −→A c −−−−−→A p′ is safely converted to c −−−−−→A c′ →− A c′ ,′for some conﬁgurations c and c .
For test transitions, a general simulation strategy is, ﬁrstly, checking the ≥,and > one by one, then check ≤ and < later. If there exists a “=” constraint,x≤15∧y>20
decomposed it into ≥ ∧ ≤. For example, a transition p −−−−−−−−→ q in they∈(20,+∞)?

x∈[0,15]?

original deﬁnition is simulated by two transitions p −−−−−−−−→ p′ −−−−−−→ q
under the new deﬁnition, where p′ is a fresh control location.
For reset transitions, a group of clocks are reset simultaneously can be simulated by resetting clocks one by one, with a zero test of the ﬁrst reset clock on{x,y}the tail. For example, a transition p −−−→ q, resetting x and y simultaneously, inx←[0,0]y←[0,0]x∈[0,0]?

the original deﬁnition is simulated by p −−−−−→ p′ −−−−−→ p′′ −−−−−→ q, wherep′ , p′′ are fresh control locations.
If a transition contains both test and reset operations, we ﬁrstly simulate
test operation, then reset operation, following the above rules.
2.2

Dense Timed Pushdown Automata

Dense Timed Pushdown Automata (DTPDAs) [3] extend TPDAs with time
update in the stack. Each symbol in the stack is equipped with a local clock
named age, and all ages in the stack elapse uniformly. An age in each context
is assigned to a value in a given interval or the value of a clock when a pushtransition occurs. A pop transition pops the top symbol provided the value of
its age belongs to a given interval, or just assigns the value of its age to a clock.
Definition 3 (Dense Timed Pushdown Automata). A dense timed pushdown automaton is a tuple D = ⟨S, s0 , Γ, C, ∆⟩ ∈ D, where– S is a finite set of states with the initial state s0 ∈ S,
– Γ is a finite stack alphabet,– C is a finite set of clocks, and– ∆ ⊆ S × O × S is a finite set of transitions.
ϕ

A transition δ ∈ ∆ is a triplet (s1 , ϕ, s2 ), written as s1 −→ s2 , in which ϕ iseither of– Local ϵ, an empty operation,– Test x ∈ I?, where x ∈ X is a clock and I ∈ I is an interval,– Assignment x ← I where x ∈ C and I ∈ I,
– Push push(γ, I), where γ ∈ Γ is a stack symbol and I ∈ I. It pushes γ tothe top of the stack, with the age in the interval I.
– Pop pop(γ, I), where γ ∈ Γ and I ∈ I. It pops the top-most stack symbol
provided that this symbol is γ, and its age belongs to I.
– PushA push(γ, x), where γ ∈ Γ is a stack symbol and x ∈ C, and– PopA pop(γ, x), where γ ∈ Γ is a stack symbol and x ∈ C.

Nested Timed Automata

5

Definition 4 (Semantics of DTPDAs). For a DTPDA ⟨S, s0 , Γ, C, ∆⟩, aconfiguration is a triplet (s, w, ν) with s ∈ S, w ∈ (Γ × R≥0 )∗ , and a clock
valuation ν on X. Time passage of the stack w + t = (γ1 , t1 + t). · · · .(γn , tn + t)
for w = (γ1 , t1 ). · · · .(γn , tn ).
The transition relation of the DTPDA is defined as follows:t– Progress transition: (s, w, ν) −→D (s, w + t, ν + t), where t ∈ R≥0 .
ϕϕ– Discrete transition: (s1 , w1 , ν1 ) −→D (s2 , w2 , ν2 ), if s1 −→ s2 , and one of thefollowing holds,• Local ϕ = ϵ, then w1 = w2 , and ν1 = ν2 . The empty operation does not
modify stack contents and clock values.
• Test ϕ = x ∈ I?, then w1 = w2 , ν1 = ν2 and ν2 (x) ∈ I holds. The
transition can be performed only if the value of x belongs to I.
• Assignment ϕ = x ← I, then w1 = w2 , ν2 = ν1 [x ← r] where r ∈ I.
The clock x is assigned an arbitrary value in I.
• Push ϕ = push(γ, I), then ν1 = ν2 , and w2 = (γ, r).w1 for some r ∈ I.
γ is pushed into the top of the stack with its age to be some arbitraryvalue r in I. The clock values are not changed.
• Pop ϕ = pop(γ, I), then ν1 = ν2 , and w1 = (γ, r).w2 for some r ∈ I.
Whether the top-most symbol in the stack is γ, and whether its age value
is in I is checked. The clock values are not changed.
• PushA ϕ = push(γ, x), then ν1 = ν2 , and w2 = (γ, ν1 (x))w1 . It pushes
γ to the stack associated with a local age with the value of the x’s value.
• PopA ϕ = pop(γ, x), then ν2 = ν1 [x ← t], and w1 = (γ, t)w2 . It pops γ
from a stack and assigns value of its local age to the global clock x.
The initial configuration κ0 = (q0 , ϵ, ν0 ). We use ,−→ to range over these transitions, and ,−→∗ is the transitive closure of ,−→, conventionally.
Example 1. Fig. 1 shows transitions between conﬁgurations of a DTPDA consisting of a singleton state set S = {•} (omitted in the ﬁgure), clocks C ={x1 , x2 , x3 }, and stack symbols Γ = {a, b, d}. From κ1 to κ2 , a discrete transition push(d, x3 ) pushes (d, 2.3) into the stack. A time transition from κ2 to κ3
elapses 2.6 time units, and each value grows older for 2.6. From κ3 to κ4 , thevalue of x2 is reset to 3.8, which lies in the interval (2, 5], and the last transition
pops (d, x1 ) and resets x1 to 4.9.
Remark 2. Deﬁnition 3 extends the deﬁnition in [3] by adding PushA and PopA ,which stores and recovers from clocks to ages and vice versa. This extension does
not destroy decidability of state reachability of DTPDAs [8], since its symbolic
encoding is easily modiﬁed to accept PushA and PopA . For instance, PushA is
encoded similar to Push, except for the deﬁnition on Reset [3]. Reset(R)[a ← I]
symbolically explores all possibility of the fraction of an instance in I. Instead,
Reset(R)[a ← x] will assign the same integer and fraction parts to x, whichmeans an age is simply placed at the same position to x in the region.

6

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen(a, 1.9)(b, 6.7)(a, 3.1)(d, 4.2)(d, 2.3)(a, 1.9)(b, 6.7)(a, 3.1)(d, 4.2)(d, 4.9)(a, 4.5)(b, 9.3)(a, 5.7)(d, 6.8)(d, 4.9)(a, 4.5)(b, 9.3)(a, 5.7)(d, 6.8)(a, 4.5)(b, 9.3)(a, 5.7)(d, 6.8)x1 ← 0.5x2 ← 3.9
x3 ← 2.3

x1 ← 0.5x2 ← 3.9
x3 ← 2.3

x1 ← 3.1x2 ← 6.5
x3 ← 4.9

x1 ← 3.1x2 ← 3.8
x3 ← 4.9

x1 ← 4.9
x2 ← 3.8
x3 ← 4.9

push(d,x3 )2.6

x2 ←(2,5]pop(d,x1 )κ1 −−−−−−−−−→D κ2 −−−−−−−−→D κ3 −−−−−−−−−→D κ4 −−−−−−−−→D κ5
Fig. 1. An Example of DTPDA

3

Nested Timed Automata

Nested Timed Automata (NeTAs) aim to give an operation strategy to agroup of TAs, in which a TA is able to preempt the other ones. All clocks in an
NeTA are local clocks, with the scope of their respective TAs. These clocks in thestack elapse simultaneously. An unbounded number of clocks may be involved in
one NeTA, due to recursive preemption loops, diﬀer from existing timed models,such as TA, TPDA, TRSMs and RTA.
Definition 5 (Nested Timed automata). A nested timed automaton is a
triplet N = (T, A0 , ∆) ∈ N , where– T is a finite set of timed automata, with the initial timed automaton A0 ∈ T .
– ∆ ⊆ T ×P ×(T ∪{ε}), where P = {push, pop, internal}. A rule (Ai , Φ, Aj ) ∈Φ∆ is written as Ai −→ Aj , where
push

Push Ai −−−→ Aj ,pop
Pop Ai −−→ ε, andinternal
Internal Ai −−−−−→ Aj .
The initial state of NeTAs is the initial location in A0 , s.t. q0 (A0 ). We also
assume that X(Ai ) ∩ X(Aj ) = ∅, and Q(Ai ) ∩ Q(Aj ) = ∅ for Ai , Aj ∈ T andi ̸= j.
The operational semantics of NeTAs is informally summarized as follows. It
starts with a stack with the only symbol of the initial TA. The system has thefollowing four behaviors: when there exists time passage, all clocks in the stack
elapse simultaneously; it is able to behave like the top TA in the stack; when
there exists a push transition from the top TA of the stack to the other TA, a
new instance of the latter TA is pushed into the stack at any time and executed,
while the suspended location of the former TA is recorded in the stack; when
the top TA in the stack reaches the ﬁnal location and a pop transition happens,
it will be popped from the stack, and the system will run the next TA beginningNested Timed Automata

7

with the suspended location; if an internal transition from the top TA to theother TA occurs, the top TA in the stack will be changed to a new instance ofthe latter TA when it reaches some ﬁnal location.
Definition 6 (Semantics of NeTAs). Given an NeTA (T, A0 , ∆), a configuration is a stack, and the stack alphabet is a tuple ⟨A, q, ν⟩, where A ∈ T isa timed automaton, q is the current running control location where q ∈ Q(A), andν is the clock valuation of X(A). For a stack content c = ⟨A1 , q1 , ν1 ⟩⟨A2 , q2 , ν2 ⟩ . . .
⟨An , qn , νn ⟩, let c + t be ⟨A1 , q1 , ν1 + t⟩⟨A2 , q2 , ν2 + t⟩ . . . ⟨An , qn , νn + t⟩.
The transition of NeTAs is represented as follows:t– Progress transitions: c →− N c + t.
ϕ
– Discrete transitions: c −→N c′ is defined as a union of the following fourkinds of transition relations,ϕϕ• Intra-action ⟨A, q, ν⟩c −→N ⟨A, q ′ , ν ′ ⟩c, if q −→ q ′ ∈ ∆(A), and one of
the following holds,∗ Local ϕ = ϵ, then ν = ν ′ .
∗ Test ϕ = x ∈ I?, ν = ν ′ and ν ′ (x) ∈ I holds.
∗ Assignment ϕ = x ← I, ν ′ = ν[x ← r] where r ∈ I.
push
push
• Push ⟨A, q, ν⟩c −−−→N ⟨A′ , q0 (A′ ), ν0′ ⟩⟨A, q, ν⟩c, if A −−−→ A′ , andq ∈ Q(A).
poppop• Pop ⟨A, q, ν⟩c −−→N c, if A −−→ ε, and q ∈ F (A).
internal
internal• Inter-action ⟨A, q, ν⟩c −−−−−→N ⟨A′ , q0 (A′ ), ν0′ ⟩c, if A −−−−−→ A′ ,and q ∈ F (A).
The initial configuration c0 = ⟨A0 , q0 (A0 ), ν0 ⟩. We use −→ to range over thesetransitions and −→∗ is the transitive closure of −→, conventionally.
In followings, we focus on the state reachability that is regarded as the mostimportant property in modelling software behavior.
Definition 7 (Safety Property). A safety property of NeTAs is defined as
the state reachability problem: Given an NeTA N = (T, A0 , ∆), and a control
location pf ∈ Q(A) for some A ∈ T , decide whether there exists a configuration
c of N and a clock valuation ν, such that c0 −→∗ ⟨A, pf , ν⟩c.
Example 2. We take a simple example to show the usage of NeTAs. Assume thattwo processes access a shared buﬀer. One is to read from the buﬀer periodicallyeach 4 time units. It accomplishes after it reads one or more data. The other is towrite to the buﬀer periodically. The execution time is between 3 and 5 time units.
It will return after writes one or more data. The writing process may overtake thereading process which initially starts running. The NeTA is shown in Fig. 2, withthree TAs. A0 is an empty TA for the idle state. A1 and A2 are for reading andinternal
writing processes, respectively. We have three transition rules: A0 −−−−−→ A1 ,pushpop
A1 −−−→ A2 , and A2 −−→ ε. The pop transition is not explicitly represented in
the ﬁgure. We use dash-line frames to represent the border of TAs in the NeTA,
double-line arrows to indicate the initial location/TA, and double-line circles torepresent the ﬁnal locations of TAs.

8

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
A1

q01

idle

A2

y ← [0, 2]

x ← [0, 0]

push

internalq11

idley ∈ (0, 5]?

y ← [0, 2]

x ∈ (0, 4]?

x ← [0, 0]

A0

qr1

wt

Fig. 2. An Example of NeTA

Remark 3 (Composition with timed automata). An NeTA is composed with a TA
by synchronization with shared actions in Σ, where we are allowed to add input
symbols as actions on transitions of NeTA. A composed TA presents behavioral
properties independent of recursive context switches such as the environment.
Although this extension does not increase the expressiveness of NeTAs, it is very
useful to model and analyze the behavioral properties in the component-basedmanner [9, 10]. A formal deﬁnition of the parallel composition, between an NeTA
N and a TA A, written as N ∥A, is formally deﬁned in Appendix A.

4

Decidability of Safety Property

In this section we prove the safety property problem of NeTAs is decidable
by encoding it into DTPDAs, of which state reachability is decidable.
4.1

Encoding NeTA to DTPDA

The idea to encode an NeTA to a DTPDA is straightforward, dealing withmultiple clocks at push and pop operations. We adopt extra fresh locations andtransitions to check whether a group of push/pop actions happens instantly.
Given an NeTA N = (T, A0 , ∆), we deﬁne E(N ) = ⟨S, s0 , Γ, C, ∇⟩ as thetarget of DTPDA encoding of N . Each element is described as,∪
The set of states S = SN ∪ Sinter , where SN = Ai ∈T Q(Ai ) is the set of
all locations of TAs in T (N ). Sinter is the set of intermediate states during thesimulation of push, pop, and internal rules of NeTAs. We assume that SN and
Sinter are disjoint.
Let n = |T | and mi = |X(Ai )| for each Ai ∈ T . Sinter is
Sinter = (

∪
Ai ∈T

i
Sreset)∪(∪push

Ai −→ Aj ∈∆

i,j
Spush
) ∪ {o}Nested Timed Automata

9

∪
i
i
– For every Ai ∈ T , we deﬁne Sreset= ( k∈{1···mi +1} rki ) ∪ ti . rki ∈ Sresetisthe start state of a transition to initialize the k-th clock of Ai to 0. ti is thestart state of a testing transition to make sure that no time is elapsed during
the sequence of initializing transitions.
∪
push
i,j
i,j
= k∈{1···mi +1} pi,j
– For every push rule Ai −→ Aj , we deﬁne Spushk . pkis the start state of a push transition that push the pair of the k-th clockof Ai and its value. After all clock values are stored in the stack, the lastdestination is the initial state q0 (Aj ) of Aj .
– o is a special state for repeat popping.
The initial state s0 = q0 (A0 ) is∪the initial location of the initial TA of N .
The set of clocks C = {d} ∪A∈T X(A) consists of all clocks of TA in
T (N ) and the special dummy clock d only to fulﬁll the ﬁeld of push and pop
rules, like push(q, d) and pop(q, d). (The value of d does not matter.)
The stack alphabet Γ = C ∪ SN .
∪The set of transitions ∇ is the union of Ai ∈T ∆(Ai ) (as Local transitionsof E(N )) and the set of transitions described in Fig. 3. For indexes, we assume
0 ≤ i, j ≤ n − 1 and 1 ≤ k ≤ mi (where i is speciﬁed in a context).

ϵ

ϵ

ϵ

ϵ

i
→ r1j , rm−
→ ti , qi −→ r1j , qi −→opi,jmi +1 −
i +1

Local

for qi ∈ F (Ai ).

xi1 ∈[0,0]?

t −−−−−−→ q0 (Ai ).
i

Test

xi ←[0,0]i
Assignment rki −−k−−−−→ rk+1.
push(xi ,xi )push(qi ,d)

Push

k k
i,j
qi −−−−−−−→ pi,j−−−−−−−→ pi,j
1 , pk −k+1 if k ≤ mi ,Popo −−−−−→ o, o −−−−−→ qpop(x,x)pop(q,d)for qi ∈ Q(Ai ).

forall x ∈ X(Ai ). q ∈ Q(Ai ).

Fig. 3. Transition Rules ∇ of E(C )Definition 8. For an NeTA N = (T, A0 , ∆), its encoding into a DTPDA E(N )is as follows.
push

Ai −→ Ajpush(xim ,xim )push(xi ,xi )push(qi ,d)

ϵ

1 1
i
i
−−−−−
−−→ · · · pi,j−−−−−−−−−→ pi,j→qi −−−−−−→ pi,jmi −1 −mi +1 −

xj ←[0,0]ϵ

xj ∈[0,0]?

j
1→− tj −−1−−−−→ q0 (Aj )r1j −−−−−→ r2j · · · rm
j +1
pop

Ai −→ ϵAiinternalϵpop(xim +1 ,xim +1 )ϵxj ←[0,0]pop(xi ,xi )pop(q,d)

i
i
1 1
qi −
→ o −−−−−−−−−−−−→ · · · −−−−−−−→ o −−−−−→ qϵxj ∈[0,0]?

j
1−→ Aj qi −→ r1j −−−−−→ r2j · · · rm→
− tj −−1−−−−→ q0 (Aj )
j +1
push

For a push transition Ai −→ Aj , E(N ) simulates, by storing current stateof Ai into the stack, pushing each clock with its current value as an age, andswitching to the initial conﬁguration of Aj (which consists of initializing each

10

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

clock x ∈ X(Aj ), testing that no timed transitions interleaved, and move to theinitial state q0 (Aj )).
pop
For a pop transition Ai −→ ϵ, Ai has ﬁnished its run at a ﬁnal state andrestores the previous context. E(N ) simulates, ﬁrst popping and setting eachclock (of E(N )), and set a state to q being stored in the stack.
Note that clocks of E(N ) are used for currently running TA (at the top of
the stack), and ages are used to store values of clocks of suspended TAs.
Example 3. An NeTA is shown in Fig. 4, which includes two TAs A1 and A2 .
p1 , p2 ∈ Q(A1 ), x1 , x2 ∈ X(A1 ), q1 , q2 ∈ Q(A2 ), and y1 , y2 ∈ X(A2 ), respectively. A push transition from A1 to A2 occurs at the location p2 , and the value ofx1 and x2 are 2.9 and 3.3, respectively. After pushing, y1 and y2 are reset tozero, and the system begins with q1 . The encoding DTPDA is shown in Fig. 5.
p2 is ﬁrstly pushed into the stack, and afterwards, x1 and x2 in A1 is pushed
into the stack one by one, with the initial value of the age as their respective
value. Then after y1 and y2 in A2 are reset to 0 through the states r12 , r22 , andr32 , the system moves to q1 provided the value of y1 is kept as 0.

q1

q2

y1 ← 0y2 ← 0p1

p2

x1 ← 2.9x2 ← 3.3

push

−−→N

p1

p2

x1 ← 2.9x2 ← 3.3

Fig. 4. A Push Transition on a Nested Timed Automaton

Example 4. The NeTA in Fig. 2 is encoded into a DTPDA in Fig. 6.
– The larger circles are the original states from the NeTA, while the smaller
ones are intermediate states.
internal– Since A0 −−−−−→ A1 , before q00 connects to q01 , all clocks in A1 are reset tozero and kept uniformly. q00 ﬁrstly is connected to r11 . r11 and r21 reset clocks
and t1 tests the uniformity of clocks.
push– Since A1 −−−→ A2 , each state in A1 connects to p1,2
1 by a transition to push
1,2
2
itself. p1 and p1,2
2 push each clock in A1 . Before connecting to q0 ∈ A2 , all222
clocks in A2 are similarly reset and tested, through r1 , r2 and t .
pop– Since A2 −−→ ε, after some ﬁnal state of A2 is reached, each clock in thestack should be popped, through an extra state o. After that, o will connect
each state in A1 , by which the respective suspended state is popped.

Nested Timed Automata

p2

x1 ← 2.9x2 ← 3.3
y1 ← 4.1y2 ← 0.5

push(p2 ,d)−−−−−−−−−−→Dr12

y1 ← 4.1y2 ← 0.5
x1 ← 2.9x2 ← 3.3

y1 ←[0,0](x2 , 3.3)−−−−−−−−−→D(x1 , 2.9)
(p2 , 0)r32

y1 ← 0y2 ← 0x1 ← 2.9x2 ← 3.3∗
y1 ∈[0,0]?
(x2 , 3.3)−−−−−−−−→D(x1 , 2.9)
(p2 , 0)11

x1 ← 2.9x2 ← 3.3
y1 ← 4.1y2 ← 0.5(p2 , 0)r22

y1 ← 0y2 ← 0.5
x1 ← 2.9x2 ← 3.3y2 ←[0,0](x2 , 3.3)−−−−−−−−→D(x1 , 2.9)
(p2 , 0)q1

y1 ← 0y2 ← 0x1 ← 2.9x2 ← 3.3(x2 , 3.3)
(x1 , 2.9)
(p2 , 0)p11,2push(xi ,xi )Fig. 5. Encoding the Push Transition in DTPDA
push(q01 , d)push(x, x)

q01

p1,2
2

r11

r12

q1
1 ,d

)

ǫ

q00

r22

ǫ
o

pop(q21 , d)y ∈ (0, 5]?

t2y ← [0, 2]

pus
h (q 2
1 , d)q12ǫǫx ∈ (0, 4]?

x ← [0, 0]

q21

t1

pop
(q 1
1 , d)y ∈ [0, 0]?

r21ǫy ← [0, 0]

x ← [0, 0]

x ∈ [0, 0]?

d)

pu
sh
(

1

q11

q02
y ← [0, 2]

,
(q 0
pop

x ← [0, 0]

p1,2
1

q13

pop(y, y)Fig. 6. Encoding the NeTA to DTPDA

4.2∗−−−−−−−−−−→D

Correctness of the Encoding

To reduce state reachability problem of NeTAs to that of DTPDAs, we showthat transitions are preserved and reﬂected by the encoding.
Definition 9 (Encoded Configuration). For an NeTA N = (T, A0 , ∆), its
DTPDA encoding E(N ) = ⟨S, s0 , Γ, C, ∇⟩. and an NeTA configurationc = ⟨A1 , q1 , ν1 ⟩⟨A2 , q2 , ν2 ⟩ . . . ⟨An , qn , νn ⟩

12

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

let chd = ⟨A1 , q1 , ν1 ⟩ and ctl = ⟨An , qn , νn ⟩. A clock valuation of c, ν(c) : C →R≥0 is defined as ν(c)(x) = ν1 (x) if x ∈ X(A1 ), and any, otherwise. 1 Let
w(c) = w1 · · · wn , where wi = (ximi , νi (ximi )) · · · (xi1 , νi (xi1 ))(qi , 0).
We denote a configuration (q1 , w(ctl ), ν(c)) of E(N ) by JcK. A configuration
κ of DTPDA with some c and κ = JcK is called an encoded conﬁguration.
Lemma 1. Given an NeTA N , its encoding E(N ), and configurations c, c′ ofN.
– (Preservation) if c −→ c′ , then JcK ,−→∗ Jc′ K;– (Reflection) if JcK ,−→∗ κ,
1. there exists c′ such that κ = Jc′ K and c −→∗ c′ , or
2. κ is not an encoded configuration, and there exists c′ such that κ ,−→∗Jc′ K by discrete transitions (of E(N )) and c −→∗ c′ .
The proof is given in Appendix B. From Lemma 1, we have the decidabilityof the safety property of NeTA.
Theorem 1. The state reachability problem of NeTAs is decidable.
Remark 4 (Global clocks). We can assign a disjoint ﬁnite set of global clocks
to an NeTA. These global clocks are tested and reassigned during push, pop
and internal transitions, to control time conditions for push, pop and internal
actions. Global clocks do not aﬀect the safety property of an NeTA, since during
the encoding to DTPDA, we just include these clocks to the set of clocks in
DTPDA, keeping the copies of global clocks for all stack elements.
Fact 1 A parallel composition of an NeTA and a TA can be encoded into an
NeTA with global clocks by forgetting the synchronizing actions.
Remark 5 (Encode DTPDAs into NeTAs). We can also encode a DTPDA into
an NeTA with global clocks by regarding each state of the DTPDA as a TA with
only one (local) clock. These TAs and their respective clocks can thus be used
to represent pairs of stack symbols and ages.

5

Deadline Analysis for Nested Interrupts

Timely interrupt handling is part of correctness for real-timed, interruptdriven system. It is vital for a deadline analysis [11, 12] in such systems to checkthat all speciﬁed deadlines for interrupt handling will be met. Such analysis isa daunting task because of large number of diﬀerent possible interrupt arrival
scenarios. An interrupt signal from outside transfers the control to an interrupt handler deferring the interrupted execution. When there are more than one
interrupts, an interrupt controller provides priorities for them according to urgency of each interrupt. An interrupt handler is suspended by another handler
1

any means any value, since except for a clock in the top stack frame of a nested
timed automaton, its value does not matter.

Nested Timed Automata

13with higher priority. After the high priority handler is done, the previous handler
is resumed. In the followings NeTA combined with TA is shown to be useful for
deadline analysis with such nested interrupt handling.
The time and frequency of interrupt signals can be represented by a TA,
with input actions as events that trigger interrupt handlers. For instance, Fig.
7 gives an example of a TA that trigger three interrupt handlers, by comingP ,comingQ , and comingR , respectively.

C

[6
0,
+
∈
y

+
5,
[4

←
)
,1
[0

∞
)?

comingR , x ← [0, 1)

,x

∈

gP

∞

)?

in
om
y

x ∈ (12, +∞)?

ComingP , x ← [0, 1)

x ∈ (15, +∞)?

comingQ , x ← [0, 1)

Fig. 7. A Timed Automata as an Environment

Assume a ﬁnite set of interrupt handler speciﬁcations H . Each handler is
speciﬁed by P (A, D), where A is a TA to describe its behavior, and D is its
relative deadline. A system should guarantee that each executed handler p of
P (A, D) is executed as A and reached to some ﬁnal location of A within D timeunits. If the handler misses the deadline, it raises an error.
An interrupt handler with relative deadline D is transformed from A to another TA with error location. Guarded : H → A is deﬁned by Guarded(P (A, D)) =(QG , q0G , F G , X G , ∆G ). Each element is shown as follows,– QG = Q(A) ∪ Q∆ ∪ {qerr }, where Q∆ = {qδ | for each δ ∈ ∆(A)}.
– q0G = q0 (A), and F G = F (A).
– X G = X(A) ∪ {xsch }.
– ∆G = ∆sch ∪ ∆err , where
xsch ∈[0,D]?
o• ∆sch = {q −→ qδ , qδ −−−−−−−−→ q ′ | δ = (q, o, q ′ ) ∈ ∆(A)}.
xsch ∈(D,+∞)?

• ∆err = {q −−−−−−−−−−→ qerr | q ∈ Q(A) ∪ Q∆ }.
Given a ﬁnite set of handler speciﬁcations H , a priority policy is describedby a relation ≺ on H . For instance, the most common policy is fixed priority
strategy (FPS), where ≺ is a strict partial order (irreﬂexive, asymmetric andtransitive). An interrupt controller Sch(H , ≺) with ≺ as a FPS is deﬁned by anested timed automaton (T, A0 , ∆) over a set of input symbols Σ where,– Σ = {ComingP | for each P ∈ H }.
– T = {Guarded(P ) | for each P ∈ H } ∪ {Aidle }, where Aidle is a singleton
timed automaton without any transitions.

14

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

– A0 = Aidle .
– ∆ is deﬁned by ∆idle ∪ ∆push ∪ ∆pop ∪ ∆internal , where
Coming ,pushP• ∆idle = {Aidle −−−−−−−−→ A | ∀P ∈ H , A = guarded(P )}.

Coming′ ,push• ∆push = {A −−−−−P−−−−→ A′ | ∀P, P ′ ∈ H , P ≺ P ′ ∧ A = guarded(P ) ∧A′ = guarded(P ′ )}.
pop• ∆pop = {A −−→ ε | ∀P ∈ H , A = guarded(P )}.
Coming′ ,internal• ∆internal = {A −−−−−P−−−−−−→ A′ | ∀P, P ′ ∈ H , P ̸≺ P ′ ∧P ̸≻ P ′ ∧A =guarded(P ) ∧ A′ = guarded(P ′ )}.
After performing parallel composition with a TA as an environment, we areallowed to check the deadline of each interrupt handler Pi through the reachability problem on the error location in Guarded(Pi ), considering the fact that aﬁnite number of interrupt handlers are eﬀectively invoked.

6

Related Work

After TAs [1] had been proposed, lots of researches were intended timed
context switches. TPDAs were ﬁrstly proposed in [2], which enjoys decidability ofreachability problem. Dang proved in [13] the decidability of binary reachability(i.e., the set of all pairs of conﬁgurations such that one can reach the other)of TPDAs. All clocks in TPDAs were treated globally, which were not eﬀected
when the context switches.
Our model relied heavily on a recent signiﬁcant result, named dense timed
pushdown automata (DTPDAs) [3]. The diﬀerence between DTPDAs and NeTAs was the hierarchical feature. In NeTAs, a ﬁnite set of local clocks were
pushed into the stack at the same time. When a pop action happens, the values of clocks belonging to popped TA were popped simultaneously and reused.
This feature eased much for modelling the behavior of time-aware software. In
DTPDAs, local clocks must be dealt within some proper bookkeeping process,which was not essential part of the analysis. In [14], a discrete version of DTPDAs, named discrete timed pushdown automata was introduced, where time wasincremented in discrete steps and thus the ages of clocks and stack symbols arein the natural numbers. This made the reachability problem much simpler, andeasier for eﬃcient implementation.
Based on recursive state machines [15], two similar timed extensions, timed
recursive state machines (TRSMs) [5] and recursive timed automata (RTAs) [4],were given independently. In these models, contexts were explicitly deﬁned. Finite number of clocks was distinguished into two categories, call-by-reference
and call-by-value. When entering a fresh context, clock values were stored in
the stack. After popping, the values of call-by-reference clocks were unaltered,
while the values of call-by-value ones restored to the previous value from thestack. When either all of clocks or none of them were call-by-reference, the statereachability problem was decidable. The main diﬀerences from NeTAs were, thetwo models had no stack time-update during progress transitions, and the number of clocks was essentially ﬁnite. The hierarchical timed automata (HTAs) [16]

Nested Timed Automata

15

kept the similar structure of clocks, where only a bounded number of levels weretreated, while NeTAs treated an unbounded number of levels.
The class of extended timed pushdown automata (ETPDAs) was proposedin [5]. An ETPDA was a pushdown automaton enriched with a set of clocks,
with an additional stack used to store/restore clock valuations. Two stacks wereindependently. ETPDAs have the same expressiveness with TRTMs via weak
timed bisimulation. The reachability problem of ETPDAs was undecidable, while
the decidability held with a syntactic restriction on the stack.
Controller automata (CAs) [17, 10], was proposed to analyze interrupts. In
a CA, a TA was assigned to each state. A TA at a state may be preempted byanother state by a labeled transition. The number of clocks of CAs were ﬁnite,
and thus when existing preemption loop, only the newest timed context were
kept. Given a strict partial order over states, an ordered controller automaton
was able to be faithfully encoded into a TA, and thus safety property of therestrictive version was preserved.
The updatable timed automata (UTAs) [7] proposed the possibility of updating the clocks in a more elaborate way, where the value of a clock could bereassigned to a basic arithmetic computation result of values of other clocks.
The paper gave undecidability and decidability results for several speciﬁc cases.
The expressiveness of the UTAs was also investigated. UTAs raised up anotherway to accumulate time when timed context switches, and thus updatable timed
pushdown automata (UTPDAs) could be an interesting extension.

7

Conclusion

This paper proposed a timed model called nested timed automata (NeTAs).
An NeTA was a pushdown system with a ﬁnite set of TAs as stack symbols. All
clocks in the stack elapse uniformly, capable to model the timed behavior of thesuspended components in the stack. The safety property of NeTAs was shown to
be decidable by encoding NeTAs to DTPDAs. As an example of its application,
behavior of multi-level interrupt handling is concisely modelled and its deadline
analysis is encoded as a safety property.
We are planning to develop a tool based on NeTAs. Instead of general NeTAs,
we will restrict a class such that a pop action occurs only with an integer-valued
age. We expect this subclass of NeTAs can be encoded into updatable TPDAs(without local age), which would be more eﬃciently implemented.

Acknowledgements
This work is supported by the NSFC-JSPS bilateral joint research project(61011140074), NSFC(61100052, 61003013, 61033002, 61261130589), and JSPS
KAKENHI Grant-in-Aid for Scientiﬁc Research(B) (23300008 and 25280023).

16

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

References
1. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science
126 (1994) 183–235
2. Bouajjani, A., Echahed, R., Robbana, R.: On the Automatic Veriﬁcation of Systems with Continuous Variables and Unbounded Discrete Data Structures. In:
Proceedings of the International Conference on Hybrid Systems: Computation andControl. Volume 999 of Lecture Notes in Computer Science., Springer-Verlag (1994)
64–85
3. Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-Timed Pushdown Automata. In:
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science(LICS’12), IEEE Computer Society (2012) 35–44
4. Trivedi, A., Wojtczak, D.: Recursive Timed Automata. In: Proceedings of the 8thInternational Symposium on Automated Technology for Veriﬁcation and Analysis(ATVA’10). Volume 6252 of Lecture Notes in Computer Science., Springer-Verlag(2010) 306–324
5. Benerecetti, M., Minopoli, S., Peron, A.: Analysis of Timed Recursive State Machines. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME’10), IEEE Computer Society (2010) 61–68
6. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking forReal-Time Systems. Information and Computation 111 (1994) 193–244
7. Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable Timed Automata. Theoretical Computer Science 321 (2004) 291–345
8. Ogawa, M., Cai, X.: On Reachability of Dense Timed Pushdown Automata. Technical Report IS-RR-2013-005, JAIST (2013)
9. Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In:
Lecture Notes on Concurrency and Petri Nets. Volume 3098 of Lecture Notes in
Computer Science., Springer-Verlag (2004) 87–124
10. Li, G., Yuen, S., Adachi, M.: Environmental Simulation of Real -Time Systems with
Nested Interrupts. In: Proceedings of the 3rd IEEE International Symposium on
Theoretical Aspects of Software Engineering(TASE’09), IEEE Computer Society(2009) 21–28
11. Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-Driven Software. IEEE
Transactions on Software Engineering (TSE) 30 (2004) 634–655
12. Fersman, E., Krcal, P., Pettersson, P., Yi, W.: Task Automata: Schedulability,
Decidability and Undecidability. Information and Computation 205 (2007) 1149–
1172
13. Dang, Z.: Pushdown Timed Automata: a Binary Reachability Characterizationand Safety Veriﬁcation. Theoretical Computer Science 302 (2003) 93–121
14. Abdulla, P.A., Atig, M.F., Stenman, J.: The Minimal Cost Reachability Problem
in Priced Timed Pushdown Systems. In: Proceedings of the 6th International Conference on Language and Automata Theory and Applications (LATA’12). Volume7183 of Lecture Notes in Computer Science., Springer-Verlag (2012) 58–69
15. Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis,
M.: Analysis of Recursive State Machines. ACM Transactions on Programming
Languages and Systems (TOPLAS) 27 (2005) 786–818
16. David, A., Möller, M.O.: From HUPPAAL to UPPAAL - A Translation from
Hierarchical Timed Automata to Flat Timed Automata. Technical Report RS-0111, BRICS (2001)

Nested Timed Automata

17

17. Li, G., Cai, X., Yuen, S.: Modeling and Analysis of Real-Time Systems with Mutex
Components. International Journal of Foundations of Computer Science (IJFCS)
23 (2012) 831–851

18

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen

A

Parallel Composition with Timed Automata

Assuming a nested timed automaton N = (T, A0 , ∇) and a timed automaton
A = (Q, q0 , F, X, ∆) are running concurrently over a shared ﬁnite set of actions
Σ. Σ τ = Σ ∪{τ }, where τ stands for a silent action. Transition of a nested timed
automaton is redeﬁned by ∇ ⊆ T × Σ τ × P × (T ∪ {ε}). A rule (Ai , a, Φ, Aj ) ∈ ∇a,Φ

is written as Ai −−→ Aj , where a is an action and Φ ∈ {push, pop, internal}.
Similarly, Transition of an TA is deﬁned by ∆ ⊆ Q × Σ τ × O × Q. A rulea,ϕ(qi , a, ϕ, qj ) ∈ ∆ is written as qi −−→ qj . We usually omit a when a = τ .
Definition 10 (Semantics of parallel Composition of NeTA and TA).
Given a nested timed automaton N = (T, A0 , ∇) and a timed automaton A =(Q, q0 , F, X, ∆) a finite set of actions Σ, a configuration of parallel composition
N ∥A is a tuple (q, ν, c), where q ∈ Q is a control location, ν is a clock valuation
on X, and c is stack that belongs to configurations of N . The transition relationof N ∥A is represented as,t– Progress transitions: (q, ν, c) →− P (q, ν + t, c + t).
a,ϕ– Discrete transitions: (q, ν, c) −−→P (q ′ , ν ′ , c′ ) is defined as a union of thefollowing kinds of transition relations,τ,ϕτ,ϕ• TA-movement (q, ν, c) −−→P (q ′ , ν ′ , c), if (q, ν) −−→A (q ′ , ν ′ ).
τ,ϕ

τ,ϕ

• NeTA-intra-movement (q, ν, c) −−→P (q, ν, c′ ), if c −−→N c′ .
τ,Φ

τ,Φ

• NeTA-inter-movement (q, ν, c) −−→P (q, ν, c′ ), if c −−→N c′ , whereΦ ∈ {push, pop, internal}.
τ,ϕ,pusha,ϕ• Push-synchronization (q, ν, c) −−−−−→P (q ′ , ν ′ , c′ ), if (q, ν) −−→A
a,push(q ′ , ν ′ ) and c −−−−→N c′ .
τ,ϕ,internala,ϕ• Internal-synchronization (q, ν, c) −−−−−−−−→P (q ′ , ν ′ , c′ ), if (q, ν) −−→A
a,internal(q ′ , ν ′ ) and c −−−−−−−→N c′ .
Note that there are no pop synchronization in the transitions.

B

A Proof of the Lemma 1

Lemma 1. Given an NeTA N , its encoding E(N ), and configurations c, c′ ofN.
– (Preservation) if c −→ c′ , then JcK ,−→∗ Jc′ K;– (Reflection) if JcK ,−→∗ κ,
1. there exists c′ such that κ = Jc′ K and c −→∗ c′ , or
2. κ is not an encoded configuration, and there exists c′ such that κ ,−→∗Jc′ K by discrete transitions (of E(N )) and c −→∗ c′ .
Proof. Let c = ⟨A1 , q1 , ν1 ⟩⟨A2 , q2 , ν2 ⟩ . . . ⟨An , qn , νn ⟩. Then, JcK = (q1 , w(ct ), ν(c)).
For preservation part, By case analysis of c ,−→ c′ .

Nested Timed Automata

19t

1. Progress transition: c −→N c′ = c + t and by deﬁnition.
d
2. Intra-action: c −→N c′ = ⟨A1 , q1′ , ν1′ ⟩⟨A2 , q2 , ν2 ⟩ . . . ⟨Am , qm , νm ⟩. ThendJcK −→D Jc′ K.
push

push

3. Push: c −−−→N c′ = ⟨Aj , q0 (Aj ), ν0 (Aj )⟩c if A1 −−−→ Aj .
push(x1m ,x1m )push(q1 ,d) push(x1 ,x1 )1 1
11
JcK = (q1 , w(ctl ), ν(c)) −−−−−−−→−−−−−−−−→ · · · −−−−−−−−−−→

xj ←[0,0]ϵ

xjm ←[0,0]1→− (r1j , w(c), ν(c)) −−−−−→ · · · −−−−−−−→jxj ∈[0,0]?

ϵ→− (tj , w(c), ν(⟨Aj , q0 (Aj ), ν0 (Aj )⟩)c) −−1−−−−→ Jc′ K
pop

pop

4. Pop: c −−→N c′ = ⟨A2 , q2 , ν2 ⟩ . . . ⟨An , qn , νn ⟩ if A1 −→ ϵ. Then q1 must be
in F (A1 ).
ϵ− (o, w(ctl ), ν(c))
JcK = (q1 , w(ctl ), ν(c)) →pop(x1m ,x1m ) pop(q1 ,d)pop(x1 ,x1 )

1 1
1
−−−−−
−−→ · · · −−−−−−−−−1→−−−−−−→ Jc′ K

internal

5. Inter-action: c −−−−−→N c′ = ⟨Aj , q0 (Aj ), ν0 (Aj )⟩⟨A2 , q2 , ν2 ⟩ . . . ⟨An , qn , νn ⟩internal

if A1 −−−−−→ Aj . Then q1 must be in F (A1 ).
xj ←[0,0]ϵ

xjm ←[0,0]1−−−→ · · · −−−−−−−→− (r1j , w(ctl ), ν(ch )) −−
JcK = (q1 , w(ctl ) →j

xj1 ∈[0,0]?

ϵ−→ (tj , w(c), ν(⟨Aj , q0 (Aj ), ν0 (Aj )⟩)ctl ) −−−−−−→ Jc′ K
For reflection part, by induction on the steps of ,−→∗ . Note that an encoded
conﬁguration always has a state in SN .
Base step: Consider the cases of JcK ,−→ κ:t

1. Progress transition If JcK →− D κ, then κ = (q1 , w(ctl ) + t, ν(c) + t) =t(qi , w(ctl + t), ν(c + t)) = Jc + tK. Thus we have c −→N c + t.
2. Localdϕ

If JcK −→D κ for pi → p′i being a transition in A1 , then κ =d(q1′ , w(ctl ), ν1 ) = J⟨A1 , q1′ , ν1 ⟩ctl K. We have c −→N ⟨A1 , q1′ , ν1 ⟩ctl .
3. The cases for Push and Pop are similar, here we show only push.
push(q1 ,d)push

If JcK −−−−−−−→ κ, then there exists a rule A1 −−−→ Aj for some j. By the encoding, we have κ = (p1,j
1 , ⟨q1 , d⟩w(ctl ), ν(c)), which is not an encoded conﬁguration. However, κ ,−→∗ ⟨q0 (Aj ), w(c), ν ′ ) where ν ′ (x) = 0 for x ∈ X(Aj ),pushand ν ′ (x) = ν(c)(x), otherwise. Thus c −−−→N ⟨Aj , q0 (Aj ), ν0 (X(Aj ))⟩c,κ ,−→∗ J⟨Aj , q0 (Aj ), ν0 (X(Aj ))⟩cK and during the transition no intermediate transitions become encoded conﬁgurations.
Induction step: Assume JcK ,−→∗ κ′ ,−→ κ. The transitions in E(N ) JcK is
ﬁner than that of c, and there are ﬁve cases of κ′ .
1. Original κ′ = (qi , w(c′ ), ν) for some ν and some i s.t. qi ∈ Q(Ai ). κ′ isan encoding conﬁguration and by induction hypothesis κ′ = Jc′ K. Then the
proof is similar to the base step.

20

Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuenii′′
2. Intermediate-Push κ′ = (pi,jk , ⟨xk−1 , tk−1 ⟩ · · · ⟨x1 , t1 ⟩⟨qi , 0⟩w(c ), ν) for some′′k ≤ mi + 1, ν, and some c . By induction hypothesis, we have discrete transitions κ′ ,−→,−→∗ Jc′ K and c −→∗ c′ . The transition κ′ ,−→ κ is either thediscrete transition κ′ ,−→ κ1 = κ (a discrete transition from pi,jk is determin′ t≥0istic), or the progress transition κ −→D κ for some t ∈ R . The ﬁrst case iseasy. In the second case, assume
i
i
′′
κ′ −
→D κ = κ′ +t = (pi,jk , ⟨xk−1 , tk−1 +t⟩ · · · ⟨x1 , t1 +t⟩⟨qi , d+t⟩(w(c )+t), ν+t).
t

Since each discrete transition starting from a state in Sinter ∪{o} is deterministic and commutes with a progress transition, we have κ = κ′ + t ,−→,−→∗
pushtJc′h (c′tl + t)K and c −→∗ −→N −−−→N c′h (c′tl + t).
3. Intermediate-Assignment κ′ = (rkj , w(c′′ ), ν) for some c′′ and ν; By induction hypothesis, there exist κ′ ,−→∗ Jc′ K and c −→∗ c′ such that c′ = c′h c′′ .
κ′ ,−→ κ is either a discrete transition κ′ ,−→ κ′1 = κ or a progress transition.
Let
t
κ′ −
→D κ = κ′ + t = (rkj , w(c′′ ) + t, ν + t).
4. Intermediate-Test κ′ = (tj , wc′ , ν). This case is similar to Assignment
case.
5. Intermediate-Pop κ′ = (o, ⟨xjk , tk ⟩ · · · ⟨xj1 , t1 ⟩⟨qj , d⟩wc′ , ν) with xjk , · · · , xj1 ∈X(Aj ) and qj ∈ Q(Aj ). This case is similar to Push case.