On Timed Scope-bounded Context-sensitive Languages

TL;DR

This paper introduces a new subclass of timed multi-stack automata called k-scope MPA, which ensures stack symbols are popped within a fixed scope, and demonstrates their decidability, closure properties, and logical characterization.

Contribution

It defines and analyzes timed k-scope MPA, establishing their decidability, closure under Boolean operations, and providing a logical framework, advancing the understanding of timed context-sensitive languages.

Findings

Decidable reachability problem for timed k-scope MPA

Closure under Boolean operations

Logical characterization of the automata

Abstract

In (DLT 2016) we studied timed context sensitive languages characterized by multiple stack push down automata (MPA), with an explicit bound on number of stages where in each stage at most one stack is used (k-round MPA). In this paper, we continue our work on timed MPA and study a subclass in which a symbol corresponding to a stack being pushed in it must be popped within fixed number of contexts of that stack---scope-bounded push-down automata with multiple stacks (k-scope MPA). We use Visibly Push-down Alphabet and Event Clocks to show that timed k-scope MPA have decidable reachability problem; are closed under Boolean operations; and have an equivalent logical characterization.

Equations

$$((l,P),a,\phi ,(l^{\prime },P),(\gamma ,\{<\kappa \},-))\in {{\Delta }^i}_c^{\prime }$$

$$((l,P),a,\phi ,(l_{a,<\kappa }^{\prime },P^{\prime }),(\gamma ,\{<\kappa \},\text{first}))\in {{\Delta }^i}_c^{\prime }$$

$$((l_{a,<\kappa }^{\prime },P^{\prime }),{<}_i\kappa ,x_a=0,(l^{\prime },P^{\prime }))\in {{\Delta }^i}_l^{\prime }$$

$$((l,P),a,\phi ,(l_{a,>\kappa }^{\prime },P),(\gamma ,\{>\kappa \},-))\in {{\Delta }^i}_c^{\prime }$$

$$((l,P),a,\phi ,(l_{a,<\kappa ,>\zeta }^{\prime },P^{\prime }),(\gamma ,\{<\kappa ,>\zeta \},\text{first}))\in {{\Delta }^i}_c^{\prime }$$

$$((l_{a,<\kappa ,>\zeta }^{\prime },P^{\prime }),{>}_i\zeta ,x_a=0,(l_{a,<\kappa }^{\prime },P^{\prime }))\in {{\Delta }^i}_l^{\prime }$$

$$((l_{a,<\kappa }^{\prime },P^{\prime }),{>}_i\kappa ,x_a=0,(l_{a,<\kappa }^{\prime },P^{\prime }))\in {{\Delta }^i}_l^{\prime }$$

$$((l,P),a,\phi ,(l_{a,>\zeta }^{\prime },P),(\gamma ,\{<\kappa ,>\zeta \},-))\in {{\Delta }^i}_c^{\prime }$$

$$\phi :=Q_a(x)|x\in X|{\mu }_j(x,y)|{⊲}_a(x)\in I|{⊳}_a(x)\in I|{\theta }_j(x)\in I|\neg \phi |\phi \vee \phi |\exists x.\phi |\exists X.\phi$$

$${{\Sigma }^i}_s^{\prime }={\Sigma }_s^i\times (Val:Z\to \{0,1{\}}^{m+n}),$$

$$X_{{\ell }_i}(x)\wedge X_{{\ell }_j}(y)\wedge Q_a(x)\wedge C_{\gamma }^h(x)\wedge$$

$$\hskip 80.00012pt\bigwedge_{b\in\Sigma^{h}}\Big{(}\big{(}\bigwedge_{(x_{b}\in I)\in\psi}\lhd_{b}{\kern-1.0pt}(x)\in I\big{)}\wedge\big{(}\bigwedge_{(y_{b}\in I)\in\psi}\rhd_{{\kern-2.0pt}b}{\kern-1.0pt}(x)\in I\big{)}\Big{)}.$$

$$X_{{\ell }_i}(x)\wedge X_{{\ell }_j}(y)\wedge Q_a(x)\wedge R_{\gamma }^h(x)\wedge {\theta }^h(x)\in I\wedge$$

$$\hskip 80.00012pt\bigwedge_{b\in\Sigma^{h}}\Big{(}\big{(}\bigwedge_{(x_{b}\in I)\in\psi}\lhd_{b}{\kern-1.0pt}(x){\in}I\big{)}\,{\wedge}\big{(}\bigwedge_{(y_{b}\in I){\in}\psi}\rhd_{{\kern-2.0pt}b}{\kern-1.0pt}(x){\in}I\big{)}\Big{)}.$$

$$X_{\ell_{i}}(x)\wedge X_{\ell_{j}}(y)\wedge Q_{a}(x)\wedge\bigwedge_{b\in\Sigma^{h}}\Big{(}\big{(}\bigwedge_{(x_{b}\in I)\in\psi}\lhd_{b}{\kern-1.0pt}(x)\in I\big{)}\wedge\big{(}\bigwedge_{(y_{b}\in I)\in\psi}\rhd_{{\kern-2.0pt}b}{\kern-1.0pt}(x)\in I\big{)}\Big{)}.$$

$$\forall x\forall y{\mu }_j(x,y)\Rightarrow \underset{\gamma \in {\Gamma }^j\setminus {\perp }_j}{\bigvee }{C}_{\gamma }^j(x)\wedge R_{\gamma }^j(y).$$

Full text

In this paper, we continue our work on timed MPA and study a subclass in which a symbol corresponding to a stack being pushed in it must be popped within fixed number of contexts of that stack —scope-bounded push-down automata with multiple stacks ($k$-scope MPA). We use Visibly Push-down Alphabet and Event Clocks to show that timed $k$-scope MPA have decidable reachability problem; are closed under Boolean operations; and have an equivalent logical characterization.

1 Introduction

The Vardi-Wolper [24] recipe for an automata-theoretic model-checking for a class of languages requires that class to be closed under Boolean operations and have decidable emptiness problem. Esparza, Ganty, and Majumdar [12] coined the term “perfect languages” for the classes of languages satisfying these properties. However, several important extensions of regular languages, such as pushdown automata and timed automata, do not satisfy these requirements. In order to lift the automata-theoretic model-checking framework for these classes of languages, appropriate restrictions have been studied including visibly pushdown automata [6] (VPA) and event-clock automata [5] (ECA). Tang and Ogawa [23] introduced a perfect class of timed context-free languages generalized both visibly pushdown automata and event-clock automata to introduce event-clock visibly pushdown automata (ECVPA).

In this paper we study a previously unexplored class of timed context-sensitive languages inspired by the scope-bounded restriction on multi-stack visibly pushdown languages introduced by La Torre, Napoli, and Parlato [17], and show that it is closed under Boolean operations and has decidable emptiness problem. Moreover, we also present a logical characterization for the proposed subclass.

Visible Stack Operations. Alur and Madhusudan [6] introduced visibly pushdown automata as a specification formalism where the call and return edges are made visible in a structure of the word. This notion is formalized by giving an explicit partition of the alphabet into three disjoint sets of call, return, and internal or local symbols and the visibly pushdown automata must push one symbol to the stack while reading a call symbol, and must pop one symbol (given the stack is non-empty) while reading a return symbol, and must not touch the stack while reading an internal symbol.

Visible Clock Resets. Alur-Dill timed automata [4] is a generalization of finite automata with continuous variables called clocks that grow with uniform rate in each control location and their valuation can be used to guard the transitions. Each transition can also reset clocks, and that allows one to constrain transitions based on the duration since a previous transition has been taken. However, the power of reseting clocks contributed towards timed automata not being closed under complementation. In order to overcome this limitation, Alur, Fix, and Henzinger [5] introduced event-clock automata where input symbol dictate the resets of the clocks. In an event-clock automata every symbol $a$ is implicitly associated with two clocks $x_{a}$ and $y_{a}$, where the “recorder” clock $x_{a}$ records the time since the last occurrence of the symbol $a$, and the “predictor” clock $y_{a}$ predicts the time of the next occurrence of symbol $a$. Hence, event-clock automata do not permit explicit reset of clocks and it is implicitly governed by the input timed word.

Visible Stack Operations and Clock Resets in Multistack Setting. We study dense-time event-clock multistack visibly pushdown automata (dt-ECMVPA) that combines event-clock dynamics of event-clock automata with multiple visibly pushdown stacks. We assume a partition of the alphabet among various stacks, and partition of the alphabet of each stack into call, return, and internal symbols. Moreover, we associate recorder and predictor clocks with each symbol. Inspired by Atig et al. [1] we consider our stacks to be dense-timed, i.e. we allow stack symbols to remember the time elapsed since they were pushed to the stack.

A finite timed word over an alphabet $\Sigma$ is a sequence $(a_{1},t_{1}),\ldots,(a_{n},t_{n})\in(\Sigma{\times}{\mathbb{R}}_{\geq 0})^{*}$ such that $t_{i}\leq t_{i+1}$ for all $1\leq i\leq n-1$. Alternatively, we can represent timed words as tuple $(\langle a_{1},\ldots,a_{n}\rangle,\langle t_{1},\ldots,t_{n}\rangle)$. We may use both of these formats depending on the context and for technical convenience. Let $T\Sigma^{*}$ denote the set of finite timed words over $\Sigma$.

We briefly discuss the concepts of rounds and scope as introduced by [17]. Consider an pushdown automata with $n$ stacks. We say that for a stack $h$, a (timed) word is a stack-$h$ context if all of its symbols belong to the alphabet of stack $h$. A round is fixed sequence of exactly $n$ contexts one for each stack. Given a timed word, it can be partitioned into sequences of contexts of various stacks. The word is called $k$-round if it can be partitioned into $k$ rounds. We say that a timed word is $k$-scoped if for each return symbol of a stack its matching call symbol occurs within the last $k$ contexts of that stack. A visibly-pushdown multistack event-clock automata is scope-bounded if all of the accepting words are $k$-scoped for a fixed $k\in\mathbb{N}$.

To introduce some of the key ideas of our model, let us consider the following example.

Example 1

Consider the timed language whose untimed component is of the form

${L=\{\hat{a}a^{x}b^{y}d^{y}c^{l}a^{l}b^{z}c^{x}\hat{c}d^{z}\mid x,l,z\geq 1,~{}y\geq 2\}}$ with the critical timing restrictions among various symbols in the following manner. The time delay between the first occurrence of $b$ and the last occurrence of $d$ in the substring $b^{y}d^{y}$ is at least $4$ time-units. The time-delay between this last occurrence of $d$ and the next occcurence of $b$ is at most $2$ time-units. Finally the last $d$ of the input string must appear within $2$ time units of the last $b$, and $\hat{c}$ must occur within $5$ time units of corresponding $\hat{a}$. This language is accepted by a dt-ECMVPA with two stacks shown in Figure 1. We annotate a transition with the symbol and corresponding stack operations if any. We write $pop^{i}$ or $push^{i}$ to emphasize pushes and pops to the $i$-th stack. We also use $pop^{i}(X)\in I$ to check if the age of the popped symbol $X$ belongs to the interval $I$. In addition, we use simple constraints on predictor/recorder clock variables corresponding to the symbols. Let $a,\hat{a}$ and $c,\hat{c}$ ($b$ and $d$, resp.) be call and return symbols for the first (second, resp.) stack. The Stack alphabet for the first stack is \Gamma^{1}=\{\alpha,\}$and for the second stack is$\Gamma^{2}={$}. In Figure [1](#S1.F1) clock x_{a}$measures the time since the occurrence of the last$a$, while constraints$pop(\gamma)\in I$checks if the age of the popped symbol$\gamma$is in a given interval$I$. This language is$3$-scoped and is accepted by a$6$-round dt-ECMVPA. But if we consider the Kleene star of this language, it will be still$3$-scoped. and its machine can be built by fusing states$l_{0}$and$l_{10}$ of the MVPA in Figure 1.

Related Work. The formalisms of timed automata and pushdown stack have been combined before. First such attempt was timed pushdown automata [9] by Bouajjani, et al and was proposed as a timed extension of pushdown automata which uses global clocks and timeless stack. We follow the dense-timed pushdown automata by Abdulla et al [1]. The reachability checking of a given location from an intial one was shown to be decidable for this model. Trivedi and Wojtczak [21] studied the recursive timed automata in which clock values can be pushed onto a stack using mechanisms like pass-by-value and pass-by-reference. They studied reachability and termination problems for this model. Nested timed automata (NeTA) proposed by Li, et al [19] is a relatively recent model which, an instance of timed automata itself can be pushed on the stack along with the clocks. The clocks of pushed timed automata progress uniformly while on the stack. From the perspective of logical characterization, timed matching logic, an existential fragment of second-order logic, identified by Droste and Perevoshchikov [11] characterizes dense-timed pushdown automata. We earlier [7] studied MSO logic for dense-timed visibly pushdown automata which form a subclass of timed context-free languages. This subclass is closed under union, intersection, complementation and determinization. The work presented in this paper extends the results from [8] for bounded-round dt-ECMVPA to the case of bounded-scope dt-ECMVPA.

Contributions. We study bounded-scope dt-ECMVPA and show that they are closed under Boolean operations and the emptiness problem for these models is decidable. We also present a logical characterization for these models.

Organization of the paper: In the next section we recall the definitions of event clock and visibly pushdown automata. In Section 3 we define $k$-scope dense time multiple stack visibly push down automata with event clocks and its properties. In the following section these properties are used to decide emptiness checking and determinizability of $k$-scope ECMVPA with event clocks. Building upon these results, we show decidability of these properties for $k$-scope dt-ECMVPA with event clocks. In Section 6 we give a logical characterization for models introduced.

2 Preliminaries

We only give a very brief introduction of required concepts in this section, and for a detailed background on these concepts we refer the reader to [3, 5, 6]. We assume that the reader is comfortable with standard concepts such as context-free languages, pushdown automata, MSO logic from automata theory; and clocks, event clocks, clock constraints, and valuations from timed automata. Before we introduce our model, we revisit the definitions of event-clock automata.

2.1 Event-Clock Automata

The general class of TA [3] are not closed under Boolean operations. An important class of TA which is determinizable is Event-clock automata (ECA) [5], and hence closed under Boolean operations. Here the determinizability is achieved by making clock resets “visible”.

To make clock resets visible we have two clocks which are associated with every action $a\in\Sigma$ : $x_{a}$ the “recorder” clock which records the time of the last occurrence of action $a$, and $y_{a}$ the “predictor” clock which predicts the time of the next occurrence of action $a$. For example, for a timed word $w=(a_{1},t_{1}),(a_{2},t_{2}),\dots,(a_{n},t_{n})$, the value of the event clock $x_{a}$ at position $j$ is $t_{j}-t_{i}$ where $i$ is the largest position preceding $j$ where an action $a$ occurred. If no $a$ has occurred before the $j$th position, then the value of $x_{a}$ is undefined denoted by a special symbol $\vdash$. Similarly, the value of $y_{a}$ at position $j$ of $w$ is undefined if symbol $a$ does not occur in $w$ after the $j$th position. Otherwise, it is $t_{k}-t_{j}$ where $k$ is the first occurrence of $a$ after $j$.

Hence, event-clock automata do not permit explicit reset of clocks and it is implicitly governed by the input timed word which makes them determinizable and closed under all Boolean operations.

We write $C$ for the set of all event clocks and we use ${\mathbb{R}}_{>0}^{\vdash}$ for the set ${\mathbb{R}}_{>0}\cup\{\vdash\}$. Formally, the clock valuation after reading $j$-th prefix of the input timed word $w$, $\nu_{j}^{w}:C\mapsto{\mathbb{R}}_{>0}^{\vdash}$, is defined as follows: $\nu_{j}^{w}(x_{q})=t_{j}{-}t_{i}$ if there exists an $0{\leq}i{<}j$ such that $a_{i}=q$ and $a_{k}\not=q$ for all $i{<}k{<}j$, otherwise $\nu_{j}^{w}(x_{q})=\ \vdash$ (undefined). Similarly, $\nu_{j}^{w}(y_{q})=t_{m}-t_{j}$ if there is $j{<}m$ such that $a_{m}=q$ and $a_{l}\not=q$ for all $j{<}l{<}m$, otherwise $\nu_{j}^{w}(y_{q})=\vdash$.

A clock constraint over $C$ is a boolean combination of constraints of the form $z\sim c$ where $z\in C$, $c\in\mathbb{N}$ and $\sim\in\{\leq,\geq\}$. Given a clock constraint $z\sim c$ over $C$, we write $\nu_{i}^{w}\models(z\sim c)$ to denote if $\nu_{j}^{w}(z)\sim c$. For any boolean combination $\varphi$, $\nu_{i}^{w}\models\varphi$ is defined in an obvious way: if $\varphi=\varphi_{1}\wedge\varphi_{2}$, then $\nu_{i}^{w}\models\varphi$ iff $\nu_{i}^{w}\models\varphi_{1}$ and $\nu_{i}^{w}\models\varphi_{2}$. Likewise, the other Boolean combinations are defined.

Let $\Phi(C)$ define all the clock constraints defined over $C$.

Definition 1

An event clock automaton is a tuple $A=(L,\Sigma,L^{0},F,E)$ where $L$ is a set of finite locations, $\Sigma$ is a finite alphabet, $L^{0}\in L$ is the set of initial locations, $F\in L$ is the set of final locations, and $E$ is a finite set of edges of the form $(\ell,\ell^{\prime},a,\varphi)$ where $\ell,\ell^{\prime}$ are locations, $a\in\Sigma$, and $\varphi$ in $\Phi(C)$.

The class of languages accepted by ECA have Boolean closure and decidable emptiness [5].

2.2 Visibly Pushdown Automata

The class of push down automata are not determinzable and also not closed under Boolean operations [15]. The determinizability is achieved by making input alphabet “visible” that is for a given input letter only one kind of stack operations is allowed giving an important subclass of Visibly pushdown automata [6] which operate over words that dictate the stack operations. This notion is formalized by giving an explicit partition of the alphabet. This notion is formalized by giving an explicit partition of the alphabet into three disjoint sets of call, return, and internal symbols and the visibly pushdown automata must push one symbol to stack while reading a call symbol, and must pop one symbol (given stack is non-empty) while reading a return symbol, and must not touch the stack while reading the internal symbol.

Definition 2

A visibly pushdown alphabet is a tuple $\langle\Sigma_{c},\Sigma_{r},\Sigma_{l}\rangle$ where $\Sigma_{c}$ is call alphabet, $\Sigma_{r}$ is a return alphabet, and $\Sigma_{l}$ is internal alphabet.

A visibly pushdown automata(VPA) over $\Sigma=\langle\Sigma_{c},\Sigma_{r},\Sigma_{l}\rangle$ is a tuple $(L,\Sigma,\Gamma,L^{0},\delta,F)$ where $L$ is a finite set of locations including a set $L^{0}\subseteq L$ of initial locations, $\Gamma$ is a finite stack alphabet with special end-of-stack symbol $\bot$, $\Delta\subseteq(L{\times}\Sigma_{c}{\times}L{\times}(\Gamma{\setminus}{\bot}))\cup(L{\times}\Sigma_{r}{\times}\Gamma{\times}L)\cup(L{\times}\Sigma_{l}{\times}L)$ is the transition relation, and $F\subseteq L$ is final locations.

Alur and Madhusudan [6] showed that VPAs are determinizable and closed under boolean operations. A language $L$ of finite words defined over visibly pushdown alphabet $\Sigma$ is a visibly pushdown language(VPL) if there exist a VPA $M$ such that $L(M)=L$. The class of languages accepted by visibly pushdown automata are closed under boolean operations with decidable emptiness property [6].

3 Dense-Time Visibly Pushdown Multistack Automata

This section introduces scope-bounded dense-timed multistack visibly pushdown automata and give some properties about words and languages accepted by these machines.

Let $\Sigma=\langle\Sigma^{h}_{c},\Sigma^{h}_{r},\Sigma^{h}_{l}\rangle_{h=1}^{n}$ where $\Sigma^{i}_{x}\cap\Sigma^{j}_{x}=\emptyset$ whenever either $i\neq j$ or $x\neq y$, and $x,y\in\{c,r,l\}$. Let $\Sigma^{h}=\langle\Sigma^{h}_{c},\Sigma^{h}_{r},\Sigma^{h}_{l}\rangle$. Let $\Gamma^{h}$ be the stack alphabet of the $h$-th stack and $\Gamma=\bigcup_{h=1}^{n}\Gamma^{h}$. For notational convenience, we assume that each symbol $a\in\Sigma^{h}$ has an unique recorder $x_{a}$ and predictor $y_{a}$ clock assigned to it. Let $C_{h}$ denote the set of event clocks corresponding to stack $h$ and $\Phi(C_{h})$ denote the set of clock constraints defined over $C_{h}$. Let $cmax$ be the maximum constant used in the clock constraints $\Phi(C^{h})$ of all stacks. Let $\mathcal{I}$ denote the finite set of intervals $\{[0,0],(0,1),[1,1],(1,2),\ldots,[cmax,cmax],(cmax,\infty)\}$.

Definition 3 ([8])

A dense-timed visibly pushdown multistack automata (dt-ECMVPA) over $\langle\Sigma^{h}_{c},\Sigma^{h}_{r},\Sigma^{h}_{l}\rangle_{h=1}^{n}$ is a tuple $(L,\Sigma,\Gamma,L^{0},F,\Delta{=}(\Delta^{h}_{c}{\cup}\Delta^{h}_{r}{\cup}\Delta^{h}_{l})_{h=1}^{n})$ where

• •

$L$ is a finite set of locations including a set $L^{0}\subseteq L$ of initial locations,

• •

$\Gamma^{h}$ is the finite alphabet of stack $h$ and has special end-of-stack symbol $\bot_{h}$,

• •

$\Delta^{h}_{c}\subseteq(L{\times}\Sigma^{h}_{c}{\times}\Phi(C_{h}){\times}L{\times}(\Gamma^{h}{\setminus}\{\bot_{h}\}))$ is the set of call transitions,

• •

$\Delta^{h}_{r}\subseteq(L{\times}\Sigma^{h}_{r}{\times}\mathcal{I}{\times}\Gamma^{h}{\times}\Phi(C_{h}){\times}L)$ is set of return transitions,

• •

$\Delta^{h}_{l}\subseteq(L{\times}\Sigma^{h}_{l}{\times}\Phi(C_{h}){\times}L)$ is set of internal transitions, and

• •

$F{\subseteq}L$ is the set of final locations.

Let $w=(a_{0},t_{0}),\dots,(a_{e},t_{e})$ be a timed word. A configuration of the dt-ECMVPA is a tuple $(\ell,\nu_{i}^{w},(((\gamma^{1}\sigma^{1},age(\gamma^{1}\sigma^{1})),\dots,(\gamma^{n}\sigma^{n},age(\gamma^{n}\sigma^{n})))$ where $\ell$ is the current location of the dt-ECMVPA, function $\nu_{i}^{w}$ gives the valuation of all the event clocks at position $i\leq|w|$, $\gamma^{h}\sigma^{h}\in\Gamma^{h}(\Gamma^{h})^{*}$ is the content of stack $h$ with $\gamma^{h}$ being the topmost symbol, and $\sigma^{h}$ the string representing stack contents below $\gamma^{h}$, while $age(\gamma^{h}\sigma^{h})$ is a sequence of real numbers denoting the ages (the time elapsed since a stack symbol was pushed on to the stack) of all the stack symbols in $\gamma^{h}\sigma^{h}$. We follow the assumption that $age(\bot^{h})=\langle\vdash\rangle$ (undefined). If for some string $\sigma^{h}\in(\Gamma^{h})^{*}$ we have $age(\sigma^{h})=\langle t_{1},t_{2},\ldots,t_{g}\rangle$ and for $\tau\in{\mathbb{R}}_{\geq 0}$ then we write $age(\sigma^{h})+\tau$ for the sequence $\langle t_{1}+\tau,t_{2}+\tau,\ldots,t_{g}+\tau\rangle$. For a sequence $\sigma^{h}=\langle\gamma^{h}_{1},\ldots,\gamma^{h}_{g}\rangle$ and a stack symbol $\gamma^{h}$ we write $\gamma^{h}::\sigma^{h}$ for $\langle\gamma^{h},\gamma^{h}_{1},\ldots,\gamma^{h}_{g}\rangle$.

A run of a dt-ECMVPA on a timed word $w=(a_{0},t_{0}),\dots,(a_{e},t_{e})$ is a sequence of configurations:

$(\ell_{0},\nu^{w}_{0},(\langle\bot^{1}\rangle,\langle\vdash\rangle),\dots,(\langle\bot^{n}\rangle,\langle\vdash\rangle))$, $(\ell_{1},\nu^{w}_{1},((\sigma^{1}_{1},age(\sigma^{1}_{1})),\dots,(\sigma^{n}_{1},age(\sigma^{n}_{1}))))$,

$\dots,(\ell_{e+1},\nu^{w}_{e+1},(\sigma^{1}_{e+1},age(\sigma^{1}_{e+1})),\dots,(\sigma^{n}_{e+1},age(\sigma^{n}_{e+1})))$ where $\ell_{i}\in L$, $\ell_{0}\in L^{0}$, $\sigma^{h}_{i}\in(\Gamma^{h})^{*}\bot^{h}$, and for each $i,~{}0\leq i\leq e$, we have:

• •

If $a_{i}\in\Sigma^{h}_{c}$, then there is $(\ell_{i},a_{i},\varphi,\ell_{i+1},\gamma^{h}){\in}\Delta^{h}_{c}$ such that $\nu_{i}^{w}\models\varphi$. The symbol $\gamma^{h}\in\Gamma^{h}\backslash\{\bot^{h}\}$ is then pushed onto the stack $h$, and its age is initialized to zero, i.e. $(\sigma^{h}_{i+1},age(\sigma^{h}_{i+1}))=(\gamma^{h}::\sigma^{h}_{i},0::(age(\sigma^{h}_{i})+(t_{i}-t_{i-1})))$. All symbols in all other stacks are unchanged, and they age by $t_{i}-t_{i-1}$.

• •

If $a_{i}\in\Sigma^{h}_{r}$, then there is $(\ell_{i},a_{i},I,\gamma^{h},\varphi,\ell_{i+1})\in\Delta^{h}_{r}$ such that $\nu_{i}^{w}\models\varphi$. Also, $\sigma^{h}_{i}=\gamma^{h}::\kappa\in\Gamma^{h}(\Gamma^{h})^{*}$ and $age(\gamma^{h})+(t_{i}-t_{i-1})\in I$. The symbol $\gamma^{h}$ is popped from stack $h$ obtaining $\sigma^{h}_{i+1}=\kappa$ and ages of remaining stack symbols are updated i.e., $age(\sigma^{h}_{i+1})=age(\kappa)+(t_{i}-t_{i-1})$. However, if $\gamma^{h}=\langle\bot^{h}\rangle$, then $\gamma^{h}$ is not popped. The contents of all other stacks remains unchanged, and simply age by $(t_{i}-t_{i-1})$.

• •

If $a_{i}{\in}\Sigma^{h}_{l}$, then there is $(\ell_{i},a_{i},\varphi,\ell_{i+1}){\in}\Delta^{h}_{l}$ such that $\nu_{i}^{w}\vDash\varphi$. In this case all stacks remain unchanged i.e. $\sigma^{h}_{i+1}{=}\sigma^{h}_{i}$, but their contents age by $t_{i}-t_{i-1}$ i.e. $age(\sigma^{h}_{i+1}){=}age(\sigma^{h}_{i})+(t_{i}-t_{i-1})$ for all $1\leq h\leq n$.

A run $\rho$ of a dt-ECMVPA $M$ is accepting if it terminates in a final location. A timed word $w$ is an accepting word if there is an accepting run of $M$ on $w$. The language $L(M)$ of a dt-ECMVPA $M$, is the set of all timed words $w$ accepted by $M$ and is called dt-ECMVPL.

A dt-ECMVPA $M=(L,\Sigma,\Gamma,L^{0},F,\Delta)$ is said to be deterministic if it has exactly one start location, and for every configuration and input action exactly one transition is enabled. Formally, we have the following conditions:

for any two moves $(\ell,a,\phi_{1},\ell^{\prime},\gamma_{1})$ and $(\ell,a,\phi_{2},\ell^{\prime\prime},\gamma_{2})$ of $\Delta^{h}_{c}$, condition $\phi_{1}\wedge\phi_{2}$ is unsatisfiable; for any two moves $(\ell,a,I_{1},\gamma,\phi_{1},\ell^{\prime})$ and $(\ell,a,I_{2},\gamma,\phi_{2},\ell^{\prime\prime})$ in $\Delta^{h}_{r}$, either $\phi_{1}\wedge\phi_{2}$ is unsatisfiable or $I_{1}\cap I_{2}=\emptyset$; and for any two moves $(\ell,a,\phi_{1},\ell^{\prime})$ and $(\ell,a,\phi_{2},\ell^{\prime})$ in $\Delta^{h}_{l}$, condition $\phi_{1}\wedge\phi_{2}$ is unsatisfiable.

An Event clock multi stack visibly push down automata (ECMVPA) is a dt-ECMVPA where the stacks are untimed i.e., a dt-ECMVPA $(L,\Sigma,\Gamma,L^{0},F,\Delta)$, with $I=[0,+\infty]$ for every $(\ell,a,I,\gamma,\phi,\ell^{\prime}){\in}\Delta^{h}_{r}$, is an ECMVPA.

A dtECVPA is a dt-ECMVPA restricted to single stack.

We now define a matching relation $\sim_{h}$ on the positions of input timed word $w$ which identifies matching call and return positions for each stack $h$. Note that this is possible because of the visibility of the input symbols.

Definition 4 (Matching relation)

Consider a timed word $w$ over $\Sigma$. Let $\mathcal{P}^{h}_{c}$ (resp. $\mathcal{P}^{h}_{r}$) denote the set of positions in $w$ where a symbol from $\Sigma^{h}_{c}$ i.e. a call symbol (resp. $\Sigma^{h}_{r}$ i.e. a return symbol ) occurs. Position i (resp. j) is called call position (resp. return position). For each stack $h$ the timed word $w$, defines a matching relation $\sim_{h}\subseteq\mathcal{P}^{h}_{c}\times\mathcal{P}^{h}_{r}$ satisfying the following conditions:

for all positions $i,j$ with $i\sim_{h}j$ we have $i<j$, 2. 2.

for any call position $i$ of $\mathcal{P}^{h}_{c}$ and any return position $j$ of $\mathcal{P}^{h}_{r}$ with $i<j$, there exists $l$ with $i\leq l\leq j$ for which either $i\sim_{h}l$ or $l\sim_{h}j$, 3. 3.

for each call position $i\in\mathcal{P}^{h}_{c}$ (resp. $i\in\mathcal{P}^{h}_{r}$) there is at most one return position $j\in\mathcal{P}^{h}_{r}$ (resp. $j\in\mathcal{P}^{h}_{c}$) with $i\sim_{h}j$ (resp. $j\sim_{h}i$).

For $i\sim_{h}j$, position $i$ (resp. $j$) is called matching call (resp. matching return).

This definition of matching relation extends that defined by La Torre, et al [18] to timed words. As matching relation is completely determined by stacks and timestamps of the input word does not play any role, we claim that above definition uniquely identifies matching relation for a given input word $w$ using uniqueness proof from [18].

Fix a $k$ from $\mathbb{N}$. A stack-$h$ context is a word in $\Sigma^{h}(\Sigma^{h})^{*}$. Given a word $w$ and a stack $h$, the word $w$ has $k$ maximal $h$-contexts if $w\in(\Sigma^{h})^{*}((\bigcup_{h\neq h^{\prime}}\Sigma^{h^{\prime}})^{*}(\Sigma^{h})^{*})^{k-1}$. A timed word over $\Sigma$ is $k$-scoped if for each matching call of stack $h$, its corresponding return occurs within at most $k$ maximal stack-$h$ contexts.

Let $Scope(\Sigma,k)$ denote the set of all $k$-scope timed words over $\Sigma$. For any fixed $k$, a $k$-scope dt-ECMVPA over $\Sigma$ is a tuple $A=(k,M)$ where $M=(L,\Sigma,\Gamma,L^{0},F,\Delta)$ is a dt-ECMVPA over $\Sigma$. The language accepted by $A$ is $L(A)=L(M)\cap Scope(\Sigma,k)$ and is called $k$-scope dense-timed multistack visibly pushdown language ($k$-scoped-dt-ECMVPL). We define $k$-scoped-ECMVPL in a similar fashion.

We now recall some key definitions from La Torre [17, 18] which help us extend the notion of scoped words from untimed to timed words.

Definition 5 ($k$-scoped splitting [17, 18])

A cut of $w$ is $w_{1}{:}w_{2}$ where $w=w_{1}w_{2}$. The cutting of $w$ is marked by “:”. A cut is $h$-consistent with matching relation $\sim_{h}$ if no call occuring in $w_{1}$ matches with a return in $w_{2}$ in $\sim_{h}$.

A splitting of $w$ is a set of cuts $w_{1}\ldots w_{i}:w_{i+1}\ldots w_{m}$ such that $w=w_{1}\ldots w_{i}w_{i+1}\ldots w_{m}$ for each $i$ in $\{1,\ldots,m-1\}$. An h-consistent splitting of $w$ is the one in which each specified cut is $h$-consistent. A context-splitting of word $w$ is a splitting $w_{1}:w_{2}:\ldots:w_{m}$ such that each $w_{i}$ is an $h$-context for some stack $h$ and $i\in\{1,\ldots,m\}$. A canonical context-splitting of word is a context-splitting of $w$ in which no two consecutive contexts belong to the same stack.

Given a context-splitting of timed word $w$, we obtain its $h$-projection by removing all non stack-$h$ contexts. See that an $h$-projection is a context-splitting. An ordered tuple of $m$ $h$-contexts is $k$-bounded if there there exists a $h$-consistent splitting of this tuple, where each component of the cut in the splitting is a concatenation of at most $k$ consecutive $h$-contexts of given tuple. A $k$-scoped splitting of word $w$ is the canonical splitting of $w$ equipped with additional cuts for each stack $h$ such that, if we take $h$-projection of $w$ with these cuts it is $k$-bounded.

The main purpose for introducing all the above definitions is to come up with a scheme which will permit us to split any arbitrary length input timed word into $k$-scoped words. Using [17, 18] for untimed words we get the following Lemma.

Lemma 1

A timed word $w$ is $k$-scoped iff there is a $k$-scoped splitting of $w$.

Next we describe the notion of switching vectors for timed words [7], which are used in determinization of $k$-scope dt-ECMVPA.

3.1 Switching vectors

Let $A$ be $k$-scoped dt-ECMVPA over $\Sigma$ and let $w$ be a timed word accepted by $A$. Our aim is to simulate $A$ on $w$ by $n$ different dtECVPAs, $A^{h}$ for each stack-$h$ inputs. We insert a special symbol $\#$ at the end of each maximal context, to obtain word $w^{\prime}$ over $\Sigma\cup\{\#,\#^{\prime}\}$. We also have recorder clocks $x_{\#}$ and predictor clocks $y_{\#}$ for symbol $\#$. For $h$-th stack, let dtECVPA $A^{h}$ be the restricted version of $A$ over alphabet $\Sigma\cup\{\#,\#^{\prime}\}$ which simulates $A$ on input symbols from $\Sigma^{h}$. Then, it is clear that at the symbol before $\#$, stack $h$ may be touched by dt-ECMVPA $A$ and at the first symbol after $\#$, stack $h$ may be touched again. But it may be the case that at positions where $\#$ occurs stack $h$ may not be empty i.e., cut defined position of # may be not be $h$-consistent.

To capture the behaviour of $A^{h}$ over timed word $w$ we have a notion of switching vector. Let $m$ be the number of maximal $h$-contexts in word $w$ and $w^{h}$ be the $h$-projection of $w$ i.e., $w^{h}=u^{h}_{1}\ldots u^{h}_{m}$. In particular, $m$ could be more than $k$. A switching vector $\mathbb{V}^{h}$ of $A$ for word $w$ is an element of $(L,\mathcal{I},L)^{m}$, where $\mathbb{V}^{h}[l]=(q,I_{l},q^{\prime})$ if in the run of $A$ over $w^{h}$ we have $q\xrightarrow{u^{h}_{l}}q^{\prime}$.

Let $w^{\prime h}=u^{h}_{1}\#u^{h}_{2}\#\ldots u^{h}_{m}\#$, where $u^{h}_{i}=(a^{h}_{i1},t^{h}_{i1}),(a^{h}_{i2},t^{h}_{i2})\ldots(a^{h}_{i,s_{i}},t^{h}_{i,s_{i}})$ is a stack-$h$ context, where $s_{i}=|u^{h}_{i}|$. Now we assign time stamps of the last letter read in the previous contexts to the current symbol $\#$ to get the word $\kappa^{h}=u^{h}_{1}(\#,t^{h}_{1,s_{1}})u^{h}_{2}(\#,t^{h}_{2,s_{2}})\ldots u^{h}_{m}(\#,t^{h}_{m,s_{m}})$.

We take the word $w^{\prime h}$ and looking at this word we construct another word $\bar{w}^{h}$ by inserting symbols $\#^{\prime}$ at places where the stack is empty after popping some symbol, and if $\#^{\prime}$ is immediately followed by $\#$ then we drop $\#$ symbol. We do this in a very canonical way as follows: In this word $w^{\prime h}$ look at the first call position $c_{1}$ and its corresponding return position $r_{1}$. Then we insert $\#^{\prime}$ after position $r_{1}$ in $w^{h}$. Now we look for next call position $c_{2}$ and its corresponding return position $r_{2}$ and insert symbol $\#^{\prime}$ after $r_{2}$. We repeat this construction for all call and its corresponding return positions in $w^{\prime h}$ to get a timed word $\bar{w}^{h}$ over $\Sigma\cup\{\#,\#^{\prime}\}$. Let $\bar{w}^{h}=\bar{u}^{h}_{1}\widehat{\#}\bar{u}^{h}_{2}\widehat{\#}\ldots\widehat{\#}\bar{u}^{h}_{z}$, where $\widehat{\#}$ is either $\#$ or $\#^{\prime}$, and $\bar{u}^{h}_{i}=(\bar{a}^{h}_{i1},\bar{t}^{h}_{i1}),(\bar{a}^{h}_{i2},\bar{t}^{h}_{i2})\ldots(\bar{a}^{h}_{i,s_{i}},\bar{t}^{h}_{i,s_{i}})$, is a timed word.

The restriction of $A$ which reads $\bar{w}^{h}$ is denoted by $A^{h}_{k}$. Assign timestamps of the last letter read in the previous contexts to the current symbol $\hat{\#}$ to get the word $\bar{\kappa}^{h}=\bar{u}^{h}_{1}(\hat{\#},\bar{t}^{h}_{1,s_{1}})\bar{u}^{h}_{2}(\hat{\#},\bar{t}^{h}_{2,s_{2}})\ldots\bar{u}^{h}_{z}(\hat{\#},\bar{t}^{h}_{z,s_{z}})$, where $s_{i}=|\bar{u}^{h}_{i}|$ for $i$ in $\{1,\ldots,z\}$.

A stack-$h$ switching vector $\bar{\mathbb{V}}^{h}$ is a $z$-tuple of the form $(L,\mathcal{I},L)^{z}$, where $z>0$ and for every $j\leq z$ if $\bar{\mathbb{V}}^{h}[j]=(q_{j},I_{j},q^{\prime}_{j})$ then there is a run of $A^{h}$ from location $q_{j}$ to $q^{\prime}_{j}$.

By definition of $k$-scoped word we are guaranteed to find maximum $k$ number of $\#$ symbols from $c_{j}$ to $r_{j}$. And we also know that stack-$h$ is empty whenever we encounter $\#^{\prime}$ in the word. In other words, if we look at the switching vector $\bar{\mathbb{V}}^{h}$ of $A$ reading $\bar{w}^{h}$, it can be seen as a product of switching vectors of $A$ each having a length less than $k$. Therefore, $\bar{\mathbb{V}}^{h}=\displaystyle\Pi_{i=1}^{r}V^{h}_{i}$ where $r\leq z$ and $V^{h}_{i}=(L\times\mathcal{I}\times L)^{\leq k}$. When we look at a timed word and refer to the switching vector corresponding to it, we view it as tuples of switching pairs, but when we look at the switching vectors as a part of state of $A^{h}_{k}$ then we see at a product of switching vectors of length less than $k$.

A correct sequence of context switches for $A^{h}_{k}$ wrt $\bar{\kappa}^{h}$ is a sequence of pairs $\bar{\mathbb{V}}^{h}=P^{h}_{1}P^{h}_{2}\dots P^{h}_{z}$, where $P^{h}_{i}=(\ell^{h}_{i},I^{h}_{i},\ell^{\prime h}_{i})$, $2\leq h\leq n$, $P^{h}_{1}=(\ell^{h}_{1},\nu^{h}_{1},\ell^{\prime h}_{1})$ and $I^{h}_{i}\in\mathcal{I}$ such that

Starting in $\ell^{h}_{1}$, with the $h$-th stack containing $\bot^{h}$, and an initial valuation $\nu^{h}_{1}$ of all recorders and predictors of $\Sigma^{h}$, the dt-ECMVPA $A$ processes $u^{h}_{1}$ and reaches some $\ell^{\prime h}_{1}$ with stack content $\sigma^{h}_{2}$ and clock valuation $\nu^{\prime h}_{1}$. The processing of $u^{h}_{2}$ by $A$ then starts at location $\ell^{h}_{2}$, and a time $t\in I^{h}_{2}$ has elapsed between the processing of $u^{h}_{1}$ and $u^{h}_{2}$. Thus, $A$ starts processing $u^{h}_{2}$ in $(\ell^{h}_{2},\nu^{h}_{2})$ where $\nu^{h}_{2}$ is the valuation of all recorders and predictors updated from $\nu^{\prime h}_{1}$ with respect to $t$. The stack content remains same as $\sigma^{h}_{2}$ when the processing of $u^{h}_{2}$ begins. 2. 2.

In general, starting in $(\ell^{h}_{i},\nu^{h}_{i})$, $i>1$ with the $h$-th stack containing $\sigma^{h}_{i}$, and $\nu^{h}_{i}$ obtained from $\nu^{h}_{i-1}$ by updating all recorders and predictors based on the time interval $I^{h}_{i}$ that records the time elapse between processing $u^{h}_{i-1}$ and $u^{h}_{i}$, $A$ processes $u^{h}_{i}$ and reaches $(\ell^{\prime h}_{i},\nu^{\prime h}_{i})$ with stack content $\sigma^{h}_{i+1}$. The processing of $u^{h}_{i+1}$ starts after time $t\in I^{h}_{i+1}$ has elapsed since processing $u^{h}_{i}$ in a location $\ell^{h}_{i+1}$, and stack content being $\sigma^{h}_{i}$.

These switching vectors were used in to get the determinizability of $k$-round dt-ECMVPA [7] In a $k$-round dt-ECMVPA, we know that there at most $k$-contexts of stack-$h$ and hence the length of switching vector (whichever it is) is at most $k$ for any given word $w$. See for example the MVPA corresponding to Kleene star of language given in the Example 1. In $k$-scope MVPA for a given $w$, we do not know beforehand what is the length of switching vector. So we employ not just one switching vector but many one after another for given word $w$, and we maintain that length of each switching vector is at most $k$. This is possible because of the definition of $k$-scope dt-ECMVPA and Lemma 1.

Lemma 2

*(Switching Lemma for $A^{h}_{k}$)

Let $A=(k,L,\Sigma,\Gamma,L^{0},F,\Delta)$ be a $k$-scope-dt-ECMVPA. Let $w$ be a timed word with $m$ maximal $h$-contexts and accepted by $A$ . Then we can construct a dtECVPA $A^{h}_{k}$ over $\Sigma^{h}\cup\{\#,\#^{\prime}\}$ such that $A^{h}_{k}$ has a run over $\bar{w}^{h}$ witnessed by a switching sequence $\bar{\mathbb{V}}^{h}=\displaystyle\Pi_{i=1}^{r}\bar{\mathbb{V}}^{h}_{i}$ where $r\leq z$ and $\bar{\mathbb{V}}^{h}_{i}=(L\times\mathcal{I}\times L)^{\leq k}$ which ends in the last component $\bar{\mathbb{V}}^{h}_{r}$ of $\bar{\mathbb{V}}^{h}$  iff there exists a $k$-scoped switching sequence $\bar{\mathbb{V}}^{\prime h}$ of switching vectors of $A$ such that for any $v^{\prime}$ of $\bar{\mathbb{V}}^{\prime h}$ there exist $v_{i}$ and $v_{j}$ in $\bar{\mathbb{V}}^{\prime}$ with $i\leq j$ and $v^{\prime}[1]=v_{i}[1]$ and $v^{\prime}[|v^{\prime}|]=v_{j}[|v_{j}|]$.*

Proof

We construct a dtECVPA $A^{k}_{h}=(L^{h},\Sigma\cup\{\#,\#^{\prime}\},\Gamma^{h},L^{0},F^{h}=F,\Delta^{h})$ where, $L^{h}\subseteq(L\times\mathcal{I}\times L)^{\leq k}\times\Sigma\cup\{\#,\#^{\prime}\}$ and $\Delta^{h}$ are given below.

For $a$ in $\Sigma$:

$(P^{h}_{1},\ldots,P^{h}_{i}=(q,I^{h}_{i},q^{\prime}),b)\xrightarrow{a,\phi}(P^{h}_{1},\ldots,P^{\prime h}_{i}=(q,I^{\prime h}_{i},q^{\prime\prime}),a)$, when $q^{\prime}\xrightarrow{a,\phi}q^{\prime\prime}$ is in $\Delta$, and $b\in\Sigma$. 2. 2.

For $a$ in $\Sigma$:

$(P^{h}_{1},\ldots,P^{h}_{i}=(q,I^{h}_{i},q^{\prime}),\#)\xrightarrow{a,\phi\wedge x_{\#}=0}(P^{h}_{1},\ldots,P^{\prime h}_{i}=(q,I^{\prime h}_{i},q^{\prime\prime}),a)$, when $q^{\prime}\xrightarrow{a,\phi}q^{\prime\prime}$ is in $\Delta$, and $b\in\Sigma$. 3. 3.

For $a$ in $\Sigma$:

$(P^{h}_{1},\ldots,P^{h}_{i}=(q,I^{h}_{i},q^{\prime}),\#^{\prime})\xrightarrow{a,\phi\wedge x_{\#^{\prime}}=0}(P^{h}_{1},\ldots,P^{\prime h}_{i}=(q,I^{\prime h}_{i},q^{\prime\prime}),a)$, when $q^{\prime}\xrightarrow{a,\phi}q^{\prime\prime}$ is in $\Delta$, and $b\in\Sigma$. 4. 4.

For $a=\#$,

$(P^{h}_{1},\ldots,P^{h}_{i}=(q,I^{h}_{i},q^{\prime}),b)\xrightarrow{a,\phi\wedge x_{b}\in I^{\prime h}_{i+1}}(P^{h}_{1},\ldots,P^{\prime h}_{i+1}=(q^{\prime\prime},I^{\prime h}_{i+1},q^{\prime\prime}),\#)$, when $q^{\prime}\xrightarrow{a,\phi}q^{\prime\prime}$ is in $\Delta$. 5. 5.

For $a=\#^{\prime}$,

$(P^{h}_{1},\ldots,P^{h}_{i}=(q,I^{h}_{i},q^{\prime}),a)\xrightarrow{a,\phi,x_{\#^{\prime}}\in\hat{I}^{h}_{1}}(\hat{P}^{h}_{1}=(q^{\prime},\hat{I}^{h}_{1},q^{\prime}),\#^{\prime})$, when $q^{\prime}\xrightarrow{a,\phi}q^{\prime\prime}$ is in $\Delta$.

Given a timed word $w$ accepted by $A$, when $A$ is restricted to $A^{h}$ then it is running on $w^{\prime h}$, the projection of $w$ on $\Sigma^{h}$, interspersed with $\#$ separating the maximal $h$-contexts in original word $w$. Let $v_{1},v_{2},\ldots,v_{m}$ be the sequence of switching vectors witnessed by $A^{h}$ while reading $w^{\prime h}$.

Now when $w^{\prime h}$ is fed to the constructed machine $A^{k}_{h}$, it is interspersed with new symbols $\#^{\prime}$ whenever the stack is empty just after a return symbol is read. Now $\bar{w}^{h}$ thus constructed is again a collection of $z$ stack-$h$ contexts which possibly are more in number than in $w^{\prime h}$. And each newly created context is either equal to some context of $w^{\prime h}$ or is embedded in exactly one context of $w^{\prime h}$. These give rise to sequence of switching vectors $v^{\prime}_{1},v^{\prime}_{2},\ldots,v^{\prime}_{z}$, where $m\leq z$. That explains the embedding of switching vectors witnessed by $A^{k}_{h}$, while reading $\bar{w}^{h}$, into switching vectors of $A$, while reading $w^{h}$. ∎

Let $w$ be in $L(A)$. Then as described above we can have a sequence of switching vectors $\bar{\mathbb{V}}_{h}$ for stack-$h$ machine $A^{h}_{k}$. Let $d^{h}$ be the number of $h$-contexts in the $k$-scoped splitting of $w$ i.e., the number of $h$-contexts in $\bar{w}^{h}$. Then we have those many tuples in the sequence of switching vectors $\bar{\mathbb{V}}^{h}$. Therefore, $\bar{\mathbb{V}}^{h}=\Pi_{y\in\{1,\ldots,d_{h}\}}\langle l^{h}_{y},I^{h}_{y},l^{\prime h}_{y}\rangle$.

We define the relation between elements of $\bar{\mathbb{V}}^{h}$ across all such sequences. While reading the word $w$, for all $h$ and $h^{\prime}$ in $\{1,\ldots,n\}$ and for some $y$ in $\{1,\ldots,d_{h}\}$ and some $y^{\prime}$ in $\{1,\ldots,d_{h^{\prime}}\}$ we define a relation $\emph{follows}(h,y)=(h^{\prime}y^{\prime})$ if $y$-th $h$-context is followed by $y^{\prime}$-th $h^{\prime}$-context.

A collection of correct sequences of context switches given via switching vectors $(\bar{\mathbb{V}}^{1},\ldots,\bar{\mathbb{V}}^{n})$ is called globally correct if we can stitch together runs of all $A^{h}_{k}$s on $\bar{w}^{h}$ using these switching vectors to get a run of $A$ on word $w$.

In the reverse direction, if for a given $k$-scoped word $w$ over $\Sigma$ which is in $L(A)$ then we have, collection of globally correct switching vectors $(\bar{\mathbb{V}}^{1},\ldots,\bar{\mathbb{V}}^{n})$.

The following lemma enables us to construct a run of $k$-scope ECMVPA on word $w$ over $\Sigma$ from the runs of ECVPA $A^{j}_{k}$ on $h$-projection of $w$ over $\Sigma^{j}$ with the help of switching vectors.

Lemma 3 (Stitching Lemma)

Let $A=(k,L,\Sigma,\Gamma,L^{0},F,\Delta)$ be a $k$-scope dt-ECMVPA. Let $w$ be a $k$-scoped word over $\Sigma$. Then $w\in L(A)$ iff there exist a collection of globally correct sequences of switching vectors for word $w$.

Proof

$(\Rightarrow)$: Assuming $w\in L(A)$ to prove existence of a collection of globally correct sequences is easy.

$(\Leftarrow)$: Assume that we have a collection of globally correct switching vectors $(\bar{\mathbb{V}}^{1},\ldots,\bar{\mathbb{V}}^{n})$ of $A$, for a word $w$. For each $h$ in $\{1,\ldots,n\}$ we have $k$-scoped splitting of word $w$ and we have a run of $A^{h}_{k}$ on $\bar{w}^{h}$, which uses $\bar{\mathbb{V}}^{h}$, the corresponding switching vector of $A$.

Let $\bar{w}$ be the word over $\Sigma\cup\{\#^{1},\ldots,\#^{n}\}\cup{\{\#^{\prime 1},\ldots,\#^{\prime n}\}}$, obtained from $w$ by using $k$-splitting as follows. Let $w=w_{1}w_{2}\ldots w_{d}$ We first insert $\#^{j}$ before $w_{1}$ if $w_{1}$ is a $j$-context. Then for all $i$ in $\{1,\ldots,d\}$, insert $\#^{l}$ in between $w_{i}$ and $w_{i+1}$ if $w_{i+1}$ is $l$-th context. Let us insert special symbol \#^{\}$to mark the end of word$w$. Now using$k$-splitting of word$w$we throw in$#^{\prime h}$as done in the case of obtaining$\bar{w}^{h}$from$w^{h}$.

Now we build a composite machine whose constituents are $A^{h}_{k}$ for all $h$ in $\{1,\ldots,n\}$. Its initial state is $(p^{1},\ldots,p^{j},\ldots,p^{n},j)$ where $p^{j}$ s are the initial states of $A^{j}_{k}$s and the last component tells which component is processing current symbol. According to this, initially we are processing first $j$-context in $\bar{w}^{j}$.

We first run $A^{j}_{k}$ on $\bar{w}^{j}$ updating location $p^{j}$ to $p^{\prime j}$ where $p^{\prime j}=(\bar{v}^{j}=(l^{j}_{1},I^{j}_{1},l^{\prime j}_{1}),a)$. When it reads $\#^{g}$ then $p^{\prime j}=(\bar{v}^{j}=(l^{j}_{1},I^{j}_{1},l^{\prime j}_{1}),\#^{g})$ and the composite state is changed to $(p^{1},\ldots,p^{\prime j},\ldots,p^{n},g)$ meaning that next context belongs to $g$-th stack. So we start simulating $A$ on first $g$-context in $\bar{w}^{g}$. But to do that $A^{j}_{k}$ should have left us in a state where $A^{g}_{k}$ can begin. That is if $p^{g}=(\bar{v}^{g}=(l^{g}_{1},I^{g}_{1},l^{\prime g}_{1}),\#^{g})$ we should have $l^{g}_{1}=l^{\prime j}_{1}$ and $x_{\#^{\prime g}}=0$ which will be the case as this is the first time we accessing $g$-th stack.

In general, if we are leaving a $j$-context and the next context belongs to $g$-th stack then the time elapsed from reading the last symbol of last $g$-context should falls in the interval of the first element of next switching vector processing next $g$-context in $\bar{w}^{g}$, along with the matching of state in which the previous context has left us in.

4 Emptiness checking and Determinizability of scope-bounded ECMVPA

First we show that emptiess problem is decidable using the ideas from [8]. Fix a $k\in\mathbb{N}$.

Theorem 4.1

Emptiness checking for $k$-scope ECMVPA is decidable.

Proof (Proof sketch)

Decidability of emptiness checking of $k$-round ECMVPA has been shown in [8]. This proof works for any general ECMVPA as the notion $k$-round has not been used. So, the same proof can be used to decide emptiness checking of $k$-scope ECMVPA.

Rest of the section is devoted for the proof of following theorem.

Theorem 4.2

The class of $k$-scope ECMVPA are determinizable.

To show this we use the determinization of VPA [6] and we recall this construction here for the reader’s convenience.

Determinization of VPA [6]

Given a VPA $M=(Q,Q_{in},\Gamma,\delta,Q_{F})$, the idea in [6] is to do a subset construction. Let $w=w_{1}a_{1}w_{2}a_{2}w_{3}$ be a word such that every call in $w_{1},w_{2},w_{3}$ has a matching return, and $a_{1},a_{2},a_{3}$ are call symbols without matching returns. After reading $w$, the deterministic VPA has stack contents $(S_{2},R_{2},a_{2})(S_{1},R_{1},a_{1})\bot$ and is in control state $(S,R)$. Here, $S_{2}$ contains all pairs of states $(q,q^{\prime})$ such that starting with $q$ on $w_{2}$ and an empty stack (contains only $\bot$), we reach $q^{\prime}$ with stack $\bot$. The set of pairs of states $S_{2}$ is called a summary for $w_{2}$. Likewise, $S_{1}$ is a summary for $w_{1}$ and $S$ is the summary for $w_{3}$. Here $R_{i}$ is the set of states reachable from the initial state after reading till the end of $w_{i}$, $i=1,2$ and $R$ is the set of reachable states obtained on reading $w$.

After $w_{3}$, if a call $a_{3}$ occurs, then $(S,R,a_{3})$ is pushed on the stack, and the current state is $(S^{\prime},R^{\prime})$ where $S^{\prime}=\{(q,q)\mid q\in Q\}$, while $R^{\prime}$ is obtained by updating $R$ using all transitions for $a_{3}$. The current control state $(S,R)$ is updated to $(S^{\prime},R^{\prime})$ where $R^{\prime}$ in the case of call and internal symbols is the set of all reachable states obtained from $R$, using all possible transitions on the current symbol read, and where the set $S^{\prime}$ is obtained as follows:

• •

On reading an internal symbol, $S$ evolves into $S^{\prime}$ where $S^{\prime}=\{(q,q^{\prime})\mid\exists q^{\prime\prime},(q,q^{\prime\prime})\in S,(q^{\prime\prime},a,q^{\prime})\in\delta\}$.

• •

On reading a call symbol $a$, $(S,R,a)$ is pushed onto the stack, and the control state is $(S^{\prime},R^{\prime})$ where $S^{\prime}=\{(q,q)\mid q\in Q\}$. On each call, $S^{\prime}$ is re-initialized.

• •

On reading a return symbol $a^{\prime}$, let the top of stack be $(S_{1},R_{1},a)$. This is popped. Thus, $a$ and $a^{\prime}$ are a matching call-return pair. Let the string read so far be $waw^{\prime}a^{\prime}$. Clearly, $w,w^{\prime}$ are well-nested, or all calls in them have seen their returns.

For the well-nested string $w$ preceding $a$, we have $S_{1}$ consisting of all $(q,q^{\prime\prime})$ such that starting on $q$ on $w$, we reach $q^{\prime\prime}$ with empty stack. Also, $S$ consists of pairs $(q_{1},q_{2})$ that have been obtained since the call symbol $a$ (corresponding to the return symbol $a^{\prime}$) was pushed onto the stack. The set $S$ started out as $\{(q_{1},q_{1})\mid q_{1}\in Q\}$ on pushing $a$, and contains pairs $(q_{1},q_{2})$ such that on reading the well-nested string between $a$ and $a^{\prime}$, starting in $q_{1}$, we reach $q_{2}$. The set $S$ is updated to $S^{\prime}$ by “stitching” $S_{1}$ and $S$ as follows:

A pair $(q,q^{\prime})\in S^{\prime}$ if there is some $(q,q^{\prime\prime})\in S_{1}$, and $(q^{\prime\prime},a,q_{1},\gamma)\in\delta$ (the push transition on $a$), $(q_{1},q_{2})\in S$, and $(q_{2},a^{\prime},\gamma,q^{\prime})\in\delta$ (the pop transition on $a^{\prime}$).

In this case, a state $q^{\prime}\in R^{\prime}$ if there exists some location $q$ in $R_{1}$ and there exists and $(q,a,q_{1},\gamma)\in\delta$ (the push transition on $a$), $(q_{1},q_{2})\in S^{\prime}_{1}$, and $(q_{2},a^{\prime},\gamma,q^{\prime})\in\delta$ (the pop transition on $a^{\prime}$). The important thing is the reachable set of states of non-deterministic machine after the call transition is updated using all possible summaries of well-matched words possible after the corresponding push transition in the past.

The set of final locations of the determinized VPA are $\{(S,R)\mid R$ contains a final state of the starting VPA$\}$, and its initial location is the set of all pairs $(S_{in},R_{in})$ where $S_{in}=\{(q,q)\mid q\in Q\}$ and $R_{in}$ is the set of all initial states of the starting VPA.

Determinization of $k$-scope ECMVPA

In this section we show that $k$-scope ECMVPA are determinizable using the result from [23] that single stack ECVPA are determinizable.

Let $A=(k,L,\Sigma,\Gamma,L^{0},F,\Delta)$ be the $k$-scoped ECMVPA and let $A^{h}_{k}$ be the ECVPA on $\Sigma^{h}\cup\{\#^{h},\#^{\prime h}\}$. Each $A^{h}_{k}$ is determinizable [23]. Recall from [23] that an ECVPA $A^{h}_{k}$ is untimed to obtain a VPA $ut(A^{h}_{k})$ by encoding the clock constraints of $A^{h}_{k}$ in an extended alphabet. This VPA can be converted back into an ECVPA $ec(ut(A^{h}_{k}))$ by using the original alphabet, and replacing the clock constraints. This construction is such that $L(ec(ut(A^{h}_{k})))=L(A^{h}_{k})$ and both steps involved preserve determinism. Determinization of VPA $ut(A^{h}_{k})$ is done in the usual way [6]. This gives $Det(ut(A^{h}_{k}))$. Again, $ec(Det(ut(A^{h}_{k})))$ converts this back into a ECVPA by simplifying the alphabet, and writing the clock constraints. The set of locations remain unchanged in $ec(Det(ut(A^{h}_{k})))$ and $Det(ut(A^{h}_{k}))$. This translation also preserves determinism, hence $B^{h}_{k}=ec(Det(ut(A^{h}_{k})))$ is a deterministic ECVPA language equivalent to ECVPA $A^{h}_{k}$. This process is also explained in the Figure 2.

The locations of $B^{h}_{k}$ are thus of the form $(S,R)$ where $R$ is the set of all reachable control states of $A^{h}_{k}$ and $S$ is a set of ordered pairs of states of $A^{h}_{k}$ as seen in section 4. On reading $\kappa_{j}$, the $R$ component of the state reached in $B^{h}_{k}$ is the set $\{\langle V^{h}\rangle\mid V^{h}~{}\mbox{is a last component of switching sequence}~{}\bar{\mathbb{V}}^{h}$ of $A^{h}_{k}\}$. Lemmas 2 and Lemma 3 follow easily using $B^{h}_{k}=ec(Det(ut(A^{h}_{k})))$ in place of $A^{h}_{k}$. We now obtain a deterministic $k$-scoped ECMVPA $B$ for language of $k$-scoped ECMVPA $A$ by simulating $B^{1}_{k},\dots,B^{k}_{k}$ one after the other on reading $w$, with the help of globally correct sequences of k-scoped switching vectors of $A^{h}_{k}$ s.

Automaton $B$ in its finite control, keeps track of the locations of all the $B^{h}_{k}$’s, along with the valuations of all the recorders and predictors of $\Sigma$. It also remembers the current context number of the $B^{h}_{k}$’s to ensure correct simulation.

Let $B^{h}_{k}=(Q^{h},\Sigma^{h}\cup\{\#,\#^{\prime}\},\Gamma^{h},Q^{h}_{0},F^{h},\delta^{h})$. Locations of $B^{h}_{k}$ have the form $(S^{h},R^{h})$. The initial state of $B^{h}_{k}$ is the set consisting of all $(S_{in},R_{in})$ where $S_{in}=\{(q,q)\mid q$ is a state of $A^{h}_{k}\}$, and $R_{in}$ is the set of all initial states of $A^{h}_{k}$. Recall that a final state of $A^{h}_{k}$ is $V^{h}$ the last component switching vector $V^{h}$ of a correct switching sequence $\bar{\mathbb{V}}^{h}$ of $A^{h}_{k}$. Thus, an accepting run in $B^{h}_{k}$ goes through states $(S_{in},R_{in}),(S_{1},R_{1})\dots,(S_{m},R_{m}),\langle V^{h}\rangle$.

Locations of $B$ have the form $(q_{1},\dots,q_{n},h)$ where $q_{y}$ is a location of $B_{y}$, $h$ is the stack number of current context. Without loss of generality we assume that the first context in any word belongs to stack $1$. The initial location of $B$ is $(q_{11},q_{12},\dots,q_{1n},1)$ where $q_{1h}$ is the initial location of $B^{h}_{k}$. We define the set of final locations of $B$ to be $(\langle V^{1}\rangle,\ldots\langle V^{n-1}\rangle\langle S_{n},R_{n}\rangle)$ where $R_{n}$ is a set containing a tuple of the form $(k,l^{\prime}_{kn},V_{n},a)$ and $l^{\prime}_{kn}$ is in $F$, the set of final locations of $A$.

We now explain the transitions $\Delta$ of $B$, using the transitions $\delta^{j}$ of $B^{h}_{k}$. Recall that $B$ processes $w=w_{1}w_{2}\dots w_{m}$ where each $w_{i}$ is context of some stack.When $w$ is $k$-scoped we can see $w$ as the concatenation of contexts $w=\bar{w}_{1}\bar{w}_{2}\ldots\bar{w}_{\bar{m}}$ where consecutive contexts need not belong to different stacks, and $\bar{m}\geq m$. Let $\eta=(q_{1},\dots,q_{h-1},q_{h},q_{h+1},\dots,q_{n},h)$ and let

$\zeta=(q_{1},\dots,q_{h-1},q,q_{h+1},\dots,q_{n},h)$, where $q_{h}$ is some state of $B^{h}_{k}$ while processing some context of $h$-th stack.

Simulation of $B^{h}_{k}$ when the $\bar{w}_{\bar{m}}$ is not an $h$-context.

• •

$\langle\eta,a,\varphi,\zeta\rangle\in\Delta^{j}_{l}$ iff $(q_{ij},a,\varphi,q)\in\delta_{l}^{j}$

• •

$\langle\eta,a,\varphi,\zeta,\gamma\rangle\in\Delta^{j}_{c}$ iff $(q_{ij},a,\varphi,\gamma,q)\in\delta_{c}^{j}$

• •

$\langle\eta,a,\gamma,\varphi,\zeta\rangle\in\Delta^{j}_{r}$ iff $(q_{ij},a,\gamma,\varphi,q)\in\delta_{r}^{j}$ 2. 2.

Change context from $h$ to $h+1$. Assume that we have processed $h$-context $\bar{w}_{g}$ and next context is $\bar{w}_{g+1}$ which is an $(h+1)$-context. Let the current state of $B$ is $\eta=(q_{1},\dots,q_{h-1},q_{h},q_{h+1},\dots,q_{n},h)$ after processing $\bar{w}_{g}$. At this point $B^{h}_{k}$ reads symbol $\#$ in $\bar{\kappa}^{h}$ and moves from state $q_{h}$ to $q^{\prime}_{h}$. Therefore, current state of $B$ becomes $\eta^{\prime}=(q_{1},\dots,q_{h-1},q^{\prime}_{h},q_{h+1},\dots,q_{n},h)$ At this point, $B$ invokes $B^{h+1}_{k}$ and starts reading first symbol of $\bar{w}_{g+1}$ when $B$ is in state $\eta^{\prime}$. This is meaningful because of Lemma 3. States of $q_{h+1}$ are of the form $(S^{h+1},R^{h+1})$ where $R^{h+1}$ have states of $A^{h+1}_{k}$ of the form $(\bar{\mathbb{V}}^{h+1},a)$, which is a possible state after processing last $h+1$ context. Globally correct stitching sequence guarantees that for all $(\bar{\mathbb{V}}^{h},a)\in R^{\prime h}$ we have at least one $(\bar{\mathbb{V}}^{h+1},a)\in R^{\prime h+1}$ such that $\bar{\mathbb{V}}^{\prime h}[last]=(x,I,y)$ then $\bar{\mathbb{V}}^{\prime h+1}[first]=(y,I^{\prime},z)$ and valuation of clocks at $\eta^{\prime}$ belongs to $I^{\prime}$, where $x,y$ are locations of $A$, and where last is the last component of $\bar{\mathbb{V}}^{\prime h}$ after processing $\bar{w}_{g}$, and first is the first componet of switching vector $\bar{\mathbb{V}}^{\prime h+1}$ for processing $\bar{\mathbb{V}}^{\prime}{h+1}$. Component location $q_{h+1}$ will be replaced based on a transition of $B^{h+1}_{k}$, and $q^{\prime h}$ is also replaced with $q^{h}$ to take care of the transition on $\#$ in $B^{h}_{k}$, where $q^{h}=(S^{h},R^{h})$ with $R^{h}$ containing all locations of the form $(\bar{\mathbb{V}}^{h},a)$, where $a$ is the last symbol of $\bar{w}_{g}$.

• •

$\langle(\dots,q^{\prime}_{h},q_{h+1},\dots,h),a,\varphi,(\dots,q_{h},q,\dots,h+1)\rangle\in\Delta^{h+1}_{l}$ iff

$(q_{h+1},a,\varphi,q)\in\delta^{h+1}_{l}$

• •

$\langle(\dots,q^{\prime}_{h},q_{h+1},\dots,h),a,\varphi,(\dots,q_{h},q,\dots,h+1),\gamma\rangle\in\Delta^{h+1}_{c}$ iff

$(q_{h+1},a,\varphi,q,\gamma)\in\delta^{h+1}_{c}$

• •

$\langle(\dots,q^{\prime}_{h},q_{h+1},\dots,h),a,\gamma,\varphi,(\dots,q_{h},q,\dots,h+1)\rangle\in\Delta^{h+1}_{r}$ iff

$(q_{h+1},a,\gamma,\varphi,q)\in\delta^{h+1}_{r}$

Transitions of $B^{h+1}$ continue on $(\dots,q_{h},q,\dots,h+1)$ replacing only the $(h+1)$-th entry until $\bar{w}_{g+1}$ is read completely. 3. 3.

Reading $\bar{w}_{\bar{m}}$ the last context of word $w$. Without loss of generality assume that this is the context of $B^{n}_{k}$ and the previous context $\bar{w}_{\bar{m}-1}$ was the context of $B^{n-1}_{k}$. When $B^{n-1}_{k}$ stops reading last symbol of $\bar{w}_{\bar{m}}$ then it is in the state $\eta=(\mathcal{V}^{1},\mathcal{V}^{2},\ldots,\mathcal{V}^{n-1},(S^{\prime n},R^{\prime n}),n)$ where no more symbols are to be read, and each $B^{h}_{k}$ is in the state $\langle\mathcal{V}^{h}\rangle$, where $\mathcal{V}^{h}$ is the last component of $k$-scoped switching vector $\bar{\mathbb{V}}^{h}$, where $R^{\prime}_{n}$ is the set of all locations of the form $(\mathcal{V}^{n},a)$, where $a$ is the last symbol of $\bar{\mathbb{V}}^{h}$. This is accepting iff there exists $\ell^{\prime}_{kn}$ as the second destination of last tuple in $\mathcal{V}^{n}$ and $\ell^{\prime}_{kn}\in F$. Note that we have ensured the following:

1. (a)

$\bar{\mathbb{V}}^{h}=\displaystyle\Pi_{1\leq i\leq m_{h}}\mathcal{V}^{h}_{i}$ and is part of correct global sequence for all $1\leq h\leq n$, and $m_{h}$ is the number of $k$-switching vectors of $A^{h}_{k}$ used in the computation. 2. (b)

At the end of $\bar{w}_{arm}$, we reach in $B^{h}_{k}$, $(S^{\prime}_{kn},R^{\prime}_{kn})$ such that there exists $\ell^{\prime}_{kn}$ as the second destination of the last tuple in $\mathcal{V}^{n}$ and $\ell^{\prime}_{kn}\in F$. 3. (c)

When switching from one context to another continuity of state is used as given in the correct global sequence.

The above conditions ensure correctness of local switching and a globally correct sequence in $A$. Clearly, $w\in L(B)$ iff $w\in L(A)$ iff there is some globally correct sequence $\bar{\mathbb{V}}^{1}\dots\bar{\mathbb{V}}^{n}$.

5 Emptiness checking and Determinizability of scope-bounded dt-ECMVPA

Fix a $k\in\mathbb{N}$. The proof is via untiming stack construction to get $k$-scope ECMVPA for which emptiness is shown to be decidable in Theorem 4.1.

We first informally describe the untiming-the-stack construction to obtain from a $k$-scope-dt-ECMVPA $M$ over $\Sigma$, an $k$-scope-ECMVPA $M^{\prime}$ over an extended alphabet $\Sigma^{\prime}$ such that $L(M)=h(L(M^{\prime}))$ where $h$ is a homomorphism $h:\Sigma^{\prime}{\times}\mathbb{R}^{\geq 0}\rightarrow\Sigma{\times}\mathbb{R}^{\geq 0}$ defined as $h(a,t)=(a,t)$ for $a{\in}\Sigma$ and $h(a,t)=\varepsilon$ for $a{\notin}\Sigma$.

Our construction builds upon that of [7].

Let $\kappa$ be the maximum constant used in the $k$-scope-dt-ECMVPA $M$ while checking the age of a popped symbol in any of the stacks. Let us first consider a call transition $(l,a,\varphi,l^{\prime},\gamma)\in\Delta^{i}_{c}$ encountered in $M$. To construct an $k$-scope-ECMVPA $M^{\prime}$ from $M$, we guess the interval used in the return transition when $\gamma$ is popped from $i$th stack. Assume the guess is an interval of the form $[0,\kappa]$. This amounts to checking that the age of $\gamma$ at the time of popping is ${<}\kappa$. In $M^{\prime}$, the control switches from $l$ to a special location $(l^{\prime}_{a,{<}\kappa},\{{{<_{i}}\kappa}\})$, and the symbol $(\gamma,{{<}\kappa},\texttt{first})$111It is sufficient to push $(\gamma,{{<}\kappa},\texttt{first})$ in stack $i$, since the stack number is known as $i$ is pushed onto the $i$th stack.

Let $Z_{i}^{\sim}=\{\sim_{i}c\mid c{\in}\mathbb{N},c\leq k,\sim{\in}\{{<},\leq,>,\geq\}\}$. Let $\Sigma^{\prime}_{i}=\Sigma^{i}\cup Z_{i}^{\sim}$ be the extended alphabet for transitions on the $i$th stack. All symbols of $Z_{i}^{\sim}$ are internal symbols in $M^{\prime}$ i.e. $\Sigma^{\prime}_{i}=\left\{\Sigma^{i}_{c},\Sigma^{i}_{l}\cup Z_{i}^{\sim},\Sigma^{i}_{r}\right\}$. At location $(l^{\prime}_{a,{<}\kappa},\{{{<_{i}}\kappa}\})$, the new symbol ${{<_{i}}\kappa}$ is read and we have the following transition : $((l^{\prime}_{a,{<}\kappa},\{{{<_{i}}\kappa}\}),{{<_{i}}\kappa},x_{a}=0,(l^{\prime},\{{{<_{i}}\kappa}\}))$, which results in resetting the event recorder $x_{{<_{i}}\kappa}$ corresponding to the new symbol ${{<_{i}}\kappa}$. The constraint $x_{a}=0$ ensures that no time is elapsed by the new transition. The information ${{<_{i}}\kappa}$ is retained in the control state until $(\gamma,{{<}\kappa},\texttt{first})$ is popped from $i$th stack. At $(l^{\prime},\{{{<_{i}}\kappa}\}))$, we continue the simulation of $M$ from $l^{\prime}$. Assume that we have another push operation on $i$th stack at $l^{\prime}$ of the form $(l^{\prime},b,\psi,q,\beta)$. In $M^{\prime}$, from $(l^{\prime},\{{{<_{i}}\kappa}\})$, we first guess the constraint that will be checked when $\beta$ will be popped from the $i$th stack. If the guessed constraint is again ${<_{i}}\kappa$, then control switches from $(l^{\prime},\{{{<_{i}}\kappa}\})$ to $(q,\{{{<_{i}}\kappa}\})$, and $(\beta,{{<}\kappa},-)$ is pushed onto the $i$th stack and simulation continues from $(q,\{{{<_{i}}\kappa}\})$. However, if the guessed pop constraint is ${<_{i}}\zeta$ for $\zeta\neq\kappa$, then control switches from $(l^{\prime},\{{{<_{i}}\kappa}\})$ to $(q_{b,{<}\zeta},\{{{<_{i}}\kappa},{{<_{i}}\zeta}\})$ on reading $b$. The new obligation ${<_{i}}\zeta$ is also remembered in the control state. From $(q_{b,{<}\zeta},\{{{<_{i}}\kappa},{{<_{i}}\zeta}\})$, we read the new symbol ${<_{i}}\zeta$ which resets the event recorder $x_{{<_{i}}\zeta}$ and control switches to $(q,\{{{<_{i}}\kappa},{{<_{i}}\zeta}\})$, pushing $(\beta,{{<}\zeta},\texttt{first})$ on to the $i$th stack. The idea thus is to keep the obligation ${{<_{i}}\kappa}$ alive in the control state until $\gamma$ is popped; the value of $x_{{<_{i}}\kappa}$ at the time of the pop determines whether the pop is successful or not. If a further ${{<_{i}}\kappa}$ constraint is encountered while the obligation ${{<_{i}}\kappa}$ is already alive, then we do not reset the event clock $x_{{<_{i}}\kappa}$. The $x_{{<_{i}}\kappa}$ is reset only at the next call transition after $(\gamma,{{<}\kappa},\texttt{first})$ is popped from $i$th stack , when ${{<_{i}}\kappa}$ is again guessed. The case when the guessed popped constraint is of the form ${>_{i}}\kappa$ is similar. In this case, each time the guess is made, we reset the event recorder $x_{{>_{i}}\kappa}$ at the time of the push. If the age of a symbol pushed later is ${>}\kappa$, so will be the age of a symbol pushed earlier. In this case, the obligation ${{>}\kappa}$ is remembered only in the stack and not in the finite control. Handling guesses of the form $\geq\zeta\wedge\leq\kappa$ is similar, and we combine the ideas discussed above.

Now consider a return transition $(l,a,I,\gamma,\varphi,l^{\prime})\in\Delta^{i}_{r}$ in $M$. In $M^{\prime}$, we are at some control state $(l,P)$. On reading $a$, we check the top of the $i$th stack symbol in $M^{\prime}$. It is of the form $(\gamma,S,\texttt{first})$ or $(\gamma,S,-)$, where $S$ is a singleton set of the form $\{{<}\kappa\}$ or $\{{>}\zeta\}$, or a set of the form $\{{<}\kappa,{>}\zeta\}$222This last case happens when the age checked lies between $\zeta$ and $\kappa$. Consider the case when the top of the $i$th stack symbol is $(\gamma,\{{<}\kappa,{>}\zeta\},\texttt{first})$. In $M^{\prime}$, on reading $a$, the control switches from $(l,P)$ to $(l^{\prime},P^{\prime})$ for $P^{\prime}=P\backslash\{{<}\kappa\}$ iff the guard $\varphi$ evaluates to true, the interval $I$ is $(\zeta,\kappa)$ (this validates our guess made at the time of push) and the value of clock $x_{{<_{i}}\kappa}$ is ${<}\kappa$, and the value of clock $x_{{>_{i}}\zeta}$ is ${>}\zeta$. Note that the third component first says that there are no symbols in $i$th stack below $(\gamma,\{{<}\kappa,{>}\zeta\},\texttt{first})$ whose pop constraint is ${<}\kappa$. Hence, we can remove the obligation ${<_{i}}\kappa$ from $P$ in the control state. If the top of stack symbol was $(\gamma,\{{<}\kappa,{>}\zeta\},-)$, then we know that the pop constraint ${<}\kappa$ is still alive for $i$th stack . That is, there is some stack symbol below $(\gamma,\{{<}\kappa,{>}\zeta\},-)$ of the form $(\beta,S,\texttt{first})$ such that ${<}\kappa{\in}S$. In this case, we keep $P$ unchanged and control switches to $(l^{\prime},P)$. Processing another $j$th stack continues exactly as above; the set $P$ contains $<_{i}\kappa,\leq_{j}\eta$, and so on depending on what constraints are remembered per stack. Note that the set $P$ in $(l,P)$ only contains constraints of the form $<_{i}\kappa$ or $\leq_{i}\kappa$ for each $i$th stack, since we do not remember $>\zeta$ constraints in the finite control.

We now give the formal construction.

Reduction from $k$-scope-dt-ECMVPA to $k$-scope-ECMVPA:

Let $Z^{\sim}=\bigcup_{i=1}^{n}Z^{\sim}_{i}$ and let $S^{\sim}=\{\sim c\mid c{\in}\mathbb{N},c\leq\kappa,\sim{\in}\{{<},\leq,{>},\geq,=\}\}$. Given $k$-scope-dt-ECMVPA $M=(L,\Sigma,\Gamma,L^{0},F,\Delta)$ with max constant $\kappa$ used in return transitions of all stacks, we construct $k$-scope-ECMVPA $M^{\prime}=(L^{\prime},\Sigma^{\prime},\Gamma^{\prime},L^{\prime 0},F^{\prime},\Delta^{\prime})$ where $L^{\prime}{=}(L{\times}2^{Z^{\sim}})\cup(L_{\Sigma_{i}{\times}S^{\sim}}{\times}2^{Z^{\sim}})\cup(L_{\Sigma_{i}{\times}S^{\sim}{\times}S^{\sim}}{\times}2^{Z^{\sim}})$, $\Sigma_{i}^{\prime}=(\Sigma^{i}_{c},\Sigma^{i}_{l}\cup Z_{i}^{\sim},\Sigma^{i}_{r})$ and $\Gamma_{i}^{\prime}=\Gamma_{i}{\times}2^{S^{\sim}}{\times}\{\texttt{first},-\}$, $L^{0}=\{(l^{0},\emptyset)\mid l^{0}{\in}L^{0}\}$, and $F=\{(l^{f},\emptyset)\mid l^{f}{\in}F\}$.

The transitions $\Delta^{\prime}$ are defined as follows:

Internal Transitions. For every $(l,a,\varphi,l^{\prime}){\in}\Delta^{i}_{l}$ we have the set of transitions $((l,P),a,\varphi,(l^{\prime},P)){\in}{\Delta^{i}}^{\prime}_{l}$. Call Transitions. For every $(l,a,\varphi,l^{\prime},\gamma){\in}\Delta^{i}_{c}$, we have the following classes of transitions in $M^{\prime}$.

The first class of transitions corresponds to the guessed pop constraint being ${<}\kappa$. In the case that, obligation is ${<}\kappa$ is alive in the state, hence there is no need to reset the clock $x_{{<_{i}}\kappa}$. Otherwise, the obligation ${<}\kappa$ is fresh and hence it is remembered as first in the $i$th stack, and the clock $x_{{<_{i}}\kappa}$ is reset.

[TABLE] 2. 2.

The second class of transitions correspond to the guessed pop constraint ${>}\kappa$. The clock $x_{{>_{i}}\kappa}$ is reset, and obligation is stored in $i$th stack.

[TABLE] 3. 3.

Finally the following transitions consider the case when the guessed pop constraint is ${>}\zeta$ and ${<}\kappa$. Depending on whether ${<}\kappa$ is alive or not, we have two cases. If alive, then we simply reset the clock $x_{{>_{i}}\zeta}$ and remember both the obligations in $i$th stack. If ${<}\kappa$ is fresh, then we reset both clocks $x_{{>_{i}}\zeta}$ and $x_{{<_{i}}\kappa}$ and remember both obligations in $i$th stack , and ${<_{i}}\kappa$ in the state.

[TABLE]

Return Transitions. For every $(l,a,I,\gamma,\varphi,l^{\prime}){\in}\Delta^{i}_{r}$, transitions in ${\Delta^{i}}^{\prime}_{r}$ are:

$((l,P),a,(\gamma,\{{<}\kappa,{>}\zeta\},-),\varphi\wedge x_{{<_{i}}\kappa}{<}\kappa\wedge x_{{>_{i}}\zeta}{>}\zeta,(l^{\prime},P))$ if $I=(\zeta,\kappa)$. 2. 2.

$((l,P),a,(\gamma,\{{<}\kappa,{>}\zeta\},\texttt{first}),\varphi\wedge x_{{<_{i}}\kappa}{<}\kappa\wedge x_{{>_{i}}\zeta}{>}\zeta,(l^{\prime},P^{\prime}))$

where $P^{\prime}=P\backslash\{{<_{i}}\kappa\}$, if $I=(\zeta,\kappa)$. 3. 3.

$((l,P),a,(\gamma,\{{<}\kappa\},-),\varphi\wedge x_{{<_{i}}\kappa}{<}\kappa,(l^{\prime},P))$ if $I=[0,\kappa)$. 4. 4.

$((l,P),a,(\gamma,\{{<}\kappa\},\texttt{first}),\varphi\wedge x_{{<_{i}}\kappa}{<}\kappa,(l^{\prime},P^{\prime}))$ with $P^{\prime}{=}P\backslash\{{<_{i}}\kappa\}$ if $I{=}[0,\kappa)$. 5. 5.

$((l,P),a,(\gamma,\{{>}\zeta\},-),\varphi\wedge x_{{>_{i}}\zeta}{>}\zeta,(l^{\prime},P))$ if $I=(\zeta,\infty)$.

For the pop to be successful in $M^{\prime}$, the guess made at the time of the push must be correct, and indeed at the time of the pop, the age must match the constraint. The control state $(l^{f},P)$ is reached in $M^{\prime}$ on reading a word $w^{\prime}$ iff $M$ accepts a string $w$ and reaches $l^{f}$. Accepting locations of $M^{\prime}$ are of the form $(l^{f},P)$ for $P\subseteq Z^{\sim}$. If $w$ is a matched word then $P$ is empty, and there must be any obligations which are pending at the end.

Let $w=(a_{1},t_{1})\dots(a_{i},t_{i})\dots(a_{n},t_{n}){\in}L(M)$. If $a_{i}\in\Sigma^{i}_{c}$, we have in $L(M^{\prime})$, a string $T_{i}$ between $(a_{i},t_{i})$ and $(a_{i+1},t_{i+1})$, with $|T_{i}|\leq 2$, and $T_{i}$ is a timed word of the form $(b_{1i},t_{i})(b_{2i},t_{i})$ or $(b_{1i},t_{i})$. The time stamp $t_{i}$ remains unchanged, and either $b_{1i}$ is $<_{i}\kappa$ or $\leq_{i}\kappa$ or $b_{1i}$ is $>_{i}\zeta$, or $b_{1i}$ is $>_{i}\zeta$ and $b_{2i}$ is one of $<_{i}\kappa$ or $\leq_{i}\kappa$ for some $\kappa,\zeta\leq k$. This follows from the three kinds of call transitions in $M^{\prime}$.

In the construction above, it can shown by inducting on the length of words accepted that $h(L(M^{\prime}))=L(M)$. Thus, $L(M^{\prime})\neq\emptyset$ iff $L(M)\neq\emptyset$. If $M$ is a $k$-scope-dt-ECMVPA, then $M^{\prime}$ is a $k$-scope-ECMVPA. Since $M^{\prime}$ is a $k$-scope-ECMVPA, its emptiness check is decidable using Theorem 4.1, which uses the standard region construction of event clock automata [5] to obtain a $k$-scope-MVPA, which has a decidable emptiness [20].

Theorem 5.1

The emptiness checking for $k$-scope dt-ECMVPA is decidable.

In [8] we have shown that $k$-round dt-ECMVPA are determinizable. Using an untiming construction to get $k$-round ECMVPA, determinize it and again converting this to get deterministic $k$-round dt-ECMVPA.

For $k$-scope dt-ECMVPA using the stack untiming construction we get a $k$-scope ECMVPA. This is determinized to get deterministic $k$-scope ECMVPA. We convert this back to get deterministic $k$-scope dt-MVPA. The morphisms used for this conversion are same as in [8].

Theorem 5.2

The $k$-scope dt-ECMVPA are determinizable.

Proof

Consider a $k$-scope dt-ECMVPA $M=(L,\Sigma,\Gamma,L^{0},F,\Delta)$ and the corresponding $k$-scope ECMVPA $M^{\prime}=(L^{\prime},\Sigma^{\prime},\Gamma^{\prime},L^{\prime 0},F^{\prime},\Delta^{\prime})$ as constructed in section LABEL:app:untime. From Theorem 4.2 we know that $M^{\prime}$ is determinizable. Let $Det(M^{\prime})$ be the determinized automaton such that $L(Det(M^{\prime}))=L(M^{\prime})$. That is, $L(M)=h(L(Det(M^{\prime})))$. By construction of $M^{\prime}$, we know that the new symbols introduced in $\Sigma^{\prime}$ are $Z^{\sim}$ ($\Sigma^{\prime}_{i}=\Sigma_{i}\cup Z_{i}^{\sim}$ for each $i$th stack ) and (i) no time elapse happens on reading symbols from $Z_{i}^{\sim}$, and (ii) no stack operations happen on reading symbols of $Z_{i}^{\sim}$. Consider any transition in $Det(M^{\prime})$ involving the new symbols. Since $Det(M^{\prime})$ is deterministic, let $(s_{1},\alpha,\varphi,s_{2})$ be the unique transition on $\alpha{\in}Z_{i}^{\sim}$. In the following, we eliminate these transitions on $Z_{i}^{\sim}$ preserving the language accepted by $M$ and the determinism of $det(M^{\prime})$. In doing so, we will construct a $k$-scope dt-ECMVPA $M^{\prime\prime}$ which is deterministic, and which preserves the language of $M$. We now analyze various types for $\alpha{\in}Z_{i}^{\sim}$.

Assume that $\alpha$ is of the form ${>_{i}}\zeta$. Let $(s_{1},\alpha,\varphi,s_{2})$ be the unique transition on $\alpha{\in}Z_{i}^{\sim}$. By construction of $M^{\prime}$ (and hence $det(M^{\prime})$), we know that $\varphi$ is $x_{a}=0$ for some $a{\in}\Sigma^{i}$. We also know that in $Det(M^{\prime})$, there is a unique transition $(s_{0},a,\psi,s_{1},(\gamma,\alpha,-))$ preceding $(s_{1},\alpha,\varphi,s_{2})$. Since $(s_{1},\alpha,\varphi,s_{2})$ is a no time elapse transition, and does not touch any stack, we can combine the two transitions from $s_{0}$ to $s_{1}$ and $s_{1}$ to $s_{2}$ to obtain the call transition $(s_{0},a,\psi,s_{2},\gamma)$ for $i$th stack . This eliminates transition on ${>_{i}}\zeta$. 2. 2.

Assume that $\alpha$ is of the form ${<_{i}}\kappa$. Let $(s_{1},\alpha,\varphi,s_{2})$ be the unique transition on $\alpha{\in}Z_{i}^{\sim}$. We also know that $\varphi$ is $x_{a}=0$ for some $a{\in}\Sigma^{i}$. From $M^{\prime}$, we also know that in $Det(M^{\prime})$, there is a unique transition of one of the following forms preceding $(s_{1},\alpha,\varphi,s_{2})$:

• (a)

$(s_{0},a,\psi,s_{1},(\gamma,\alpha,-))$, (b) $(s_{0},a,\psi,s_{1},(\gamma,\alpha,\texttt{first}))$, or

• (c)

$(s_{0},{>_{i}}\zeta,\varphi,s_{1})$ where it is preceded by $(s^{\prime}_{0},a,\psi,s_{0},(\gamma,\{\alpha,{>}\zeta\},X))$ for $X{\in}\{\texttt{first},-\}$.

As $(s_{1},\alpha,\varphi,s_{2})$ is a no time elapse transition, and does not touch the stack, we can combine two transitions from $s_{0}$ to $s_{1}$ (cases $(a)$, $(b)$) and $s_{1}$ to $s_{2}$ to obtain the call transition $(s_{0},a,\psi,s_{2},(\gamma,\alpha,-))$ or $(s_{0},a,\psi,s_{2},(\gamma,\alpha,\texttt{first}))$. This eliminates the transition on ${<_{i}}\kappa$.

In case of transition $(c)$, we first eliminate the local transition on ${>_{i}}\zeta$ obtaining $(s^{\prime}_{0},a,\psi,s_{1},\gamma)$. This can then be combined with $(s_{1},\alpha,\varphi,s_{2})$ to obtain the call transitions $(s^{\prime}_{0},a,\psi,s_{2},\gamma)$. We have eliminated local transitions on ${<_{i}}\kappa$.

Merging transitions as done here does not affect transitions on any $\Sigma^{i}$ as they simply eliminate the newly added transitions on $\Sigma_{i}^{\prime}\setminus\Sigma_{i}$. Recall that checking constraints on recorders $x_{<_{i}\kappa}$ and $x_{>_{i}\zeta}$ were required during return transitions. We now modify the pop operations in $Det(M^{\prime})$ as follows: Return transitions have the following forms, and in all of these, $\varphi$ is a constraint checked on the clocks of $C_{\Sigma^{i}}$ in $M$ during return: transitions $(s,a,(\gamma,\{{<}\kappa\},X),\varphi\wedge x_{{<_{i}}\kappa}{<}\kappa,s^{\prime})$ for $X{\in}\{-,\texttt{first}\}$ are modified to $(s,a,[0,\kappa),\gamma,\varphi,s^{\prime})$; transitions $(s,a,(\gamma,\{{<}\kappa,{>}\zeta\},X),\varphi\wedge x_{{>_{i}}\zeta}{{>}}\zeta\wedge x_{{<_{i}}\kappa}{{<}}\kappa,s^{\prime})$ for $X{\in}\{-,\texttt{first}\}$ are modified to $(s,a,(\zeta,\kappa),\gamma,\varphi,s^{\prime})$; and transition $(s,a,(\gamma,\{{>}\zeta\},-),\varphi\wedge x_{{>_{i}}\zeta}{>}\zeta,s^{\prime})$ are modified to the transitions $(s,a,(\zeta,\infty),\gamma,\varphi,s^{\prime})$. Now it is straightforward to verify that the $k$-scope dt-ECMVPA $M^{\prime\prime}$ obtained from the $k$-scope ECMVPA $det(M^{\prime})$ is deterministic. Also, since we have only eliminated symbols of $Z^{\sim}$, we have $L(M^{\prime\prime})=L(M)$ and $h(L(M^{\prime\prime}))=L(det(M^{\prime}))$. This completes the proof of determinizability of $k$-scope dt-ECMVPA.

It is easy to show that $k$-scoped ECMVPAs and $k$-scoped dt-ECMVPAs are closed under union and intersection; using Theorem 4.2 and Theorem 5.2 we get closure under complementation.

Theorem 5.3

The classes of $k$-scoped ECMVPLs and $k$-scoped dt-ECMVPLs are closed under Boolean operations.

6 Logical Characterization of $k$-dt-ECMVPA

Let $w=(a_{1},t_{1}),\ldots,(a_{m},t_{m})$ be a timed word over alphabet $\Sigma=\langle\Sigma^{i}_{c},\Sigma^{i}_{l},\Sigma^{i}_{r}\rangle_{i=1}^{n}$ as a word structure over the universe $U=\{1,2,\dots,|w|\}$ of positions in $w$. We borrow definitions of predicates $Q_{a}(i),\lhd_{a}{\kern-1.0pt}(i),\rhd_{{\kern-2.0pt}a}{\kern-1.0pt}(i)$ from  [7]. Following [16], we use the matching binary relation $\mu_{j}(i,k)$ which evaluates to true iff the $i$th position is a call and the $k$th position is its matching return corresponding to the $j$th stack. We introduce the predicate $\theta_{j}(i)\in I$ which evaluates to true on the word structure iff $w[i]=(a,t_{i})$ with $a\in\Sigma^{j}_{r}$ and $w[i]\in\Sigma^{j}_{r}$, and there is some $k<i$ such that $\mu_{j}(k,i)$ evaluates to true and $t_{i}-t_{k}\in I$. The predicate $\theta_{j}(i)$ measures time elapsed between position $k$ where a call was made on the stack $j$, and position $i$, its matching return. This time elapse is the age of the symbol pushed onto the stack during the call at position $k$. Since position $i$ is the matching return, this symbol is popped at $i$, if the age lies in the interval $I$, the predicate evaluates to true. We define MSO($\Sigma$), the MSO logic over $\Sigma$, as:

[TABLE]

where $a{\in}\Sigma$, $x_{a}{\in}C_{\Sigma}$, $x$ is a first order variable and $X$ is a second order variable.

The models of a formula $\phi\in\mbox{MSO}(\Sigma)$ are timed words $w$ over $\Sigma$. The semantics is standard where first order variables are interpreted over positions of $w$ and second order variables over subsets of positions. We define the language $L(\varphi)$ of an MSO sentence $\varphi$ as the set of all words satisfying $\varphi$.

Words in $Scope(\Sigma,k)$, for some $k$, can be captured by an MSO formula $Scope_{k}(\psi)=\displaystyle\bigwedge_{1\leq j\leq n}Scope_{k}(\psi)^{j}$, where $n$ is number of stacks, where

$Scope_{k}(\psi)^{j}=\forall yQ_{a}(y)\wedge a\in\Sigma^{r}_{j}\Rightarrow(\exists x\mu_{j}(x,y)\wedge$ $(\psi_{kcnxt}^{j}\wedge\psi_{matcnxt}^{j}\wedge\psi_{noextracnxt}))$

where $\psi_{kcnxt}^{j}=\exists x_{1},\ldots,x_{k}(x_{1}\leq\ldots\leq x_{k}\leq y\displaystyle\bigwedge_{1\leq q\leq k}(Q_{a}(x_{q})\wedge a\in\Sigma_{j}\wedge(Q_{b}(x_{q}-1)\Rightarrow b\notin\Sigma_{j}))$,

and $\psi_{matcnxt}^{j}=\displaystyle\bigvee_{1\leq q\leq k}\forall x_{i}(x_{q}\leq x_{i}\leq x(Q_{c}(x_{i})\Rightarrow c\in\Sigma_{j}))$, and

$\psi_{noextracnxt}=\exists x_{l}(x_{1}\leq x_{l}\leq y)(Q_{a}(l)\wedge a\in\Sigma_{j}\wedge Q_{b}(x_{l}-1)\wedge b\in\Sigma_{j})\Rightarrow x_{l}\in\{x_{1},\ldots,x_{k}\}.$

Formulas $\psi_{noextracnxt}$ and $\psi_{kcnxt}$ say that there are at most $k$ contexts of $j$-th stack, while formula $\psi_{matcnxt}$ says where matching call position $x$ of return position $y$ is found. Conjuncting the formula obtained from a dt-ECMVPA $M$ with $Scope(\psi)$ accepts only those words which lie in $L(M)\cap Scope(\Sigma,k)$. Likewise, if one considers any MSO formula $\zeta=\varphi\wedge Scope(\psi)$, it can be shown that the dt-ECMVPA $M$ constructed for $\zeta$ will be a $k$-dt-ECMVPA.

Hence we have the following MSO characterization.

Theorem 6.1

A language $L$ over $\Sigma$ is accepted by an k-scope dt-ECMVPA iff there is a MSO sentence $\varphi$ over $\Sigma$ such that $L(\varphi)\cap Scope(\Sigma,k)=L$.

The two directions, dt-ECMVPA to MSO, as well as MSO to dt-ECMVPA can be handled using standard techniques, and can be found in Appendix 0.B.

7 Conclusion

In this work we have seen timed context languages characterized by $k$-scope ECMVPA and dense-timed $k$-scope dt-ECMVPA, along with logical characterizations for both classes (for $k$-scope ECMVPA, equivalent MSO is obtained by dropping predicate $\theta_{j}(x){\in}I$–which checks if the aging time of pushed symbol $x$ of stack $j$ falls in interval $I$–from MSO of $k$-scope dt-ECMVPA).

Here, while reading an input symbol of a stack, clock constraints involve the clocks of symbols associated with the same stack. It would be interesting to see if our results hold without this restriction. Another direction, would be to use alternate methods like Ramsey theorem based [2, 14] or Anti-chain based [13, 10] methods avoiding complementation and hence determinization to do language inclusion check.

Appendix 0.A Case study: Modeling A single channel packet switching communication network

A single channel packet switching communication network uses a common medium to send fixed sized packets from a transmitter to one or many receivers. Such medium may be a bus or a cable or any other transmission medium. The communication network consists of multiple stations sharing a single error free communication channel supported by the medium. All stations transmit fixed sized packets of data over the channel and stations receive them. The time is slotted into frames and the transmission of new packet can start only at the beginning of the frame. It is possible that one than one stations may transmit packets simultaneously, and in that case packets are said to collide. Such collision results in the transmission error and whether a collision has occured or not is decided at the end of frame. If the collision has happended, it is visible to all stations and failure of communication is concluded. If no collision occurs, packet is assumed to be transmitted successfully. All stations employ same protocol to avoid collision and retransmission. Such choice of such protocol determines various characteristics of the network like stability and maximum throughput. Here we model the Capetanakis-Tsybakov-Mikhailov (CTM) protocol [22] using a dt-ECMVPA shown in Figure 3. It shows state transitions for station $i$. The actual automaton for CTM protocol is constructed by taking cross product of automata for all stations.

For each station $i$, the symbol $\text{SF}_{i}$, $\text{EF}_{i}$, $\text{P}_{i}$ and $\text{R}_{i}$ denote the start of frame, end of frame, arrival of new packet and receipt of packet respectively. We use a global shared variable array active to record stations which are actively sending packets. active[i] is true iff station $i$ is sending packet. We detect the occurance of collision if more that one entry in active is true. The constant $D_{F}$ denote the durations of frame (i.e. time difference between SF and EF). There is an idle period between two successive frames (i.e. time difference between EF for first frame and SF of the next frame). We denote it using constant $D_{I}$. The event clocks have been used to measure such timing requirements. CTM algorithm expects that start and end of frame is synchronized for all stations. Such requirement can be taken care by introducing extra symbols during initialization phase (not shown in Figure 3). We introduce additional return input symbol $P^{\prime}_{0}$. At global time zero input symbol $P_{0}$ occurs which pushes $\alpha_{0}$ on the stack at station 0. We then require that input symbols $\text{SF}_{0}\dots\text{SF}_{n}$ occur. We then mandate $P^{\prime}_{0}$ to occur when the age of popped $\alpha_{0}$ is zero. This ensures that the all $\text{SF}_{i}$ are synchronized when global time is zero.

Appendix 0.B Details of Theorem 6.1

Here, we give the details of the translations from dt-ECMVPA to MSO and conversely. A technical point is regarding the projection operation: in general, it is known that event clock automata (hence dt-ECMVPA) are not closed under projections. However, we need to handle projections while quantifying out variables in the MSO to dt-ECMVPA construction. We do this by working on Quasi dt-ECMVPA where the underlying alphabet $\Sigma$ is partitioned into finitely many buckets $P_{1},\dots,P_{k}$ via a ranking function $\rho:\Sigma\rightarrow\mathbb{N}$. All symbols in a $P_{j}$ are then “equivalent” : we assign one event recorder and one event predictor per $P_{i}$. This helps in arguing the correctness of the constructed dt-ECMVPA from an MSO formula while projecting out variables. In Section 0.B.1, we show the equi-expressiveness of quasi dt-ECMVPA and dt-ECMVPA which allows us to complete the logical characterization.

• •

Logic to automata. We first show that the language accepted by an MSO formula $\varphi$ over $\Sigma=\langle\Sigma^{i}_{c},\Sigma^{i}_{l},\Sigma^{i}_{r}\rangle_{i=1}^{n}$, $L(\varphi)$ is accepted by a dt-ECMVPA. Let $Z=(x_{1},\dots,x_{m},X_{1},\dots,X_{n})$ be the free variables in $\varphi$. As usual, we work on the extended alphabet $\Sigma^{\prime}=\langle{\Sigma^{i}}^{\prime}_{c},{\Sigma^{i}}^{\prime}_{l},{\Sigma^{i}}^{\prime}_{r}\rangle_{i=0}^{n}$ where

[TABLE]

for $s\in\{c,l,r\}$. A word $w^{\prime}$ over $\Sigma^{\prime}$ encodes a word over $\Sigma$ along with the valuation of all first order and second order variables. Thus ${\Sigma^{i}}^{\prime}$ consists of all symbols $(a,v)$ where $a\in\Sigma^{i}$ is such that $v(x)=1$ means that $x$ is assigned the position $i$ of $a$ in the word $w$, while $v(x)=0$ means that $x$ is not assigned the position of $a$ in $w$. Similarly, $v(X)=1$ means that the position $i$ of $a$ in $w$ belongs to the set $X$. Next, we use quasi-event clocks for $\Sigma^{\prime}$ by assigning suitable ranking function. Quasi dt-ECMVPA are equiexpressive to dt-ECMVPA as explained in Section 0.B.1. We partition each ${\Sigma^{i}}^{\prime}$ such that for a fixed $a\in\Sigma^{i}$, all symbols of the form $(a,d_{1},\dots,d_{m+n})$ and $d_{i}\in\{0,1\}$ lie in the same partition ($a$ determines their partition). Let $\rho^{\prime}:\Sigma^{\prime}\rightarrow\mathbb{N}$ be the ranking function of $\Sigma^{\prime}$ wrt above partitioning scheme.

Let $L(\psi)$ be the set of all words $w^{\prime}$ over $\Sigma^{\prime}$ such that the underlying word $w$ over $\Sigma$ satisfies formula $\psi$ along with the valuation $Val$. Structurally inducting over $\psi$, we show that $L(\psi)$ is accepted by a dt-ECMVPA. The cases $Q_{a}(x),\mu_{j}(x,y)$ are exactly as in [16]. We only discuss the predicate $\theta_{j}$ here. Consider the atomic formula $\theta_{j}(x)\in I$. To handle this, we build a dt-ECMVPA that keeps pushing symbols $(a,v)$ onto the stack $j$ whenever $a\in\Sigma^{j}_{c}$, initializing the age to 0 on push. It keeps popping the stack on reading return symbols $(a^{\prime},v^{\prime})$, $a^{\prime}\in\Sigma^{j}_{r}$, and checks whether $v^{\prime}(x)=1$ and $age(a^{\prime},v^{\prime})\in I$. It accepts on finding such a pop. The check $v^{\prime}(x)=1$ ensures that this is the matching return of the call made at position $x$. The check $age(a^{\prime},v^{\prime})\in I$ confirms that the age of this symbol pushed at position $x$ is indeed in the interval $I$. Negations, conjunctions, and disjunctions follow from the closure properties of dt-ECMVPA.

Existential quantifications correspond to a projection by excluding the chosen variable from the valuation and renaming the alphabet $\Sigma^{\prime}$. Let $M$ be a dt-ECMVPA constructed for $\varphi(x_{1},\dots,x_{n},X_{1},\dots,X_{m})$ over $\Sigma^{\prime}$. Consider $\exists x_{i}.\varphi(x_{1},\dots,x_{n},X_{1},\dots,X_{m})$ for some first order variable $x_{i}$. Let $Z_{i}=(x_{1},\dots,x_{i-1},x_{i+1},\dots,x_{n},X_{1},\dots,X_{m})$ by removing $x_{i}$ from $Z$. We simply work on the alphabet $\Sigma^{\prime}{\downarrow}i=\Sigma\times(Val:Z_{i}\rightarrow\{0,1\}^{m+n-1})$. Note that $\Sigma^{\prime}{\downarrow}i$ is partitioned exactly in the same way as $\Sigma^{\prime}$. For a fixed $a\in\Sigma$, all symbols $(a,d_{1},\dots,d_{m+n-1})$ for $d_{i}\in\{0,1\}$ lie in the same partition. Thus, $\Sigma^{\prime}$ and $\Sigma^{\prime}{\downarrow}i$ have exactly the same number of partitions, namely $|\Sigma|$. Thus, an event clock $x_{a}=x_{(a,d_{1},\dots,d_{m+n})}$ used in $M$ can be used the same way while constructing the automaton for $\exists x_{i}.\varphi(x_{1},\dots,x_{n},X_{1},\dots,X_{m})$. The case of $\exists X_{i}.\varphi(x_{1},\dots,x_{n},X_{1},\dots,X_{m})$ is similar. Hence we obtain in all cases, a dt-ECMVPA that accepts $L(\psi)$ when $\psi$ is an MSO sentence.

• •

Automata to logic. Consider a dt-ECMVPA $M=(L,\Sigma,\Gamma,L^{0},F,\Delta)$. For each stack $i$, let $C^{i}_{\gamma}$ denote a second order variable which collects all positions where $\gamma$ is pushed in stack $i$. Similarly, let $R^{i}_{\gamma}$ be a second order variable which collects all positions where $\gamma$ is popped from stack $i$. Let $X_{l_{i}}$ be a second order variable which collects all positions where the location is $l_{i}$ in a run. Let $\mathcal{C}$, $\mathcal{R}$ and $\mathcal{L}$ respectively be the set of these variables.

The MSO formula encoding runs of the dt-ECMVPA is: $\exists\mathcal{L}~{}\exists\mathcal{C}~{}\exists\mathcal{R}~{}\varphi(\mathcal{L},\mathcal{C},\mathcal{R})$. We assert that the starting position must belong to $X_{l}$ for some $l\in L^{0}$. Successive positions must be connected by an appropriate transition. To complete the reduction we list these constraints.

• –

For call transitions $(\ell_{i},a,\psi,\ell_{j},\gamma)\in\Delta^{h}_{c}$, for positions $x,y$, assert

[TABLE]

[TABLE]

• –

For return transitions $(\ell_{i},a,I,\gamma,\psi,\ell_{j})\in\Delta^{h}_{r}$ for positions $x$ and $y$ we assert that

[TABLE]

[TABLE]

• –

Finally, for internal transitions $(\ell_{i},a,\psi,\ell_{j})\in\Delta^{h}_{l}$ for positions $x$ and $y$ we assert

[TABLE]

We also assert that the last position of the word belongs to some $X_{l}$ such that there is a transition (call, return, local) from $l$ to an accepting location. The encoding of all three kinds of transitions are given as above. Additionally, we assert that corresponding call and return positions should match, i.e.

[TABLE]

0.B.1 Remaining part: Quasi dt-ECMVPA

A quasi k-dt-ECMVPA is a weaker form of k-dt-ECMVPA where more than one input symbols share the same event clock. Let the finite input alphabet $\Sigma$ be partitioned into finitely many classes via a ranking function $\rho:\Sigma\to\mathbb{N}$ giving rise to finitely many partitions $P_{1},\dots,P_{k}$ of $\Sigma$ where $P_{i}=\left\{a\in\Sigma\mid\rho(a)=i\right\}$. The event recorder $x_{P_{i}}$ records the time elapsed since the last occurrence of some action in $P_{i}$, while the event predictor $y_{P_{i}}$ predicts the time required for any action of $P_{i}$ to occur. Notice that since clock resets are “visible” in input timed word, the clock valuations after reading a prefix of the word are also determined by the timed word.

Definition 6 (Quasi k-dt-ECMVPA)

A quasi $k$-dt-ECMVPA over alphabet $\Sigma{=}\left\{\Sigma^{i}_{c},\Sigma^{i}_{r},\Sigma^{i}_{l}\right\}_{i=1}^{n}$ is a tuple $M{=}(L,\Sigma,\rho,\Gamma,L^{0},F,\Delta)$ where $L$ is a finite set of locations including a set $L^{0}\subseteq L$ of initial locations, $\rho$ is the ranking function, $\Gamma$ is the stack alphabet and $F{\subseteq}L$ is a set of final locations.

Lemma 4

Quasi k-dt-ECMVPA and k-dt-ECMVPA are effectively equivalent.

The proof of Lemma 4 is obtained by using the construction proposed in the proof of Lemma 5 for single stack machines.

Lemma 5 ([7])

The class of $q$-dtVPA is equally expressive as the class of dtVPA.

Valid homomorphisms for quasi k-dtMVPA

Let $\Sigma=\left\{\Sigma^{i}_{c},\Sigma^{i}_{r},\Sigma^{i}_{l}\right\}_{i=1}^{n}$ and $\Pi=\left\{\Pi^{i}_{c},\Pi^{i}_{r},\Pi^{i}_{l}\right\}_{i=1}^{n}$ be the alphabets of k-dtMVPAs $M_{1}=(L_{1},\Sigma,\rho_{1},\Gamma_{1},L^{0}_{1},F_{1},\Delta_{1})$ and $M_{2}=(L_{2},\Pi,\rho_{2},\Gamma_{2},L^{0}_{2},F_{2},\Delta_{2})$ respectively. A homomorphism $h:\Sigma\mapsto\Pi$ is said to valid iff following conditions are satisfied

• •

$h$ preserves stack mapping $i.e.$ $a\in\Sigma^{i}_{c}$ iff $h(a)\in\Pi^{i}_{c}$, $b\in\Sigma^{i}_{r}$ iff $h(b)\in\Pi^{i}_{r}$ and $c\in\Sigma^{i}_{l}$ iff $h(c)\in\Pi^{i}_{l}$

• •

$h$ preserves event clock partition $i.e.$ $\rho_{1}(a)=\rho_{2}(h(a))$ for all $a\in\Sigma$.