On Termination and Boundedness of Nested Updatable Timed Automata

Abstract

We introduce a model named nested updatable timed automata (NeUTAs), which can be regarded as a combination of nested timed automata (NeTAs) and updatable timed automata with one updatable clock (UTA1s). The model is suitable for soft real-time system analysis, since the updatable clock representing a deadline can be updated due to environments. A NeUTA behaves as a UTA1, in which all clocks can be tested/updated and a special clock can be incremented/decremented. It also behaves as a pushdown system, in which a UTA1 can be pushed to a stack or popped from a stack. When time elapses, all clocks (clocks in the current running UTA1 or in the stack) proceed uniformly. We show the termination and boundedness of NeUTAs are decidable.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Recently, numerous extensions of Alur and Dill’s timed automata (TAs) have been proposed to model and reason real-time systems. They increase the expressive power of TAs in various ways, such as augmenting a stack, adding more operations on clocks, and extending the original deterministic reset operation to a non-deterministic update operation.

Nested timed automata (NeTAs) [1, 2] are pushdown systems whose control locations and stack alphabet are TAs. A control location describes a working TA, and the stack presents a pile of interrupted TAs. A NeTA can 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. It is a natural model for analyzing real-time systems with context switches, e.g., interrupt systems. The reachability problem for NeTAs is shown to be decidable.

Updatable timed automata (UTAs) [3] are extensions of TAs having the ability to update clocks in a more elaborate way (i.e. increment and decrement) besides the normal operations. The reachability problem of UTAs is undecidable, which can be easily verified by encoding two counter machine with UTAs. However, there are still many decidable subclasses of UTAs by restricting the expressive power. Among them, updatable timed automata with one updatable clock (UTA1s) [4] is an interesting decidable subclass by restricting the number of updatable clocks to be one.

The aim of this paper is to combine NeTAs and UTA1s as a new model and to study the verification problems. More precisely, we replace TAs in NeTAs with UTA1s and thus get nested updatable timed automata (NeUTAs). Such kind of model is suitable for soft real-time system analysis, since the updatable clock of each UTA1 is used to describe the soft deadline, which is adjusted due to different environment. Termination and boundedness of the model are proved to be decidable, by encoding NeUTAs to vector pushdown systems, after digitizing dense time. The properties of the latter model are proved to be decidable by extending the reduced reachability tree proof technique of pushdown vector addition systems [5]. Note that pushdown vector addition systems assume the set of locations is a WQO, while the stack alphabet is finite. vector pushdown systems assume the set of locations is finite, while stack alphabet is a WQO.

Related Work. Timed automata (TAs) [6], proposed by Alur and Dill, are finite automata augmented with a finite set of clocks. Clocks can be used to record precisely how much time has elapsed in a dense manner and constrain the behaviour of the model. Although the theory of timed automata is successful in modeling and analyzing real-time systems with a large number of problems having been studied, it is so low-level that it is hard to apply it to verification of systems in reality directly. Actually many researchers are devoted to study subclasses or extensions of timed automata.

Hybrid automata [7,8,9] can be regarded as a generalization of timed automata. It is a mathematical model for mixed discrete-continuous systems, in which a discrete problem is embedded in continuous changing environments. The decidability of reachability problem is undecidable for general hybrid automata, while initialized rectangular automata form a maximum decidable subclass of hybrid automata that lies in the boundary of decidability.

Dense timed pushdown automata (DTPDAs) [10] play an essential role of the prove in this paper. DTPDAs extend timed automata with an additional stack, where a stack symbol with an age can be pushed to the stack. When time elapses, all clocks together with ages in the stack proceed uniformly. When popping, the value of the age in the top stack frame can be checked. The reachability problem for DTPDAs is shown to be EXPTIME-complete.

Interrupt timed automata (ITAs) [11, 12] intend to model timed multi-task systems with different priority levels. As extensions of TAs, each control state in ITAs is in an interrupt level, ranged from 1 to n, with exactly one active clock recording time in each interrupt level. When ITAs are in a given interrupt level, all clocks of lower interrupt levels are suspended and those of higher interrupt levels are undefined. The reachability problem for ITAs is shown to be in NEXPTIME and PTIME when the number of clocks is fixed. Though both ITAs and NeTAs can be used to model interrupt systems, they are different in what they are focus on. ITAs focus on the interrupt level, while NeTAs focus on context switches.

Paper Organization. The remainder of this paper is structured as follows: In Sect. 2 we introduce basic notations and models. Section 3 defines syntax and the semantics of UDTPDA1s. Section 4 shows that the termination and boundedness of UDTPDA1s are decidable. Section 5 introduces NeUTAs and shows the decidability on termination and boundedness by encoding NeUTAs to UDTPDA1s. Section 6 concludes this paper with summarized results.

2 Preliminaries

Let ${\mathbb {R}}^{\ge 0}$ and ${\mathbb {N}}$ be the sets of non-negative real and natural numbers, respectively. Let ${\mathbb {N}}_\omega \, {:=}\,\mathbb {N}\cup \{\omega \}$, where $\omega$ is the least limit ordinal. ${\mathcal {I}}$ denotes the set of intervals, which are (a, b), [a, b], [a, b) or (a, b] for $a\in {\mathbb {N}}$ and $b\in {\mathbb {N}}_\omega$.

Let $X=\{x_1,\ldots ,x_n\}$ be a finite set of clocks. A clock valuation $\nu : X\rightarrow {\mathbb {R}}^{\ge 0}$, assigns a value to each clock $x\in X$. $\nu _{\mathbf {0}}$ denotes the clock valuation assigning each clock in X to 0. Given a clock valuation $\nu$ and a time $t\in {\mathbb {R}}^{\ge 0}$, $(\nu +t) (x)=\nu (x)+t$, for $x\in X$. A clock assignment function $\nu [y\leftarrow b]$ is defined by $\nu [y\leftarrow b](x)= b$ if $x=y$, and $\nu (x)$ otherwise. Further, multiple clock assignment function $\nu [y_1\leftarrow b_1, \cdots , y_n\leftarrow b_n]$ is defined by $\nu [y_1\leftarrow b_1, \cdots , y_n\leftarrow b_n](x)= b_i$ if $x=y_i$ for $1 \le i \le n$, and $\nu (x)$ otherwise. ${\mathcal {V}}al(X)$ is used to denote the set of clock valuation of X.

For finite words $w = a w'$, we denote $a = head(w)$ and $w' = tail(w)$. The concatenation of two words w, v is denoted by w.v, and $\epsilon$ is the empty word. we denote the set of finite multisets over D by $\mathcal {MP}(D)$, and the union of two multisets $M, M'$ by $M \uplus M'$. We regard a finite set as a multiset with the multiplicity 1, and a finite word as a multiset by ignoring the ordering.

2.1 Updatable Timed Automata

Updatable timed automata (UTAs) [13, 14] are extensions of timed automata, based on the possibility to update the clocks in a elaborate way such as increment and decrement operations and assignments to arbitrary values. However, generally, the reachability problem of updatable timed automata is undecidable. Several decidable subclasses are investigated, based on restriction on the update abilities [3]. In [4], we proposed another decidable subclass by restricting the number of updatable clocks to be one. We will adopt the restriction in the following content paper.

Definition 1

(Updatable Timed Automata with One Updatable Clock). An updatable timed automaton with one updatable clock (UTA1) is a tuple ${\mathcal {A}}=\langle Q, q_0, X, c, \varDelta \rangle$, where

• Q is a finite set of control locations, with the initial control location $q_0\in Q$,

• $X=\{x_1,\ldots ,x_k\}$ is a finite set of normal clocks, and c is the singleton updatable clock,

• $\varDelta \subseteq Q \times Actions^{+}_{{\mathcal {A}}} \times Q$ is a finite set of actions. A (discrete) transition $\delta \in \varDelta$ is a sequence of actions $(q_1,\phi _1, q_2)\ldots (q_i,\phi _i, q_{i+1})$, written as $q_1\xrightarrow {\phi _1;\ldots ;\phi _i}q_{i+1}$, in which $\phi _j$ (for $1\le j\le i$) is one of the following

• Local $\epsilon$, an empty operation,

• Test $x \in I?$, where $x \in X \cup \{ c \}$ is a clock and $I\in {\mathcal {I}}$ is an interval,

• Assignment $x\leftarrow I$, where $x\in X \cup \{ c \}$ and $I\in {\mathcal {I}}$,

• Increment $c \,{:=}\, c+1$, and

• Decrement $c\, {:=} \,c-1$.

Similar to the definitions in [2], for an easier encoding later, a transition as a sequence of actions $q_1 \xrightarrow {\phi _1;\cdots ;\phi _i} q_{i+1}$ prohibits interleaving time progress. This can be encoded with an extra clock by resetting it to 0 and checking it still 0 after transitions, and introducing fresh control states.

Given a UTA1 ${\mathcal {A}}\in {\mathscr {A}}$, we use $Q({\mathcal {A}})$, $q_0({\mathcal {A}})$, $X({\mathcal {A}})$, $c({\mathcal {A}})$ and $\varDelta ({\mathcal {A}})$ to represent the set of control locations, the initial location, the set of normal clocks, the updatable clock and the set of actions, respectively. We will use similar notations throughout the paper.

Definition 2

(Semantics of UTA1s). Given a UTA1 ${\mathcal {A}}=\langle Q, q_0, X, c, \varDelta \rangle$, a configuration is a pair $(q,\nu )$ of a control location $q\in Q$, and a clock valuation $\nu$ on $X \cup \{ c \}$. The transition relation of the UTA1 is represented as follows,

• Progress transition: $(q,\nu )\xrightarrow {t}(q,\nu +t)$, where $t\in {\mathbb {R}}^{\ge 0}$.

• Discrete transition: $(q_1,\nu _1)\xrightarrow {\phi }(q_2,\nu _2)$, if $q_1\xrightarrow {\phi } q_2 \in \varDelta$, and one of the following holds,

  • Local $\phi =\epsilon$, then $\nu _1=\nu _2$. This operation only changes the control location and leaves the clock valuation unaltered.

  • Test $\phi = x\in I?$, $\nu _1=\nu _2$ and $\nu _2(x)\in I$ holds. The transition can be performed only if the value of x belongs to I.

  • Assignment $\phi = x\leftarrow I$, $\nu _2=\nu _1[x\leftarrow r]$ where $r\in I$. Clock x is assigned to a non-deterministic value in I.

  • Increment $\phi = c\, {:=}\, c+1$, $\nu _2=\nu _1[c\leftarrow \nu _1(c) + 1]$. The value of the updatable clock c is incremented by 1.

  • Decrement $\phi = c \,{:=}\, c-1$, $\nu _2=\nu _1[c\leftarrow \nu _1(c) - 1]$ and $\nu _1(c) \ge 1$ holds. The value of the updatable clock c is decremented by 1.

The initial configuration is $(q_0, \nu _\mathbf{0})$.

Proposition 1

The reachability problem of UTA1 under diagonal-free constraints is decidable [4].

2.2 Dense Timed Pushdown Automata

Dense timed pushdown automata [2, 10] extend timed pushdown automata with time updating in the stack. Each symbol in the stack is equipped with a local clock named an age, and all ages in the stack proceed uniformly. An age in each context is assigned to the value of a clock when a push action occurs. A pop action pops the top symbol to assign the value of its age to a specified clock.

Definition 3

(Dense Timed Pushdown Automata). A dense timed pushdown automaton is a tuple ${\mathcal {D}}=\langle Q, q_{0}, \varGamma , X, \varDelta \rangle \in {\mathscr {D}}$, where

• Q is a finite set of control locations with the initial control location $q_0 \in Q$,

• $\varGamma$ is a finite stack alphabet,

• X is a finite set of clocks, and

• $\varDelta \subseteq Q \times Actions_{{\mathcal {D}}}^{+} \times Q$ is a finite set of actions.

A (discrete) transition $\delta \in \varDelta$ is a sequence of actions $(q_1, \varphi _1, q_2), \cdots , (q_{i}, \varphi _i, q_{i+1})$ written as $q_1 \xrightarrow {\varphi _1;\cdots ;\varphi _i} q_{i+1}$, in which $\varphi _j$ (for $1 \le j \le i$) is one of the followings,

• Local $\epsilon$, an empty operation,

• Test $x \in I?$, where $x\in X$ is a clock and $I\in {\mathcal {I}}$ is an interval,

• Assign $x\leftarrow I$ where $x \in X$ and $I\in {\mathcal {I}}$,

• Push $push(\gamma ,x)$, where $\gamma \in \varGamma$ is a stack symbol and $x\in X$, and

• Pop $pop(\gamma ,x)$, where $\gamma \in \varGamma$ is a stack symbol and $x\in X$.

Definition 4

(Semantics of DTPDAs). For a dense timed pushdown automaton $\langle Q, q_0, \varGamma , X, \varDelta \rangle$, a configuration is a triplet $(q,w,\nu )$ with a control location $q \in Q$, a stack $w \in (\varGamma \times {\mathbb {R}}^{\ge 0})^{*}$, and a clock valuation $\nu$ on X. In a stack $w = (\gamma _1,t_1). \cdots .(\gamma _n,t_n)$, $\gamma _i$ is a stack symbol and $t_i$ is an age. t-time passage on the stack increases all ages in the stack by the same value, which is denoted by $w + t = (\gamma _1,t_1 + t). \cdots .(\gamma _n,t_n + t)$. The transition relation of a DTPDA is represented as follows.

• Progress transition: $(q,w,\nu )\xrightarrow {t}_{\mathscr {D}}(q,w+t,\nu +t)$, where $t\in {\mathbb {R}}^{\ge 0}$. When time elapses, all clocks together with all ages in the stack proceed uniformly.

• Discrete transition: $(q_1,w_1,\nu _1)\xrightarrow {\varphi }_{\mathscr {D}}(q_2,w_2,\nu _2)$, if $q_1\xrightarrow {\varphi } q_2$, and one of the following holds,

  • Local $\varphi =\epsilon$, then $w_1=w_2$, and $\nu _1=\nu _2$.

  • Test $\varphi =x\in I?$, then $w_1=w_2$, $\nu _1=\nu _2$ and $\nu _1(x)\in I$ holds.

  • Assign $\varphi = x\leftarrow I$, then $w_1=w_2$, $\nu _2=\nu _1[x\leftarrow r]$ where $r\in I$.

  • Push $\varphi =push(\gamma , x)$, then $\nu _1=\nu _2$, $w_2= (\gamma ,\nu _1(x)). w_1$. The stack symbol $\gamma$ and an age of the value of clock x are pushed to the stack.

  • Pop $\varphi =pop(\gamma , x)$, then $\nu _2=\nu _1[x\leftarrow t]$, $w_1= (\gamma ,t) . w_2$. The top stack frame $(\gamma ,t)$ is popped from the stack and the clock x is assigned with the value of the age t.

The initial configuration $\varrho _0= (q_0, \epsilon , \nu _\mathbf{0})$.

Remark 1

For simplicity of the later proofs, the definition of DTPDAs follows Definition 1 in [2], slightly modified from the original [10]. The former can encode the later easily.

3 Updatable Dense Timed Pushdown Automata

An updatable dense timed pushdown automaton with one updatable clock (UDTPDA1) is different from Definition 3 at:

• besides the set X of normal clocks (of the fixed number k), an updatable clock c is introduced. We refer to the normal clocks as $x_1, x_2, ..., x_k$ and sometimes we refer to the updatable clock c as $x_0$ for simplicity.

• a tuple of ages (for simplicity, we fix the length of a tuple to be $k+1$) is pushed on the stack and/or popped from the stack.

Definition 5

(UDTPDA1s). A UDTPDA1 is a tuple ${\mathcal {U}}=\langle S, s_0, \varGamma , X, c, \varDelta \rangle \in {\mathscr {U}}$, where

• S is a finite set of control locations with the initial control location $s_0\in S$,

• $\varGamma$ is a finite stack alphabet,

• X is a finite set of local clocks (with $|X| = k$),

• c is the singleton updatable clock and

• $\varDelta \subseteq S \times Action_{{\mathcal {U}}}^+\times S$ is a finite set of actions.

A (discrete) transition $\delta \in \varDelta$ is a sequence of actions $(s_1, \varphi _1, s_2), \cdots , (s_{i}, \varphi _i, s_{i+1})$ written as $s_1 \xrightarrow {\varphi _1;\cdots ;\varphi _i} s_{i+1}$, in which $\varphi _j$ (for $1 \le j \le i$) is one of the followings,

• Local $\epsilon$, an empty operation,

• Test $x \in I?$, where $x\in X \cup \{c\}$ is a clock and $I\in {\mathcal {I}}$ is an interval,

• Assign $x\leftarrow I$ where $x\in X \cup \{c\}$ and $I\in {\mathcal {I}}$,

• Increment $c\,{:=}\,c+1$,

• Decrement $c\,{:=}\,c-1$,

• Push $push(\gamma )$, where $\gamma \in \varGamma$, and

• Pop $pop(\gamma )$, where $\gamma \in \varGamma$.

Definition 6

(Semantics of UDTPDA1s). For a UDTPDA1 $\langle S, s_0, \varGamma , X, c, \varDelta \rangle$, a configuration is a triplet $(s,w,\nu )$ with a control location $s \in S$, a stack $w \in (\varGamma \times ({\mathbb {R}}^{\ge 0})^{k+1})^{*}$, and a clock valuation $\nu$ on $X \cup \{c\}$. In a stack $w = (\gamma _1,{\bar{t}}_1). \cdots .(\gamma _n,{\bar{t}}_n)$, $\gamma _i$ is a stack symbol and ${\bar{t}}_i = (t_i^0,\cdots ,t_i^{k})$ is a $k+1$-tuple of ages. t-time passage on the stack increases all ages in the stack by the same value t, which is denoted by $w + t = (\gamma _1, {\bar{t}}_1 + t). \cdots .(\gamma _n, {\bar{t}}_n + t)$ where ${\bar{t}}_i + t = (t_i^0 + t, \cdots , t_i^{k} + t)$.

The transition relation of a UDTPDA1 is represented as follows.

• Time progress: $(s,w,\nu )\xrightarrow {t}_{\mathscr {U}}(s,w+t,\nu +t)$, where $t\in {\mathbb {R}}^{\ge 0}$.

• Discrete transition: $(s_1,w_1,\nu _1)\xrightarrow {\varphi }_{\mathscr {U}}(s_2,w_2,\nu _2)$, if $s_1\xrightarrow {\varphi } s_2$, and one of the following holds,

  • Local $\varphi =\epsilon$, then $w_1=w_2$, and $\nu _1=\nu _2$.

  • Test $\varphi =x \in I?$, then $w_1=w_2$, $\nu _1=\nu _2$, and $\nu _1(x)\in I$ holds.

  • Assign $\varphi = x\leftarrow I$, then $w_1=w_2$, $\nu _2=\nu _1[x\leftarrow r]$ where $r\in I$.

  • Increment $c\,{:=}\,c+1$, then $w_1=w_2$, and $\nu _2=\nu _1[c\leftarrow \nu _1(c) + 1]$,

  • Decrement $c\,{:=}\,c-1$, then $w_1=w_2$, $\nu _2=\nu _1[c\leftarrow \nu _1(c) - 1]$ and $\nu _1(c)\ge 1$ holds,

  • Push $\varphi =push(\gamma )$, then $\nu _2= \nu _\mathbf{0}$, $w_2= (\gamma ,(\nu _1(c), \nu _1(x_1),\cdots ,\nu _1(x_k))) . w_1$ for $X = \{ x_1, \cdots , x_k \}$. The values of k+1 clocks are pushed as ages in the stack.

  • Pop $\varphi =pop(\gamma )$, then $\nu _2=\nu _1[c\leftarrow t_0, x_1\leftarrow t_1, \cdots , x_k\leftarrow t_{k}]$, $w_1= (\gamma ,(t_0,\cdots ,t_{k})) . w_2$. The values of k+1 clocks are recovered with ages in the top stack frame.

The initial configuration $\varrho _0= (s_0, \epsilon , \nu _\mathbf{0})$. We use $\hookrightarrow$ to range over these transitions, and $\hookrightarrow ^{*}$ is the reflexive and transitive closure of $\hookrightarrow$.

Example 1

  The figure shows transitions $\varrho _{1} \hookrightarrow \varrho _{2} \hookrightarrow \varrho _{3} \hookrightarrow \varrho _{4}$ of a UDTPDA1 with $S = \{ \bullet \}$ (omitted in the figure), $X = \{x_{1},x_{2}\}$ and $\varGamma = \{a,b,d\}$. All values which are changed in a transition are in bold. At $\varrho _{1} \hookrightarrow \varrho _{2}$, the values of c, $x_1$ and $x_2$ (2.3, 0.5 and 3.9) are pushed to the stack with d. After pushing, value of c, $x_1$ and $x_2$ will be reset to zero, At $\varrho _{2} \hookrightarrow \varrho _{3}$, time elapses 2.6. At $\varrho _{3} \hookrightarrow \varrho _{4}$, a increment occurs which increases the value of c from 2.6 to 3.6.

4 Termination and Boundedness of UDTPDA1s

In this section, we show that the termination and boundedness of UDTPDA1s are decidable. We first introduce vector pushdown systems and prove its decidability on termination and boundedness. Then we describe the digitization technique in UDTPDA1s using digitized configuration and its operations, which intend to simulate configurations and transitions of UDTPDA1s, respectively. Finally, the specific encoding from a UDTPDA1 to a snapshot vector pushdown system is given.

4.1 Vector Pushdown Systems

Definition 7

(Vector Pushdown Systems). A vector pushdown system is a tuple ${\mathcal {P}}=(Q, \varGamma ,{\mathbb {N}}^k, \varDelta )$, where Q is a finite set of states, $\varGamma$ is a finite stack alphabet, ${\mathbb {N}}^k$ is k-dimension natural number vectors, and $\varDelta \subseteq P\times (\varGamma \times {\mathbb {N}}^k)^{\le 2}\times P \times (\varGamma \times {\mathbb {N}}^k)^{\le 2}$. We use $\alpha , \beta , \gamma , \cdots$ to range over $\varGamma \times {\mathbb {N}}^k$, and $w, v, \cdots$ over words in $(\varGamma \times {\mathbb {N}}^k)^*$.

A configuration of ${\mathcal {P}}$ is a pair $\langle q, w\rangle$, where a state $q\in Q$ and a stack $w\in (\varGamma \times {\mathbb {N}})^*$. A transition relation $\Longrightarrow$ between configurations of ${\mathcal {P}}$ is defined by

$$\begin{aligned} \frac{(p, \gamma \rightarrow p',\gamma ') \in \varDelta }{\langle p, \gamma w\rangle \hookrightarrow \langle p',\gamma 'w\rangle }{\quad \textsc {Inter}} \quad \frac{(p, \gamma \rightarrow p',\alpha \beta ) \in \varDelta }{\langle p, \gamma w\rangle \hookrightarrow \langle p',\alpha \beta w\rangle }{\quad \textsc {Push}} \end{aligned}$$

$$\begin{aligned} \frac{(p, \gamma \rightarrow p',\epsilon ) \in \varDelta }{\langle p, \gamma w\rangle \hookrightarrow \langle p',w\rangle }{\quad \textsc {Pop}}\quad \frac{(p, \epsilon \rightarrow p',\alpha ) \in \varDelta }{\langle p, w\rangle \hookrightarrow \langle p',\alpha w\rangle }{\quad \textsc {Simple}\hbox {-}\textsc {Push}} \end{aligned}$$

$$\begin{aligned} \frac{(p, \alpha \beta \rightarrow p',\gamma ) \in \varDelta }{\langle p, \alpha \beta w\rangle \hookrightarrow \langle p',\gamma w\rangle }{\quad \textsc {Nonstandard}\hbox {-}\textsc {Pop}} \end{aligned}$$

Remark 2

In a pushdown system, the Simple-Push and Nonstandard-Pop rules can be encoded by other three rules. However, in a vector pushdown system, since the stack symbols in $\varGamma \times {\mathbb {N}}^k$ are essential unbounded, thus all of the five rules are necessary.

Let |w| denotes the length of word w and w[i] denotes the i-th symbol in w. The head h(p, w) of a configuration $\langle p,w\rangle$ is (p, w[1]) if $w\not =\epsilon$; otherwise, $h(p, w ) = (p,\bot )$. Since a finite set is well-quasi-ordered and $({\mathbb {N}}^{k}, \le )$ is well-quasi-ordered, by Dickson’s Lemma, we can obtain the set of heads of configurations is well-quasi-ordered.

Besides, we denote $a_1a_2\ldots a_m$ $\underline{\ll }$ $b_1b_2\ldots b_n$, if $m=n$ and, for each i, $a_i\le b_i$ holds, and $w{\ll }v$ if $w\underline{\ll }v$ and $w\not = v$.

The reachability tree of a VPS ${\mathcal {V}}=(Q, \varGamma ,{\mathbb {N}}^k, \varDelta )$ with an initial configuration $c_{0}$ is a rooted unordered tree defined as follows. Each node of the tree is labeled by a configuration of ${\mathcal {V}}$. The root r is labeled by the initial configuration $c_{0}$, denoted by $r : c_{0}$. Each node $n : c_n$ has a child $m : c_m$ when $c_n \hookrightarrow c_m$. Note that the reachability tree of ${\mathcal {V}}$ is finitely branching since $\varDelta$ is finite.

Termination Problem. The termination problem asks whether all runs of a given system are finite, we have the following definition.

Definition 8

A node $s : \langle p, w \rangle$ pumps a node $t : \langle q, v\rangle$ if

• there is a path from s to t, and every node $t' : \langle p', w'\rangle$ on it satisfies $|w'| \ge |w|$.

• $h(\langle p, w \rangle )\trianglelefteq h(\langle q, v \rangle )$, i.e., $p \preceq q$ and either $w=\epsilon$ or $w[1] \le v[1]$.

We call a node pumpable if there exists a node pumping it. The notion of pumpable nodes is similar to subsumed nodes in [5], but we consider the increase of heads instead of states. Let the reduced reachability tree be the largest prefix of the reachability tree such that every pumpable node has no children.

The intuition of pumpable nodes is that if the run from $\langle p,w\rangle$ to $\langle q, v\rangle$ only changes the top element of w, then we can simulate this run from $\langle q, v\rangle$ to some $\langle q',v'\rangle$ by monotonicity, satisfying $p\preceq q\preceq q'$, and $w[1]\le v[1]\le v'[1]$. We can construct an infinite run by repeating this process.

Conversely, assume $\langle p_0,w_0\rangle \hookrightarrow \langle p_1,w_1\rangle \cdots$ is an infinite run, we can extract an infinite subsequence, say $\langle p_{i_0},w_{i_0}\rangle , \langle p_{i_1},w_{i_1}\rangle , \cdots$, such that each node is chosen if it has the minimal depth of the stack in its suffix run. Note that each pair of $\langle p_{i_k},w_{i_k}\rangle$ and $\langle p_{i_j},w_{i_j}\rangle$ with $k<j$ in this subsequence satisfies the first condition of pumpable nodes. By the fact that the set of heads is well-quasi-ordered, it must contain a pumpable node.

Theorem 1

A VPS has an infinite run if, and only if, its reduced reachability tree contains a pumpable node.

Boundedness Problem. The boundedness asks whether the reachability set is finite. We know that any infinite run has a pumpable node. If a pumpable node is exactly the same as the one that pumps it, still an infinite run keeps the reachability set finite. Otherwise, a VPS enlarges reachable configurations infinitely.

Definition 9

A node $s:\langle p, w\rangle$ strictly pumps a node $t:\langle q, v\rangle$ if s pumps t, and either $|w|<|v|$ or $h(\langle p, w\rangle ) \triangleleft h(\langle q, v\rangle )$.

Theorem 2

A VPS has an infinite reachability set if, and only if, its reduced reachability tree contains a strictly pumpable node.

Proof

(Only-if) Assume a VPS ${\mathcal {V}}$ has an infinite reachability set. Let ${\mathcal {T}}$ be the largest prefix of its reachability tree such that, on each branch, all nodes have distinct labels. The tree ${\mathcal {T}}$ is infinite since every configuration in the reachability set is a node in ${\mathcal {T}}$.

By K${\ddot{o}}$nig’s lemma, it follows that ${\mathcal {T}}$ contains finitely many branches in which all nodes are distinct. Since the reduced reachability tree of ${\mathcal {V}}$ is finite, among finitely many branches, there are two nodes n : (p, w) and m : (q, v) such that they are in the reduced reachability tree and n pumps m.

Thus, $(p, w) \ne (q, v)$ and (p, w) pumps (q, v). By definition of pumpable nodes, we have two cases: (1) $|w| < |v|$, and (2) $|w| = |v|$. In case (2), either $w \ll v$ or $p\prec q$ holds. $w[2,|w| ] = v[2,|v| ]$ implies either $w[1]<v[1]$ or $p\prec q$. Thus, both cases, n strictly pumps m.

(If) Similar to that of Theorem 1. The path from the root to a strictly pumpable node yields a run

$$\begin{aligned} (p_0, w_0) \overset{op_1}{\longrightarrow } \ldots \overset{op_k}{\longrightarrow } (p_k, w_k) \overset{op_{k+1}}{\longrightarrow } \ldots \overset{op_l}{\longrightarrow }(p_l, w_l) \end{aligned}$$

such that $(p_k, w_k)$ strictly pumps $(p_l, w_l)$, which leads an infinite run by iterating the sequence of operations $op_{k+1}, ..., op_l$. As the case analysis, if $|w| < |v|$, the resulting infinite run enlarges the length of the stack infinitely; if $w[1] < v[1]$, the resulting infinite run enlarges the top element of the stack infinitely.

4.2 Digitized Configuration and Its Operations

Let $\langle S, s_0, \varGamma , X, c, \varDelta \rangle$ be a UDTPDA1, and let n be the largest integer (except for $\omega$) appearing in $\varDelta$. For $v \in {\mathbb {R}}^{\ge 0}$, $proj(v) = \mathtt{r}_i$ if $v \in \mathtt{r}_i \in Intv(n)$, where

$$\begin{aligned} Intv(n) =\{ \mathtt{r}_{2i}=[i,i] \mid 0 \le i \le n\} \cup \{ \mathtt{r}_{2i+1} = (i,i+1) \mid 0 \le i < n\} \cup \{ \mathtt{r}_{2n+1} = (n,\omega )\} \end{aligned}$$

The idea of the next digitization is inspired by [15,16,17].

Definition 10

(Digitization). Let $frac(t) = t - floor(t)$ for $t \in {\mathbb {R}}^{\ge 0}$. A digitization function $\mathtt{digi} : \mathcal {MP}((\{c\} \cup X \cup \varGamma ) \times {\mathbb {R}}^{\ge 0}) \rightarrow \mathcal {MP}((\{c\} \cup X \cup \varGamma ) \times Intv(n))^*$ is defined as follows.

For $\bar{{\mathcal {Y}}} \in \mathcal {MP}((\{c\}\cup X \cup \varGamma ) \times {\mathbb {R}}^{\ge 0})$, let $Y_0, Y_1, \cdots , Y_m$ be multisets that collect (x, proj(t))’s having the same frac(x, t) for $(x, t) \in \bar{{\mathcal {Y}}}$. Among them, $Y_0$ (which is possibly empty) is reserved for the collection of (x, proj(t)) with $frac(t) = 0$. We assume that $Y_i$’s except for $Y_0$ is non-empty (i.e., $Y_i = \emptyset$ with $i>0$ is omitted), and $Y_i$’s are sorted by the increasing order of frac(t) (i.e., $frac(t) < frac(t')$ for $(x, proj(t)) \in Y_i$ and $(x', proj(t')) \in Y_{i+1}$). Thus, $\mathtt{digi}(\bar{{\mathcal {Y}}})$ is a word ${\bar{Y}} = Y_0Y_1\cdots Y_m$.

For a stack frame $v = (\gamma , (t_0, \cdots , t_{k}))$ of a UDTPDA1, we denote a word $(\gamma ,t_0) \cdots (\gamma ,t_{k})$ by dist(v). Given a clock valuation $\nu$, we denote a clock word $(c, \nu (c))(x_1,\nu (x_1)) \ldots (x_n, \nu (x_k))$ by $time(\nu )$ where c is the singleton updatable clock and $x_i\in X$ for $1 \le i \le k$.

Example 2

In Example 1, we assume $n = 6$ and have 13 intervals illustrated below.

For the configuration $\varrho _1 = (\bullet , v_4 \cdots v_1,\nu )$ in Example 1, let $\bar{{\mathcal {Y}}} = dist(v_4) \uplus time(\nu )$ be a word, and ${\bar{Y}}=\mathtt{digi}(\bar{{\mathcal {Y}}})$, then

$$\begin{aligned} \bar{{\mathcal {Y}}}&= \{(a,1.5), (a,1.9), (a,4.5), (c, 2.3), (x_1, 0.5), (x_2, 3.9)\}\\ {\bar{Y}}&= \{\}\{(c,\mathtt{r}_{5})\} \{(x_{1},\mathtt{r}_{1}), (a,\mathtt{r}_{3}) ,(a,\mathtt{r}_{9})\}\{(x_{2},\mathtt{r}_{7}),(a,\mathtt{r}_{3})\}\\ \end{aligned}$$

Definition 11

(Digiword). A word ${\bar{Y}} \in \mathcal {MP}((\{c\} \cup X \cup \varGamma ) \times Intv(n))^*$ is a digiword if the following is satisfied:

• Let a $k+1$-pointer ${\bar{\rho }}$ of ${\bar{U}}$ is a tuple of $k+1$ pointers to mutually different $k+1$ elements in ${\bar{U}}$. Then there are a pair of $k+1$-pointers $({\bar{\rho }}_1,{\bar{\rho }}_2)$ in ${\bar{Y}}$ that point to clocks and ages in the topmost stack frame, respectively.

• For every element in ${\bar{Y}}$, either ${\bar{\rho }}_1$ or ${\bar{\rho }}_2$ points to it.

We refer the element $(\gamma , \mathtt{r})$ pointed by the i-th pointer by ${\bar{\rho }}[i]$ where $0 \le i \le k$. Let the set Digi contains all digiwords. Digi is a finite set by observing that at most $2k+2$ elements exist in a digiword.

A digiword ${\bar{Y}}$ intends to be the digitization of the current clock valuation (pointed by ${\bar{\rho }}_1$) and the topmost stack frame (pointed by ${\bar{\rho }}_2$) in a UDTPDA1. More precisely, for $0 \le i \le k$, ${\bar{\rho }}_1[i]$ points to $(x_i, proj(\nu (x_i)))$ for $(x_i, \nu (x_i)) \in time(\nu )$ where $\nu$ is the clock valuation and ${\bar{\rho }}_2[i]$ points to $(\gamma , proj(t_i))$ for $(\gamma , t_i) \in dist(v)$ where v is the topmost stack frame.

Definition 12

(Digitized Configuration). A digitized configuration is a tuple ${\bar{U}} \in Digi \times N^2$, which contains a digiword and a pair of natural numbers. The pair of natural numbers intend to roughly record the time passage when the value of updatable clocks in the current clock valuation and the topmost stack frame exceed the maximum integer n. Each time the updatable clocks value exceeds n and meanwhile its value changes between integer and non-integer with time elapsing, we increase the corresponding natural number by one.

Example 3

The word ${\bar{Y}}$ in Example 2 can be extended to a digitized configuration ${\bar{U}}$ by adding a pair of 3-pointers $(\bar{\rho _1}, \bar{\rho _2})$ (pointers are marked with the numbered overlines and underlines). and a pair of numbers (0, 0).

${\begin{array}{rl} {\bar{U}}= &{} ( \{\} \{\overline{(c,\mathtt{r}_{5})}^0\}\{\overline{(x_{1},\mathtt{r}_{1})}^1, \underline{(a,\mathtt{r}_{3})}_0 , \underline{(a,\mathtt{r}_{9})}_2\}\{\overline{(x_{2},\mathtt{r}_{7})}^2,\underline{(a,\mathtt{r}_{3})}_1\}, 0, 0)\\ \end{array} }$

Pointers are given more explicitly below:

${\begin{array}{lll} \bar{\rho _1}(0) = (c,\mathtt{r}_{5}) \quad &{}\bar{\rho _1}(1) = (x_{1},\mathtt{r}_{1}) \quad &{} \bar{\rho _1}(2) = (x_{2},\mathtt{r}_{7}) \\ \bar{\rho _2}(0) = (a,\mathtt{r}_{3}) &{}\bar{\rho _2}(1) = (a,\mathtt{r}_{3}) &{}\bar{\rho _2}(2) = (a,\mathtt{r}_{9}) \\ \end{array}}$

Definition 13

(Operations on Digitized Configuration). Let ${\bar{U}} = (Y_0 \cdots Y_m, num_1, num_2), {\bar{U}}' = (Y'_0 \cdots Y'_{m'}, num'_1,num'_2), {\bar{V}} = (Y''_0 \cdots Y''_m,num''_1, num''_2) \in Digi \times {\mathbb {N}}^2$ are digitized configurations such that ${\bar{U}}$ (resp. ${\bar{U}}'$ and ${\bar{V}}$) has a pair of $k+1$-pointers $({\bar{\rho }}_1, {\bar{\rho }}_2)$ (resp. $({\bar{\rho }}'_1, {\bar{\rho }}'_2)$ and $({\bar{\rho }}''_1, {\bar{\rho }}''_2)$). We define operations as follows which are used to simulate transitions of UDTPDA1s in the next subsection. Note that except for Rotate, $\mathbf{Map}$, and $\mathbf{Propogate}$, the $k+1$-pointers ${\bar{\rho }}_1$ is changed corresponding to the operation to ensure that properties of digiwords are still satisfied after operations. Namely when an element is removed, the pointer which points to it is set to empty. And when an element $(x_i, \mathtt{r})$ for $x_i \in \{c\}\cup X$ is added, the pointer ${\bar{\rho }}_1[i]$ is modified to point to that new element.

• $\mathbf{Insert}_x$ : $insert_x({\bar{U}},(x,\mathtt{r}_{i}))$ for $x \in X$ inserts $(x, \mathtt{r}_{i})$ to ${\bar{U}}$ (may nondeterministically) at

  $$\begin{aligned} \left\{ \begin{array}{l@{\quad }l} either\,\, put\,\, into\,\, Y_j\,\, for\,\, j > 0,\,\, or\\ \qquad ~~ \,put\,\, the\,\, singleton\,\, set \,\, \{(x, \mathtt{r}_{i})\} \,\, at\,\, any\,\, place\,\,after\,\, Y_0 &{} if\,\, i\,\, is \,\,odd \\ put\,\, into\,\, Y_0 &{} if\,\, i\,\, is\,\, even \\ \end{array} \right. \end{aligned}$$

• $\mathbf{Insert}_c$ : $insert_c({\bar{U}},(c,\mathtt{r}_{i}))$ for the updatable clock c inserts $(c, \mathtt{r}_{i})$ to ${\bar{U}}$ and updates natural number $num_1$ in one of three following ways:

  $$\begin{aligned} \left\{ \begin{array}{l@{\quad }l} { (1)} \,\, either\,\, put\,\, (c,\, \mathtt{r}_i) \,\, into\,\, Y_{j}\,\, for \,\, j > 0,\,\, or\\ ~~~put\,\, the\,\, singleton \,\,set\,\, \{(c,\, \mathtt{r}_{i})\} \,\,at \,\,any\,\, place\,\, after \,\, Y_0 \\ ~~\,\, and \,\,\ num_1=0 &{} if \,\, i \,\, \le 2n \,\, and\,\, i\,\, is\,\, odd \\ { (2)} \,\, put\,\, (x,\, \mathtt{r}_{i}) \,\,into\,\, Y_0\,\, and \,\,num_1=0 &{} if \,\,i \le 2n \,\,and \,\, i \,\, is\,\, even \\ { (3)} \,\, either\,\, put \,\,(c,\, \mathtt{r}_{i})\,\, into \,\, Y_{j}\,\, for\,\, j \ge 0,\,\, or\\ ~~~put\,\, the\,\, singleton\,\, set\,\, \{(c,\, \mathtt{r}_{i})\} \,\,at\,\, any\,\, place \,\, after \,\, Y_0 \\ ~~ ~and \,\,num_1=d,\,\, where\,\,d\,\, is\,\, a\,\, positive\,\, integer \\ ~~~and \,\,d\,\, is \,\,odd \,\,if \,\,(c,\, \mathtt{r}_{i})\,\, is\,\, put\,\, into \,\,Y_0 \,\,otherwise \,\,even &{} if \,\, i = 2n+1 \\ \end{array} \right. \end{aligned}$$

• Init: For ${\bar{U}} = (Y_0 \cdots Y_m,num_1, num_2)$, $init({\bar{U}})$ is obtained by updating $Y_0$ with $Y_0 \uplus \{ (x_i, \mathtt{r}_0) \mid x_i \in \{c\}\cup X \}$ and $num_1$ with 0.

• Delete: $delete({\bar{U}},x)$ for $x \in \{c\} \cup X$ is obtained from ${\bar{U}}$ by deleting the element $(x,\mathtt{r})$ indexed by x.

• Increase: $increase({\bar{U}})$ is obtained from ${\bar{U}}$ by replacing the element $(c,\mathtt{r}_i)$ indexed by c with element $(c,\mathtt{r}_{min\{i+2, 2n+1\}})$ and updating $num_1$ as follows:

  $$\begin{aligned} \left\{ \begin{array}{l@{\quad }l} num_1 \,{:=}\, num_1 &{} if \,\, i < 2n - 1 \\ num_1 \,{:=}\, num_1 + 1 &{} if\,\, i = 2n - 1\\ num_1 \,{:=}\, num_1 + 2 &{} otherwise \end{array} \right. \end{aligned}$$

• Decrease: $decrease({\bar{U}})$ is obtained from ${\bar{U}}$ by replacing the element $(c,\mathtt{r}_i)$ indexed by c with element $(c,\mathtt{r}_{j})$ and updating $num_1$ as follows:

  $$\begin{aligned} \left\{ \begin{array}{l@{\quad }l} j = max(i - 2, 0) ~~\,\, and \,\,~~num_1\, {:=}\, num_1 &{} if \,\, num_1 \le 1 \\ j = i - 1\,\, and\,\, num_1 \,{:=}\, 0 &{} else \,\, if \,\, num_1 = 2 \\ j = i\,\,and \,\,num_1\, {:=} \, num_1 - 2 &{} otherwise \end{array} \right. \end{aligned}$$

• Rotate: Rotate intends to simulate the time progress transition. A rotation ${\bar{U}} = (Y_0 \cdots Y_m, num_1, num_2) \Rightarrow {\bar{U}}' = (Y_0' \cdots Y_{m'}', num'_1, num'_2)$ is defined as follows.

  $$\begin{aligned} \left\{ \begin{array}{lll} {\bar{U}}'= &{}(Y'_0\cdots Y'_{m+1}, &{} if\, Y_0 \ne \emptyset ,\,\, Y'_0 = \emptyset ,\,\, Y'_1 = \{(\gamma ,\mathtt{r}_{min\{i+1, 2n+1\}}) \\ &{} num'_1, num'_2) &{} \mid (\gamma ,\mathtt{r}_i) \in Y_0\},\,\,Y'_j = Y_{j-1}\,\, for\,\,j \in [2..m+1], \\ &{} &{} num'_1=num_1+1 \,\,if\,\, (c,\, \mathtt{r}_i) \in Y_0\,\,and \,\,i \ge 2n \\ &{} &{} otherwise\,\,num_1,\,\, and\,\, num'_2=num_2+1\,\, if \\ &{} &{} \bar{\rho }_1[0] = (\gamma ,\, \mathtt{r}_i) \in Y_0\,\, and \,\,i \ge 2n,\,\, otherwise \\ &{} &{} num_2 + 1. \\ {\bar{U}}'= &{}(Y'_0\cdots Y'_{m-1}, &{} otherwise, \,\,Y'_0=\{(\gamma ,\mathtt{r}_{min\{i+1, 2n+1\}}) \mid (\gamma ,\mathtt{r}_i) \in Y_m\}, \\ &{} num'_1, num'_2) &{} Y'_j=Y_j\,\, for\,\,j \in [1..m-1], \,\,num'_1=num_1+1, \\ &{} &{} if\,\,(c, \mathtt{r}_i) \in Y_m\,\, and \,\,i \ge 2n, \,\,otherwise \,\,num_1, \\ &{} &{} and\,\, num'_2=num_2+1 \,\,if\,\,{\bar{\rho }}_1[0] = (\gamma , \mathtt{r}_i) \in Y_m \\ &{} &{} and\,\, i \ge 2n,\,\, otherwise\,\,num_2. \\ \end{array} \right. \end{aligned}$$

  $({\bar{\rho }}_1,{\bar{\rho }}_2)$ are updated to correspond to the permutation accordingly. As convention, we define $\Rightarrow ^*$ as reflexive transitive closure of $\Rightarrow$.

• Map: Map intends to simulate the push transition. $map({\bar{U}},\gamma )$ for $\gamma \in \varGamma$ is obtained from ${\bar{U}}$ by the following operations. First delete all elements pointed by ${\bar{\rho }}_2$. Then replace $(x, \mathtt{r}_j)$ pointed by ${\bar{\rho }}_1$ for $x \in \{c\} \cup X$ with $(\gamma , \mathtt{r}_j)$ and set ${\bar{\rho }}_2$ to point to that. Finally assign value of $num_1$ to $num_2$.

• Propogate: Propogate intends to simulate the pop transition. $propogate({\bar{U}},{\bar{U}}',\gamma )$ for $\gamma \in \varGamma$ is set to be ${\bar{V}}$ which is obtained by finding a rotation ${\bar{U}}' \Rightarrow ^* {\bar{V}}$ such that ${\bar{\rho }}''_1$ of ${\bar{V}}$ matches the original ${\bar{\rho }}_2$ of ${\bar{U}}$. That is to say, for $0 \le i \le k$, ${\bar{\rho }}''_1[i] = (x, \mathtt{r}_m)$ and ${\bar{\rho }}_2[i] = (\gamma , \mathtt{r}_n)$, we have $m = n$.

Example 4

We begin with the digitized configuration ${\bar{U}}$ in Example 3, to simulate transitions $\varrho _1\hookrightarrow ^*\varrho _4$ in Example 1.

• push(d) is simulated by ${\bar{U}}_1=init(map({\bar{U}},d))$.

  $\begin{array}{rl} {\bar{U}}_1= &{} ( \{\overline{(c,\mathtt{r}_{0})}^0, \overline{(x_1,\mathtt{r}_{0})}^1, \overline{(x_2,\mathtt{r}_{0})}^2\} \{\underline{(d,\mathtt{r}_{5})}_0\} \{\underline{(d,\mathtt{r}_{1})}_1\}\{\underline{(d,\mathtt{r}_{7})}_2\}, 0, 0)\\ \end{array}$

• Time elapse of 2.6 time units is simulated by ${\bar{U}}_1 \Rightarrow ^* {\bar{U}}_2$

  $\begin{array}{rl} {\bar{U}}_2= &{} ( \{\}\{\underline{(d,\mathtt{r}_{7})}_1\}\{\underline{(d,\mathtt{r}_{13})}_2\} \{\overline{(c,\mathtt{r}_{5})}^0, \overline{(x_1,\mathtt{r}_{5})}^1, \overline{(x_2,\mathtt{r}_{5})}^2\} \{\underline{(d,\mathtt{r}_{9})}_0\} , 0, 0)\\ \end{array}$

• $c\, {:=}\, c+1$ is simulated by ${\bar{U}}_3=increase({\bar{U}}_2)$.

  $\begin{array}{rl} {\bar{U}}_3= &{} ( \{\}\{\underline{(d,\mathtt{r}_{7})}_1\}\{\underline{(d,\mathtt{r}_{13})}_2\} \{\overline{(c,\mathtt{r}_{7})}^0, \overline{(x_1,\mathtt{r}_{5})}^1, \overline{(x_2,\mathtt{r}_{5})}^2\} \{\underline{(d,\mathtt{r}_{9})}_0\} , 0, 0)\\ \end{array}$

4.3 Snapshot Vector Pushdown System

A snapshot vector pushdown system (snapshot VPS) keeps the digitization of clock valuation and ages in the top stack frame and a pair of natural numbers that record roughly how much the current updatable clock pointed by ${\bar{\rho }}_1[0]$ and the age of element pointed by ${\bar{\rho }}_2[0]$ exceed the maximum integer n in the top stack frame, as a digitized configuration.

We show that a UDTPDA1 is encoded into its digitization, called a snapshot VPS. The keys of the encoding are, when a pop occurs, the time progress recorded at the top stack symbol is propagated to the next stack symbol after finding a series of rotations by matching between $k+1$-pointers ${\bar{\rho }}_2$ and ${\bar{\rho }}'_1$. Using digitized configuration and its operations defined in the last subsection, the encoding is quite natural.

Definition 14

Let $\pi : \varrho _0 = (s_0, \epsilon , \nu _\mathbf{0}) \hookrightarrow ^{*} \varrho = (s, w, \nu )$ be a transition sequence of a UDTPDA1 from the initial configuration. If $\pi$ is not empty, we refer the last step as $\lambda : \varrho ' \hookrightarrow \varrho$, and the preceding sequence by $\pi ': \varrho _0 \hookrightarrow ^{*} \varrho '$. Let $w = v_m \cdots v_1$. A snapshot is a digitized configuration $snap(\pi ) = ({\bar{Y}}, num_1, num_2)$, where $num_1 = 2\times (floor(\nu (c)) - n) + ceiling(frac(\nu (c)))$, $num_2 = 2\times (floor(t_0) - n) + ceiling(frac(t_0))$ if w is not empty and $v_m=(\gamma , t_0, \cdots , t_{k})$, otherwise $num_2 = 0$, and ${\bar{Y}} = \mathtt{digi}(dist(v_m) \uplus time(\nu ))$.

In $snap(\pi )$, we define the $k+1$-pointer ${\bar{\rho }}_1[i] = (x_i,\nu (x_i))$ for $0 \le i \le k$. We also define ${\bar{\rho }}_2[i] = (\gamma , proj(t_i))$ for $(\gamma ,t_i) \in dist(v_m)$ if w is not empty, otherwise ${\bar{\rho }}_2$ is left undefined. A snapshot configuration $Snap(\pi )$ is inductively defined from $Snap(\pi ')$.

$$\begin{aligned} \left\{ \begin{array}{l@{\quad }l} (s_0, snap(\epsilon )) \quad \qquad \,\, if\,\, \pi = \epsilon .\\ (s', snap(\pi )~tail(Snap(\pi '))) \qquad \,\, if \,\, \lambda \,\, is \,\, \mathbf{Time progress},\mathbf{Local}, \mathbf{Test}, \\ \qquad \qquad \qquad \quad \qquad \qquad \qquad \mathbf{Assign},\,\, \mathbf{Increment}\,\, and\,\, \mathbf{Decrement}. \\ (s', snap(\pi )~Snap(\pi ')) \qquad \,\, if \,\, \lambda \,\, is \,\, \mathbf{Push}. \\ (s', snap(\pi )~tail(tail(Snap(\pi ')))) \quad \,\, if\,\, \lambda \,\, is \,\, \mathbf{Pop}. \\ \end{array} \right. \end{aligned}$$

Definition 15

For a UDTPDA1 $\langle S, s_0, \varGamma , X, c, \varDelta \rangle$, we define the corresponding encoded snapshot VPS $\langle S, s_0, Digi,{\mathbb {N}}^2, \varDelta _d \rangle$ with the initial configuration $\langle s_0, snap(\epsilon ) \rangle$. Then $\varDelta _d$ consists of:

• Time progress $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s, {\bar{U}}'\rangle$ for ${\bar{U}} \Rightarrow ^{*} {\bar{U}}'$.

• Local ($s \xrightarrow {\epsilon } s' \in \varDelta$) $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', {\bar{U}} \rangle$.

• Test ($s \xrightarrow {x \in I?} s' \in \varDelta$ with $x\in X \cup \{c\}$) If $\mathtt{r}_i \subseteq I$ and $(x,\mathtt{r}_i) \in {\bar{Y}}$, where ${\bar{U}}=({\bar{Y}}, num_1, num_2)$, $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', {\bar{U}} \rangle$.

• Assign ($s \xrightarrow {x \leftarrow I} s' \in \varDelta$ with $x\in X$) For $\mathtt{r}_i \subseteq I$,

  $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', (insert_x(delete({\bar{U}},x),(x,\mathtt{r}_i))) \rangle$.

• Assign ($s \xrightarrow {c \leftarrow I} s' \in \varDelta$) For $\mathtt{r}_i \subseteq I$,

  $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', (insert_c(delete({\bar{U}},c),(c,\mathtt{r}_i))) \rangle$.

• Increment ($s \xrightarrow {c \,{:=}\, c+1} s' \in \varDelta$)

  $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', increase({\bar{U}}) \rangle$.

• Decrement ($s \xrightarrow {c\, {:=}\, c-1} s' \in \varDelta$)

  $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', decrease({\bar{U}}) \rangle$.

• Push ($s \xrightarrow {push(\gamma )} s' \in \varDelta$)

  $\langle s, {\bar{U}} \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', (init(map({\bar{U}},\gamma ))) {\bar{U}} \rangle$.

• Pop ($s \xrightarrow {pop(\gamma )} s' \in \varDelta$)

  $\langle s, {\bar{U}} {\bar{U}}' \rangle \hookrightarrow _{{\mathcal {S}}} \langle s', propagate({\bar{U}}, {\bar{U}}', \gamma ) \rangle$.

By induction on the number of steps of transitions, the encoding relation between a UDTPDA1 with a single updatable clock and a snapshot VPS is observed.

Lemma 1

Let us denote $\varrho _0$ and $\varrho$ (resp. $\langle s_0, {\tilde{w}}_0 \rangle$ and $\langle s, {\tilde{w}} \rangle$) for the initial configuration and a configuration of a UDTPDA1 (resp. its snapshot VPS ${{\mathcal {S}}}$).

• (Preservation) If $\pi : \varrho _0 \hookrightarrow ^{*} \varrho$, there exists $\langle s, {\tilde{w}} \rangle$ such that $\langle s_0, {\tilde{w}}_0 \rangle \hookrightarrow ^{*}_{{\mathcal {S}}} \langle s, {\tilde{w}} \rangle$ and $Snap(\pi ) = \langle s, {\tilde{w}} \rangle$.

• (Reflection) If $\langle s_0, {\tilde{w}}_{0} \rangle \hookrightarrow ^{*}_{{\mathcal {S}}} \langle s, {\tilde{w}} \rangle$, there exists $\pi : \varrho _0 \hookrightarrow ^{*} \varrho$ with $Snap(\pi ) = \langle s, {\tilde{w}} \rangle$.

5 Nested Updatable Timed Automata

5.1 Nested Updatable Timed Automata

Nested Updatable Timed Automata(NeUTAs) extend NeTAs [1, 2] by replacing every TA in NeTAs to a UTA1. A NeUTA has internal transitions, in which it will behave as a individual UTA1 having local, test, assign, increment and decrement transitions, and push and pop transitions. The stack of a NeUTA contains a pile of UTA1s which have been pushed.

Definition 16

(Nested Updatable Timed Automata). A nested updatable timed automaton (NeUTA) is a quadruplet ${\mathcal {N}}=(T,{\mathcal {A}}_0, X, c,\varDelta )$, where

• T is a finite set $\{{\mathcal {A}}_0,{\mathcal {A}}_1, \cdots , {\mathcal {A}}_m\}$ of UTA1s, with the initial UTA1 ${\mathcal {A}}_0\in T$. We assume the sets of states of ${\mathcal {A}}_i$, denoted by $S({\mathcal {A}}_i)$, are mutually disjoint, i.e., $S({\mathcal {A}}_i) \cap S({\mathcal {A}}_{j}) = \emptyset$ for $i \ne j$. We denote the initial state of ${{\mathcal {A}}_i}$ by $q_0({{\mathcal {A}}_i})$.

• X is the finite set of k local clocks and c is the updatable clock.

• $\varDelta \subseteq Q \times (Q \cup \{\varepsilon \}) \times Actions \times Q \times (Q \cup \{\varepsilon \})$ describes transition rules below, where $Q = \cup _{{\mathcal {A}}_i \in T} S({\mathcal {A}}_i)$.

• Internal $(q, \varepsilon , internal, q', \varepsilon )$, which describes an internal transition in the working UTA1 (placed at a control location) with $q,q' \in {\mathcal {A}}_{i}$.

• Push $(q, \varepsilon , push, q_0({\mathcal {A}}_{i'}), q)$, which interrupts the currently working UTA1 ${\mathcal {A}}_i$ at $q \in S({\mathcal {A}}_i)$. Then, a UTA1 ${\mathcal {A}}_{i'}$ newly starts.

• Pop $(q, q', pop, q', \varepsilon )$, which restarts ${\mathcal {A}}_{i'}$ in the stack from $q' \in S({\mathcal {A}}_{i'})$ after ${\mathcal {A}}_i$ has finished at $q \in S({\mathcal {A}}_i)$.

Definition 17

(Semantics of NeUTAs). Given a NeUTA $(T,{\mathcal {A}}_0, X, c, \varDelta )$, the current control state is referred by q. Let ${\mathcal {V}}al_X = \{ \nu : X \cup \{c\} \rightarrow {{\mathbb {R}}}^{\ge 0} \}$. A configuration of a NeUTA is an element in $(Q \times {\mathcal {V}}al_X , (Q \times {\mathcal {V}}al_X)^{*})$.

• Time progress transitions: $(\langle q, \nu \rangle , v) \xrightarrow {t} (\langle q, \nu +t \rangle , v + t)$ for $t \in {{\mathbb {R}}}^{\ge 0}$, where $v + t$ set $\nu '\, {:=}\, \nu ' + t$ of each $\langle q', \nu ' \rangle$ in the stack.

• Discrete transitions: $\kappa \xrightarrow {\varphi } \kappa '$ is defined as follows.

  • Internal $(\langle q, \nu \rangle , v) \xrightarrow {\varphi } (\langle q', \nu ' \rangle , v)$, if $\langle q,\nu \rangle \xrightarrow {\varphi } \langle q', \nu ' \rangle$ is in Definition 2.

  • Push $(\langle q, \nu \rangle , v) \xrightarrow {push} (\langle q_0({\mathcal {A}}_{i'}), \nu _{\mathbf {0}} \rangle , \langle q, \nu \rangle . v)$. The current working UTA1 (including its control location and clock valuation) is pushed to the stack.

  • Pop $(\langle q, \nu \rangle , \langle q', \nu ' \rangle . w) \xrightarrow {pop} (\langle q', \nu ' \rangle , w)$. The current working UTA1 is replaced with the topmost UTA1 in the stack and the topmost stack frame is removed.

The initial configuration of NeUTA is $(\langle q_0({\mathcal {A}}_0), \nu _\mathbf{0} \rangle , \varepsilon )$, where $\nu _\mathbf{0}(x) = 0$ for $x \in X \cup \{c\}$. We use $\longrightarrow$ to range over these transitions, and $\longrightarrow ^{*}$ is the reflexive and transitive closure of $\longrightarrow$.

5.2 Termination and Boundedness of NeUTAs

In this subsection we present a trivial encoding from NeUTAs to UDTPDA1s and so the termination and boundedness of NeUTAs are decidable.

Let ${\mathcal {N}}=(T,{\mathcal {A}}_0,X,c, \varDelta )$ be a NeUTA. We define a corresponding UDTPDA1 ${\mathcal {E}}({\mathcal {N}})=\langle S, s_0,\varGamma , X, c, \nabla \rangle$, such that

• $S = \varGamma = \bigcup _{{\mathcal {A}}_{i}\in T} S({\mathcal {A}}_{i})$ is the set of all locations of UTA1s in T, with

• $s_0= q_{0}({\mathcal {A}}_{0})$ is the initial location of the initial UTA ${\mathcal {A}}_{0}$ of ${\mathcal {N}}$.

• $X=\{x_1,\ldots , x_k\}$ is the set of k local clocks, and c is the singleton updatable clock.

• $\nabla$ is the union $\bigcup _{{\mathcal {A}}_{i}\in T} \varDelta ({\mathcal {A}}_{i}) \bigcup {\mathcal {H}}({\mathcal {N}}$) where $\left\{ \begin{array}{ll} \varDelta ({\mathcal {A}}_{i}) &{} = \{ \mathbf{Local}, \mathbf{Test}, \mathbf{Assign}, \mathbf{Increment}, \mathbf{Decrement} \}, \\ {\mathcal {H}}({\mathcal {N}}) &{} \text {consists of rules below.} \\ \end{array} \right.$

$$\begin{aligned} \begin{array}{lll} \mathbf{Push } &{} q \xrightarrow {push (q)} {q}_0({{\mathcal {A}}}_{i'}) &{} \hbox { if}\ (q, \varepsilon , push, {q}_0({{\mathcal {A}}}_{i'}), q)\in \varDelta ({\mathcal {N}}) \\ \mathbf{Pop } &{} q \xrightarrow {pop (q')} q' &{} \hbox { if}\ (q, q', pop, q', \varepsilon )) \in \varDelta ({\mathcal {N}}) \\ \end{array} \end{aligned}$$

Definition 18

Let ${\mathcal {N}}$ be a NeUTA $(T,{\mathcal {A}}_0,X, c, \varDelta )$ and let ${\mathcal {E}}({\mathcal {N}})$ be a UDTPDA1 $\langle S, s_0,\varGamma , X, c,\nabla \rangle$. For a configuration $\kappa = (\langle {\mathcal {A}},q,\nu \rangle , v)$ of ${\mathcal {N}}$ such that $v = ({\mathcal {A}}_1, q_1,\nu _1)\ldots ({\mathcal {A}}_n, q_n,\nu _n)$, $\llbracket \kappa \rrbracket$ denotes a configuration $(q,{\overline{w}}(\kappa ),\nu )$ of ${\mathcal {E}}({\mathcal {N}})$ where ${\overline{w}}(\kappa )= w_{1}\cdots w_{n}$ with $w_i=(q_i, \nu _i)$.

Lemma 2

For a NeUTA ${\mathcal {N}}$, a UDTPDA1 ${\mathcal {E}}({\mathcal {N}})$, and configurations $\kappa$, $\kappa '$ of ${\mathcal {N}}$,

• (Preservation) if $\kappa \longrightarrow _{{\mathcal {N}}} \kappa '$, then $\llbracket \kappa \rrbracket \hookrightarrow _{{\mathcal {E}}({\mathcal {N}})}^{*} \llbracket \kappa '\rrbracket$, and

• (Reflection) if $\llbracket \kappa \rrbracket \hookrightarrow _{{\mathcal {N}}}^{*} \varrho$, there exists $\kappa '$ with $\varrho \hookrightarrow _{{\mathcal {E}}({\mathcal {N}})}^{*} \llbracket \kappa '\rrbracket$ and $\kappa \longrightarrow _{{\mathcal {N}}}^{*} \kappa '$.

By this encoding, we have our main result in Theorem 3.

Theorem 3

The termination and boundedness of a NeUTA $(T,{\mathcal {A}}_0, X, c, \varDelta )$ are decidable.

6 Conclusion

This paper investigates termination and boundedness of NeUTAs, which extend NeTAs by replacing TAs with UTA1s. The proof of decidability can be seen as two phases of encoding, first an encoding NeUTAs to UDTPDA1s, then the one from UDTPDA1s to snapshot vector pushdown systems which extends the idea of digitization. Finally, the decidability of termination and boundedness of vector pushdown systems is obtained by the reduced reachability tree technique. The future work includes consider more verification problems of NeUTAs, as well as vector pushdown systems, such as coverability, reachability, and temporal logic model checking [18,19,20,21] et al..