## Languages

D. Bhave^{1}, V. Dave^{1}, S. N. Krishna^{1}, R. Phawade^{1}, and A. Trivedi^{1,2}

1 IIT Bombay and^{2} CU Boulder

Abstract. Perfect languages—a term coined by Esparza, Ganty, and Majumdar—are the classes of languages that are closed under Boolean operations and enjoy decidable emptiness problem. Perfect languages form the basis for decidable automata-theoretic model-checking for the respective class of models. Regular languages and visibly pushdown languages are paradigmatic examples of perfect languages. Alur and Dill initiated the language-theoretic study of timed languages and introduced timed automata capturing a timed analog of regular languages. However, unlike their untimed counterparts, timed regular languages are not perfect.

Alur, Fix, and Henzinger later discovered a perfect subclass of timed languages recognized by event-clock automata. Since then, a number of perfect subclasses of timed context-free languages, such as event-clock visibly pushdown languages, have been proposed. There exist examples of perfect languages even beyond context-free languages:—La Torre, Madhusudan, and Parlato characterized first perfect class of context- sensitive languages via multistack visibly pushdown automata with an explicit bound on number of stages where in each stage at most one stack is used. In this paper we extend their work for timed languages by characterizing a perfect subclass of timed context-sensitive languages and provide a logical characterization for this class of timed languages.

### 1 Introduction

A classC of languages is calledperfect[9] if it is closed under Boolean operations and permits algorithmic emptiness-checking. Perfect languages are the key ingre- dient for the Vardi-Wolper recipe for automata-theoretic model-checking:—given a system specificationS and a system implementationMas languages inC, the model-checking involves deciding the emptiness of the language M ∩ ¬S ∈ C.

The class of (ω-)regular languages is a well-known class of perfect languages, while other classes of languages such as context-free languages (CFLs) or context- sensitive languages (CSLs) are, in general, not perfect. CFLs are not perfect since they are not closed under intersection and complementation, although emptiness is decidable.On the other hand, CSLs are closed under Boolean operations but emptiness, in general, is undecidable for CSLs [6].

Alur and Madhusudan [4] discovered a perfect subclass of CFLs, called visibly pushdown languages (VPLs), characterized byvisibly pushdown automata that operate over words that dictate the stack operations. This notion is formalized by

giving an explicit partition of the alphabet into three disjoint sets of call,return, andinternal 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 an internal symbol. This visibility enables closure of these automata under all of the Boolean operations, while retaining the decidable emptiness property. Building upon this work, La Torre, Madhusudan, and Parlato [10]

introduced a perfect class of CSLs, called multistack visibly pushdown languages (MVPLs), recognized by visibly pushdown automata with multiple stacks (and call-return symbols for each stack) where the number of switches between various stacks for popping-purposes is bounded.

Example 1. L={a^{n}b^{n} : n≥0}is a VPL withaas call andbas return symbol for
the unique stack, whereas L^{0}={a^{n}_{1}a^{m}_{2} b^{n}_{1}b^{m}_{2} : n, m≥0} is a MVPL considering
a_{i} andb_{i} as call and return symbols, respectively, for stack-i wherei∈ {1,2}.

Finally,L^{00}={a^{n}b^{n}c^{n} : n≥0} is neither VPL nor MVPL for any partition of
alphabets as call and respectively alphabets of various stacks.

In this paper we introduce a timed extension of this context-sensitive language and study language-theoretic properties of the class in [13]. We characterize a perfect subclass of timed context-sensitive languages and provide a logical characterization for this class of timed languages.

Quest for Perfect Timed Languages.Alur and Dill [2] initiated automata- theoretic study of timed languages and characterized the class of timed-regular languages as the languages defined by timed automata. Unlike untimed regular languages, Alur and Dill showed that timed regular languages are not perfect as they are not closed under complementation. However, the emptiness of timed automata is a decidable using a technique known as region-construction. To overcome the limitation of timed automata for model-checking, Alur, Fix, and Henzinger introduced a perfect class of timed languages called the event-clock automata [3] (ECA)that achieves the closure under Boolean operations by making clock resets visible—the reset of each clock variable is determined by a fixed class of events and hencevisible just by looking at the input word. The decidability of the emptiness for ECA follows from the decidability of regular timed languages.

Two of the well-known models for context-free timed languages include recur- sive timed automata (RTAs) [14] and dense-time pushdown automata (dtPDAs) [1].

RTAs generalize recursive state machines with clock variables, whiledtPDAs gen- eralize pushdown automata with clocks and stack with variable ages. In general, the emptiness problem for theRTAin undecidable, however [14] characterizes classes of RTA with decidable emptiness problem. However, without any further restrictions, such as event-clock or visible stack, the languages captured by these classes are not perfect, since they strictly generalize both timed regular languages and CFLs. Tang and Ogawa in [15] proposed a first perfect timed context-free lan- guage class characterized byevent-clock visibly pushdown automata (ECVPA) that generalized bothECAandVPA. For the proposed model they showed determiniz- ability as well as closure under Boolean operations, and proved the decidability of the emptiness problem. However, ECVPAs, unlike dtPDAs, do not support

l_{0}
start

l_{1} l_{2}

l3

l_{4} l_{5}

a, push^{1}($)

a, push^{1}(α)
b, push^{2}($)

b, push^{2}(β)

c,x_{a}≥1, pop^{1}(α)

c, pop^{1}($)∈[2,2]

c, pop^{1}(α)∈[0,2]

c, pop^{1}($)∈[2,2]

d, pop^{2}(β)

d, pop^{2}($)∈[4,4]

Fig. 1.Dense-time Multistack Visibly Pushdown Automata used in Example 2

pushing the clocks on the stack. We proposed [7] a generalization of ECVPA called dense-time visibly pushdown automata (dtVPA), that are strictly more expressive thanECVPAas they support stack with variable ages (like dtPDA) and showed thatdtVPAcharacterize a perfect timed context-free language.

Contributions.We study a class of timed context-sensitive languages called dense-time multistack visibly pushdown languages (dtMVPLs), characterized by dense-time visibly pushdown multistack automata (dtMVPA), that generalize MVPLs with multiple stacks with ages as shown in the following example.

Example 2. Consider the timed language whose untimed component is of the
form {a^{y}b^{z}c^{y}d^{z} |y, z ≥1} with the critical timing restrictions among various
symbols in the following manner. The firstc must appear after 1 time-unit of
last a, the firstd must appear within 3 time-unit after lastb, and finally the
lastb must appear within 2 time units of the beginning and lastdmust appear
precisely at 4 time unit. This language is accepted by adtMVPAwith two stacks
shown in Figure 1. Letaandc(bandd, resp.) be call and return symbols for the
first (second, resp.) stack. Stack alphabets for first stack isΓ^{1}={α,$}and for
second stack isΓ^{2}={β,$}. In the figure a clock xa measures the time since the
occurrence of lasta, while constraintspop(γ)∈Ichecks if the age of the popped
symbol is in a given intervalI. The correctness of the model is easy to verify.

In this paper we show dtMVPLs are closed under Boolean operations and enjoy decidable emptiness problem. Although, the emptiness problem for restrictions of context sensitive languages has been studied extensively [5,8,13,12,11], ours is the first attempt to formalize perfect dense-time context-sensitive languages.

We will also give a logical characterization of this class of languages. We believe that dtMVPLs provide an expressive yet decidable model-checking framework for concurrent time-critical software systems (See Appendix A for an example).

The paper is organized as follows. We begin by introducing dense-time visibly pushdown multistack automata in the next section. In Section 3 we show closure under Boolean operations for this model, followed by logical characterization in Section 4. Due to lack of space, the proof for the decidability of emptiness is deferred to the Appendix.

### 2 Dense-Time Visibly Pushdown Multistack Automata

We assume that the reader is comfortable with standard concepts from automata theory (such as context-free languages, pushdown automata, MSO logic), con- cepts from timed automata (such as clocks, event clocks, clock constraints, and valuations), and visibly pushdown automata. Due to space limitation, 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 [2,3,4].

A finite timed word over Σ is a sequence (a_{1}, t_{1}),(a_{2}, t_{2}), . . . ,(a_{n}, t_{n}) ∈
(Σ×R≥0)^{∗} such that t_{i} ≤ t_{i+1} for all 1 ≤ i ≤ n−1. Alternatively, we can
represent timed words as tuple (ha_{1}, . . . , a_{n}i,ht_{1}, . . . , t_{n}i). We use both of these
formats depending on technical convenience. We represent the set of finite timed
words overΣbyT Σ^{∗}. Before we introduce our model, we recall the definitions
of event-clock automata and visibly pushdown automata.

2.1 Preliminaries

Event-clock automata (ECA) [3] are a determinizable subclass of timed au- tomata [2] that for every action a∈Σ implicitly associate two clocks xa and ya, where the “recorder” clock xa records the time of the last occurrence of actiona, and the “predictor” clockya predicts the time of the next occurrence of actiona. Hence, event-clock automata do not permit explicit reset of clocks and it is implicitly governed by the input timed word. This property makesECA determinizable and closed under all Boolean operations.

Notice that since clock resets are “visible” in input timed word, the clock valuations after reading a prefix of the word is also determined by the timed word.

For example, for a timed wordw= (a_{1}, t_{1}),(a_{2}, t_{2}), . . . ,(a_{n}, t_{n}), the value of the
event clockxa at positionj istj−tiwhere iis the largest position precedingj
where an actionaoccurred. If noahas occurred before the jth position, then
the value of xa is undefined denoted by a special symbol`. Similarly, the value
of ya at positionj of wis undefined if symbola does not occur inw after the
jth position. Otherwise, it istk−tj wherekis the first occurrence ofaafter j.

We writeCfor the set of all event clocks and we useR^{`}>0for the setR>0∪ {`}.

Formally, the clock valuation after readingj-th prefix of the input timed word
w,ν_{j}^{w}:C7→R^{`}>0, is defined in the following way:ν_{j}^{w}(xq) =tj−ti if there exists
an 0≤i<j such that ai = q andak 6= q for all i<k<j, otherwise ν^{w}_{j}(xq) = `
(undefined). Similarly, ν_{j}^{w}(yq) =tm−tj if there isj<msuch that am=qand
a_{l} 6= q for all j<l<m, otherwise ν_{j}^{w}(y_{q}) =`. A clock constraint over C is a
boolean combination of constraints of the form z∼c wherez ∈C, c∈Nand

∼∈ {≤,≥}. Given a clock constraint z ∼c overC, we write ν_{i}^{w} |= (z ∼c) to
denote if ν_{j}^{w}(z)∼c. For any boolean combination ϕ, ν_{i}^{w}|=ϕis defined in an
obvious way: if ϕ=ϕ_{1}∧ϕ_{2}, thenν_{i}^{w}|=ϕiff ν_{i}^{w}|=ϕ_{1} andν_{i}^{w}|=ϕ_{2}. Likewise,
the other boolean combinations are defined.

Definition 3. An event clock automaton is a tuple A= (L, Σ, L^{0}, F, E)where
L is a set of finite locations,Σ is a finite alphabet,L^{0}∈L is the set of initial

locations, F∈Lis the set of final locations, and E is a finite set of edges of the
form(`, `^{0}, a, ϕ)where `, `^{0} are locations, a∈Σ, andϕ is a clock constraint.

The class of languages accepted by event-clock automata are closed under boolean operations with decidable emptiness property [3].

Visibly pushdown automata [4] are a determinizable subclass of pushdown automata that operate over words that dictate the stack operations. 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 4. A visibly pushdown alphabet is a tuple Σ=hΣc, Σr, Σintiwhere
Σ is partitioned into a callalphabetΣc, a return alphabetΣr, and an internal
alphabet Σint. A visibly pushdown automata(VPA)over Σ=hΣc, Σr, Σinti is a
tuple(L, Σ, Γ, L^{0}, δ, F)whereLis a finite set of locations including a setL^{0}⊆L
of initial locations,Γ is a finite stack alphabet with special end-of-stack symbol

⊥, ∆ ⊆ (L×Σc×L×(Γ\⊥))∪(L×Σr×Γ×L)∪(L×Σint×L) is the transition relation, and F⊆L is final locations.

The class of languages accepted by visibly pushdown automata are closed under boolean operations with decidable emptiness property [4].

2.2 Dense-Time Visibly Pushdown Multistack Automata(dtMVPA)
We introduce the dense-time visibly pushdown automata as an event-clock
automaton equipped with multiple (sayn≥1) timed stacks along with a visibly
pushdown alphabet Σ=hΣ_{c}^{h}, Σ_{r}^{h}, Σ_{int}^{h} i^{n}_{h=1} where Σ_{x}^{i} ∩Σ_{x}^{j} =∅ for i6=j, and
x∈ {c, r, int}. Due to space limitation and notational convenience, we assume
that the partitioning function is one-to-one, i.e. each symbola∈Σ^{h} has unique
recorderx_{a} and predictory_{a} clocks assigned to it. LetΓ^{h}be the stack alphabet
of theh-th stack. LetΓ =Sn

h=1Γ^{h} and letΣ^{h}=hΣ_{c}^{h}, Σ_{r}^{h}, Σ_{int}^{h} i. LetC_{Σ}h (or
ChwhenΣ^{h}is clear) be a finite set of event clocks. LetΦ(Ch) be the set ofclock
constraints overCh andI be the set of intervals.

Definition 5. A dense-time visibly pushdown multistack automata (dtMVPAs)
overhΣ_{c}^{h}, Σ_{r}^{h}, Σ_{int}^{h} i^{n}_{h=1} is a tuple (L, Σ, Γ, L^{0}, F, ∆=(∆^{h}_{c}∪∆^{h}_{r}∪∆^{h}_{int})^{n}_{h=1})where

– Lis a finite set of locations including a set L^{0}⊆Lof initial locations,
– Γ^{h} is the finite alphabet of thehth stack with special end-of-stack symbol⊥_{h},
– ∆^{h}_{c} ⊆(L×Σ_{c}^{h}×Φ(Ch)×L×(Γ^{h}\⊥h))is the set of call transitions,

– ∆^{h}_{r} ⊆(L×Σ_{r}^{h}×I×Γ^{h}×Φ(Ch)×L) is set of return transitions,
– ∆^{h}_{int}⊆(L×Σ_{int}^{h} ×Φ(Ch)×L) is set of internal transitions, and
– F⊆Lis the set of final locations.

Letw= (a0, t0), . . . ,(ae, te) be a timed word. A configuration of the dtMVPAis
a tuple (`, ν_{i}^{w},(((γ^{1}σ^{1}, age(γ^{1}σ^{1})), . . . ,(γ^{n}σ^{n}, age(γ^{n}σ^{n}))) where`is the current
location of thedtMVPA,ν_{i}^{w}gives the valuation of all the event clocks at position
i≤ |w|, γ^{h}σ^{h} ∈Γ^{h}(Γ^{h})^{∗} is the content of stack hwithγ^{h} being the topmost
symbol and σ^{h} is the string representing the stack content below γ^{h}, while
age(γ^{h}σ^{h}) is a sequence of real numbers encoding the ages of all the stack symbols
(the time elapsed since each of them was pushed on to the stack). We follow the
assumption thatage(⊥^{h}) =h`i(undefined). If for some stringσ^{h} ∈(Γ^{h})^{∗} we
have that age(σ^{h}) = ht_{1}, t_{2}, . . . , t_{g}iand for τ ∈ R≥0 we write age(σ^{h}) +τ for
the sequence ht_{1}+τ, t_{2}+τ, . . . , t_{g}+τi. For a sequenceσ^{h}=hγ^{h}_{1}, . . . , γ_{g}^{h}iand a
memberγ^{h} we writeγ^{h}::σ^{h} forhγ^{h}, γ_{1}^{h}, . . . , γ^{h}_{g}i.

A run of adtMVPA onw= (a0, t0), . . . ,(ae, te) is a sequence of configuratio-
ns (`0, ν_{0}^{w},(h⊥^{1}i,h`i), . . . ,(h⊥^{n}i,h`i)), (`1, ν_{1}^{w},((σ_{1}^{1}, age(σ_{1}^{1})), . . . ,(σ_{1}^{n}, age(σ_{1}^{n}))),
. . . ,(`e+1, ν_{e+1}^{w} ,(σ^{1}_{e+1}, age(σ^{1}_{e+1})), . . . ,(σ_{e+1}^{n} , age(σ_{e+1}^{n} )))) where`i∈L,`0∈L^{0},
σ^{h}_{i} ∈(Γ^{h}∪ {⊥^{h}})^{+}, and for eachi, 0≤i≤e, we have:

– Ifa_{i}∈Σ^{h}_{c}, then there is (`_{i}, a_{i}, ϕ, `_{i+1}, γ^{h})∈∆^{h}_{c} such thatν_{i}^{w}|=ϕ. The symbol
γ^{h} ∈ Γ^{h}\{⊥^{h}} is then pushed onto the stack h, and its age is initialized
to zero, i.e. (σ^{h}_{i+1}, age(σ^{h}_{i+1})) = (γ^{h} :: σ^{h}_{i},0 :: (age(σ^{h}_{i}) + (t_{i}−t_{i−1}))). All
symbols in all other stacks are unchanged, and age byt_{i}−t_{i−1}.

– Ifai∈Σ_{r}^{h}, then there is (`i, ai, I, γ^{h}, ϕ, `i+1)∈∆^{h}_{r} such thatν_{i}^{w}|=ϕ. Also,
σ_{i}^{h} = γ^{h} :: κ∈Γ^{h}(Γ^{h})^{∗} and age(γ^{h}) + (ti−t_{i−1}) ∈ I. The symbol γ^{h} is
popped from stackhobtainingσ_{i+1}^{h} =κandage(σ^{h}_{i+1}) =age(σ^{h}_{i})+(ti−ti−1).

However, ifγ^{h} = h⊥^{h}i, then γ^{h} is not popped. The contents of all other
stacks remains unchanged, and simply age by (ti−ti−1).

– Ifa_{i}∈Σ_{int}^{h} , then there is (`_{i}, a_{i}, ϕ, `_{i+1})∈∆^{h}_{int} such thatν^{w}_{i} ϕ. In this case
all stacks remain unchanged i.e.σ^{h}_{i}=σ_{i+1}^{h} , andage(σ_{i+1}^{h} )=age(σ_{i}^{h})+(ti−t_{i−1})
for all 1≤h≤n. All symbols in all stacks age byti−t_{i−1}.

A runρof a dtMVPAM is accepting if it terminates in a final location. A timed wordwis an accepting word if there is an accepting run ofM onw. The languageL(M) of adtMVPAM, is the set of all timed wordswaccepted byM.

A dtMVPA M = (L, Σ, Γ, L^{0}, F, ∆) is said to be deterministic if it has
exactly one start location, and for every configuration and input action ex-
actly one transition is enabled. Formally, we have the following conditions:

for every (`, a, φ_{1}, `^{0}, γ_{1}),(`, a, φ_{2}, `^{00}, γ_{2})∈ ∆^{h}_{c}, φ_{1}∧φ_{2} is unsatisfiable; for ev-
ery (`, a, I_{1}, γ, φ_{1}, `^{0}),(`, a, I_{2}, γ, φ_{2}, `^{00}) ∈∆^{h}_{r}, either φ_{1}∧φ_{2} is unsatisfiable or
I_{1}∩I_{2} = ∅; and for every (`, a, φ_{1}, `^{0}),(`, a, φ_{2}, `^{0}) ∈ ∆^{h}_{int}, φ_{1}∧φ_{2} is unsatis-
fiable. An ECMVPA is a dtMVPA where the stacks are untimed. A ECMVPA
(L, Σ, Γ, L^{0}, F, ∆) is andtMVPAifI= [0,+∞] for every (`, a, I, γ, φ, `^{0})∈∆^{h}_{r}.

LetΣ=hΣ_{c}^{h}, Σ_{r}^{h}, Σ_{int}^{h} i^{n}_{h=1}be a visibly pushdown alphabet. Acontext over
Σ^{h}=hΣ_{c}^{h}, Σ_{r}^{h}, Σ_{int}^{h} iis a timed word in (Σ^{h})^{∗}. The empty word εis a context.

For ease, we assume in this paper that any contexthas at least one symbol fromΣ.

Around overΣis a timed wordwoverΣof the formw1w2. . . wn such that each
whis a context overΣ^{h}. Ak-round overΣis a timed wordwthat can be obtained
as a concatenation ofkrounds overΣ. That is, w=u1u2. . . uk, where eachui

is a round. LetRound(Σ, k) denote the set of allk-round timed words overΣ.

For any fixedk, ak-rounddtMVPAoverΣ is a tupleA= (k, L, Σ, Γ, L^{0}, F, ∆)
whereM = (L, Σ, Γ, L^{0}, F, ∆) is adtMVPAoverΣ. The language accepted by
Ais L(A) =L(M)∩Round(Σ, k) and is calledk-round dense time multistack
visibly push down language. The class ofk-round dense time multistack visibly
push down languages is denotedk-dtMVPL. The setS

k≥1k-dtMVPL is denoted bd-dtMVPL, and is the class of dense time multistack visibly push down languages with a bounded number of rounds. We definek-ECMVPL andbd-ECMVPL in a similar fashion. Also, we writek-dtMVPAand k-ECMVPAto denotek-round dtMVPA andk-roundECMVPA. The key result of the paper is the following.

Theorem 6 (A Perfect Timed Context-Sensitive Language).The classes of languages accepted byk-dtMVPAand k-ECMVPAare perfect:— they are closed under Boolean operations with decidable emptiness problem.

We sketch key lemmas towards this proof in the following section. As an applica- tion of this theorem we show Monadic second-order logic characterization of the languages accepted by k-dtMVPAin Section 4.

### 3 Proof of Theorem 6

The closure under union and intersection for bothk-dtMVPAandk-ECMVPA is straightforward and is sketched in Appendix B. In order to show closure under complementation, the main hurdle is to show determinizability of these automata.

We sketch the key ideas required to get determinizability for k-ECMVPA in Section 3.1 and fork-dtMVPAin Section 3.2. The decidability of the emptiness problem fork-ECMVPAfollows as for everyk-ECMVPA, via region construction [3], one can get an untimed-bisimilark-MVPA, which has a decidable emptiness [13].

In Section 3.2 we show that for everyk-dtMVPAwe get an emptiness-preserving k-ECMVPA and hence this result in combination with previous remark yield decidability of emptiness fork-dtMVPA.

3.1 Determinizability of k-ECMVPA

For the determinizability proof the key observation is the since the words accepted byAis a catenation ofkrounds, and the stacks (or contexts) do not interfere with each other, thek-ECMVPAAcan be considered as a “composition” ofnECVPA A1, . . . , An, with stack of eachAi corresponds toi-th stack of thek-ECMVPA.A has to simulate thenECVPAs in a round robin fashion forkrounds.

Ifw∈L(A), thenw=u1u2. . . uk, and ui =ui1ui2. . . uin, whereuij is the
jth context in theith round. Starting in an initial location`11, control is passed
toA1, which runs on u11 and enters location `^{0}_{11} =`12. Let ν_{11}^{0} = ν12 be the
values of all clocks after processingu11. At this point of time, A2 runs on u12

starting in location`12, and so on, untilAn runs onu1n starting in location`1n.
Now first round is over, andu1 is processed.An ends in some location`^{0}_{1n}=`21.
NowA1 starts again in`21 and processesu21. The values of all recorders and

predictors change according to the time that elapsed during the simulation of A2, . . . , An. It must be noted that between two consecutive roundsiandi+ 1 of anyAj, none of the clocks pertaining toAj get reset; they only reflect the time that has elapsed since the last round ofAj. This continues forkrounds, untilukn

is processed.Aj processes in order,u1j, u2j, . . . , ukj over (Σ^{j})^{∗} for 1≤j≤n. In
roundi, 1≤i≤k, eachA_{j}, 1≤j≤n−1, starts in location `_{ij}, runs onu_{ij} and

“computes” a location`_{ij+1}. Similarly,A_{n} moves from roundito roundi+ 1, by
starting in `_{in}, runs onu_{in}and computes a location `_{i+11}. The (i+ 1)th round
begins in this location withA_{1}running onu_{i+11}. Thus, by stitching together the
locations needed to switch fromA_{j} toA_{j+1}, we can obtain a simulation ofA.

Let u_{ij} = (a^{1}_{j}, t^{1}_{ij}). . .(a^{last}_{j} , t^{last}_{ij} ), where t^{1}_{ij}, . . . , t^{last}_{ij} are the time stamps
on reading u_{ij}. Let κ_{j} =u_{1j}(#_{1}, t^{last}_{1j} )u_{2j}(#_{2}, t^{last}_{2j} ). . . u_{kj}(#_{k}, t^{last}_{kj} ). The new
symbols #_{i} help disambiguateA_{j} processing u_{1j}, . . . , u_{kj} inkrounds. We first
focus on each ECVPA Aj which processes u1j, u2j, . . . , ukj. Let cmax be the
maximum constant used in clock constraints of Σ^{j} in the ECMVPA A. Let
I ={[0,0],[0,1], . . . ,[cmax, cmax],[cmax,∞)} be a set of intervals. Acorrect
sequence of round switches forAj with respect toκj is a sequence of pairsVj=
P1jP2j. . . Pkj, wherePhj = ((`hj, Ihj), `^{0}_{hj}), 2≤h≤k,P1j = ((`1j, ν1j), `^{0}_{1j}) and
Ihj∈ I such that

1. Starting in `1j, with thejth stack containing ⊥j, and an initial valuation
ν1j of all recorders and predictors of Σ^{j}, the ECMVPA A processes u1j

and reaches some`^{0}_{1j} with stack contentσ2j and clock valuation ν_{1j}^{0} . The
processing of u_{2j} by A then starts at location`_{2j}, and a timet ∈I_{2j} has
elapsed between the processing ofu_{1j} andu_{2j}. Thus,Astarts processingu_{2j}
in (`_{2j}, ν_{2j}) whereν_{2j} is the valuation of all recorders and predictors updated
fromν_{1j}^{0} with respect tot. The stack content remains same asσ_{2j} when the
processing ofu_{2j} begins.

2. In general, starting in (`hj, νhj),h >1 with thejth stack containingσhj, and νhj obtained fromνh−1j by updating all recorders and predictors based on the time intervalIhj that records the time elapse between processing uhj−1

anduhj,Aprocessesuhjand reaches (`^{0}_{hj}, ν_{hj}^{0} ) with stack contentσh+1j. The
processing ofu_{h+1j} starts after timet∈I_{h+1} has elapsed since processing
u_{hj} in a location`_{h+1j}, and stack content beingσ_{h+1j}.

Lemma 7. (Round Switching Lemma forAj) LetA= (k, L, Σ, Γ, L^{0}, F, ∆) be
ak-ECMVPA. Let w=u1u2. . . uk withui =ui1ui2. . . uin,1≤i≤k. Then we
can construct a ECVPAAj overΣ^{j}∪ {#1, . . . ,#k} which reaches a locationVj

on readingκj iffVj is a correct sequence of round switches forAj.

Proof. Recall thatκj is defined by annotatingu1ju2j. . . ukj with new symbols
{#1, . . . ,#k}and appropriate time stamps. LetVj =P1j. . . Pkj be a correct se-
quence of round switches forAj. Given thek-ECMVPAA= (k, L, Σ, Γ, L^{0}, F, ∆)
withw, theECVPAAj is constructed by simulating the transitions ofAonΣ^{j} by
guessingVj in its initial location. The alphabet ofAj isΣ^{j}∪ {#1, . . . ,#n}, and
hence has event clocksxa, x#i,a∈Σ^{j}. WheneverAj reads the #i, the control lo-
cation as well as the valuation of all recorders and predictors are changed according

toPi+1j, 1≤i≤k−1. On reading #k,Aj enters the locationVjfrom its current
location`^{0}_{kj}. The locations ofAj areVj∪ {(i, `ij, Vj),(i, `ij, Vj,#),(i, `ij, Vj, a)|
1≤i≤k, `∈L, a∈Σ^{j}, V_{j} ∈((L×I)×L)^{k}},∪((L×I)×L)^{k}, I ∈ I. The set
of initial locations are {(1, `1j, Vj) | Vj ∈ ((L×I)×L)^{k}, I ∈ I}. Starting in
(1, `1j, Vj), Aj processes u1j. When the last symbol a of u1j is read, it enters
a location (1, `^{0}_{1j}, Vj, a). From this location, only #1 transitions are enabled.

On reading #1, we move from (1, `^{0}_{1j}, Vj, a) to a location (2, `2j, Vj,#), where
P2= ((`2j, I2j), `^{0}_{2j}) andP1= ((`1j, ν1j), `^{0}_{1j}), after checking no time elapse since
a(checkxa=0). This ensures that no time is spent in processing #1afteru1j. Now
Aj starts processingu2j starting in location (2, `2j, Vj,#). From (2, `2j, Vj,#),
on reading a symbola∈Σ^{j}, we check that the time elapse since #1lies in the
intervalI2j (checkx#_{1}∈I2j) as given byP2and so on. When roundkis reached,
Aj starts processing in some location (k, `kj, Vj,#), and reaches (k, `^{0}_{kj}, Vj, a).

When #k is read,Aj enters locationVj. The transitionsδ^{j} of Aj are given in
Appendix C. It is easy to see thatVj is reached byAj only when the guessedVj

in the initial location is a correct sequence of round switches forAj. ut
While eachVj talks about the correct sequence of round switches, 1≤j≤n,
the sequence V1V2. . . Vn is called a globally correct sequence iff we can stitch
together the individualVi’s to obtain a complete simulation ofAonwby moving
across contexts and rounds. For instance, consider Vj = P1jP2j. . . Pkj and
Vj+1 =P1j+1P2j+1. . . Pkj+1 for 1≤j ≤n−1. Recall thatPij = ((`ij, Iij), `^{0}_{ij})
and Pij+1 = ((`ij+1, Iij+1), `^{0}_{ij+1}) for 1 ≤ i ≤ k. The sequence V1V2. . . Vn is
globally correct iff`^{0}_{ij} =`ij+1, j≤n−1 and`^{0}_{in}=`i+11 for 1≤i≤k.

Lemma 8. Let w = u1u2. . . uk be a timed word in Round(Σ, k), with A =
(k, L, Σ, Γ, L^{0}, F, ∆)being a k-ECMVPAoverΣ, and letui=ui1ui2. . . uinand
κj be as defined above. Then w∈L(A) iff for 1≤j ≤n, there exists a correct
switching sequence V_{j} of theECVPAA_{j} for κ_{j} such that V_{1}V_{2}. . . V_{n} is a globally
correct sequence forA with`_{11}∈L^{0} and`^{0}_{kn}∈F.

Proof. The proof essentially shows how one can simulate Aby composing the Aj’s using a globally correct sequenceV1V2. . . Vn. The idea is to simulate each Aj one after the other, allowingAj+1to begin on uij+1 iff the location reached

`^{0}_{ij} at the end of uij byAj matches with`ij+1, the proposed starting location
ofAj+1 onuij+1. Lets construct a composition of A1, . . . , An which runs onw,
and acceptswiff there exists a globally correct sequenceV1V2. . . Vn. The initial
locations are of the form (p1, p2, . . . , pn,1,1), where the last two entries denote
the current round number and context number andp_{j} is an initial location ofA_{j}.
The transitions∆ of the composition are defined using the transitionsδ^{j} ofA_{j}.
In some chosen initial location, we first runA1 updating only the first entry
p1 of the tuple until u11 is completely read. The first entry of the tuple then
has the form p^{0}_{1} = (1, `^{0}_{11}, V1, a) where a is the last symbol of u11. When A1

reads #1, the current location in the composition is (p^{0}_{1}, p2, . . . , pn,1,1). In the
composition ofA1, . . . , An, since there are no #’s to be read, we start simulation
ofA2 onu12 from (p^{0}_{1}, p2, . . . , pn,1,1) iffp2is (2, `12, V2) such that the`^{0}_{11} inp1

is same as the`12 inp2. We then add the transition from (p^{0}_{1}, p2, . . . , pn,1,1) to
(p^{00}_{1} = (2, `21, V1, a), q, . . . , pn,1,2) where q is obtained from p2 by a transition
in A2 on the first symbol of u12. The a in p^{00}_{1} is the last symbol ofu11 taken
fromp^{0}_{1}= (1, `^{0}_{11}, V1, a), and the`21in p^{00}_{1} is obtained fromP21= ((`21, I21), `^{0}_{21})
of V1. We continue like this till we reach u1n, the last context in round 1,
and reach some location (s_{1}, s_{2}, . . . , s_{n−1}, p^{0}_{n},1,1) withs_{1}= (2, `_{21}, V_{1}, a_{1}), s_{2}=
(2, `_{22}, V_{2}, a_{2}), . . . , s_{n−1}= (2, `_{2}_{n−1}, V_{n−1}, a_{n−1}) andp^{0}_{n}= (1, `^{0}_{1n}, V_{n}, a_{n}).

Now, to start the second round, that is onu21, we allow the transition from
the above location iff`^{0}_{1n} =`21and ifxa_{1} ∈I21and we start simulatingA1again,
after updatingp^{0}_{n}, the context and round number. That is, we have the transition
(s1, . . . , sn−1, p^{0}_{n},1, n) on the first symbol ofu21 to (r, . . . , sn−1, sn,2,1) where
s_{n} = (2, `_{2}_{n}, V_{n}, a_{n}) iff `^{0}_{1n}=`_{21}andx_{a}_{1} ∈I_{21}. Also,r is obtained froms_{1}by
a transition of A_{1} on the first symbol ofu_{21}. The checkx_{a}_{1} ∈I_{21} is consistent
with the check ofx_{#}_{1} ∈I_{21}in A_{1}. From (r, . . . , s_{n−1}, s_{n},2,1), the processing of
u_{21}happens as inA_{1}, and we continue till we finish processing u_{2n}. The same
checks are repeated at the start of each fresh round.

It is clear that we have a run onwin the composition only when we have
a globally correct sequence. On completing u_{kn}, this would lead to a loca-
tion (V_{1}, . . . , V_{n−1}, V_{n}, k, n), each V_{j} obtained from the individual A_{j}. We de-
fine the accepting locations of the composition to be {(V_{1}, . . . , V_{n}) | P_{kn} =
(`^{0}_{kn},[0,∞)), `^{0}_{kn}∈F}. Clearly, whenever there is a run inAonw that ends up
in `^{0}_{kn}∈F, we have an accepting run onw in the composition. ut
The key idea of the determinization ofk-ECMVPAfollows from Lemma 8 and
the determinizability of ECVPA[15]. Details are given in Appendix D.

Theorem 9. k-ECMVPAs are determinizable.

3.2 Determinizability of k-dtMVPA

Given ak-dtMVPAM, we first construct (untiming construction) ak-ECMVPAM^{0}
and a morphismhsuch thatL(M) =h(L(M^{0})). We then use the determinizability
ofk-ECMVPA (Theorem 9) to obtain a deterministick-ECMVPAM^{00} such that
L(M^{0}) =L(M^{00}). We then show how to obtain ak-dtMVPADfromM^{00}preserving
the determinism of M^{00}such thatL(D) =h(L(M^{00})) =h(L(M^{0})) =L(M).

We give an intuition to the untiming construction, and give formal details
in Appendix E. Each time a symbol is pushed on to a stack (say stack i), we
guess its age (the time interval) at the time of popping the symbol. For instance,
in the dtMVPAM, while pushing a symbol aon a stack, if we guess that the
constraint checked at the time of the pop is< κforκ∈N, then in theECMVPA
M^{0}, we push in the stack i, the symbol (a, < κ, f irst) if this is the first symbol
for which the guessed age is< κ. If< κ has already been guessed as the age for
a symbol pushed earlier, then we push (a, < κ) onto the stacki. The guess <iκ
is remembered in the finite control of theECMVPAM^{0}. Thus, for each symbola
pushed in stackiof thedtMVPAM, we push in stackiof theECMVPAM^{0}, either
(a, < κ, f irst) or (a, < κ) and remember <i κin the finite control as a set of

obligations. This information<iκis retained in the finite control until popping
the symbol (a, < κ, f irst) from stacki. New symbols<iκare added as internal
symbols to theECMVPAM^{0}. The number of these symbols is finite since we have
finitely many stacks and there is a maximum constant used in age comparisons
of thedtMVPAM. After pushing (a, < κ, f irst) onto the stack i, we read the
internal symbol<_{i}κ, ensuring no time elapse since the last input symbol. Thus
the event clockx_{<}_{i}_{κ} is reset at the same time as pushing (a, < κ, f irst) on the
stack. While popping (a, < κ, f irst), we check that the value of the event clock
x_{<}_{i}_{κ} is less than κ. Constraints of the form > κ are handled similarly. Since
the nstacks do not interfere with each other, this construction (adding extra
symbols<_{i}κone per stack, retaining these symbols in the finite control until
popping (a, < κ, f irst) from stacki) can be done for all stacks, mimicking the
timed stack. Note that the language accepted by the dtMVPAM ish(L(M^{0})),
wherehis the morphism which erases symbols of the form<iκand>iκfrom
L(M^{0}). This gives anECMVPA preserving emptiness of the dtMVPA. We can
determinize theECMVPAM^{0} obtainingdet(M^{0}) using Theorem 9. It remains to
eliminate the transitions on the new symbols<iκand>iκfromdet(M^{0}) and
argue that the resulting machine stays deterministic and acceptsL(M).

Theorem 10. k-dtMVPAs have decidable emptiness and are determinizable.

### 4 Logical Characterization of k-dtMVPA

We consider a timed wordw= (a0, t0),(a1, t1), . . . ,(am, tm) over alphabet Σ=
hΣ^{i}_{c}, Σ_{int}^{i} , Σ_{r}^{i}i^{n}_{i=1} as a word structure over the universe U = {1,2, . . . ,|w|} of
positions in the timed word. The predicates in the word structure areQa(i) for
a∈Σwhich evaluates to true at positioniiffw[i] =a, wherew[i] denotes theith
position ofw. Following [10], we use the matching binary relation µj(i, k) which
evaluates to true iff theith position is a call and thekth position is its matching
return corresponding to thejth stack. We also introduce three predicatesC^{a},B^{a},
andθjcapturing the following relations. For an intervalI, the predicateC^{a}(i)∈I
evaluates to true on the word structure iffν^{w}_{i} (xa)∈Ifor recorder clock xa. For
an interval I, the predicate B^{a}(i)∈I evaluates to true on the word structure
iff ν_{i}^{w}(y_{a})∈I for predictor clock y_{a}. For an intervalI, the predicate θ_{j}(i)∈I
evaluates to true on the word structure iff w[i] ∈Σ_{r}^{j}, and there is somek < i
such thatµ_{j}(k, i) evaluates to true andt_{i}−t_{k} ∈I. The predicateθ_{j}(i) measures
the time elapse between positionk where a call was made on the stackj, and
positioni, its matching return. This time elapse is the age of the symbol pushed
on to the stack during the call at position k. Since position iis the matching
return, this symbol is popped at positioni; if the age lies in the intervalI, the
predicate evaluates to true. We define MSO(Σ), the MSO logic overΣ, as:

ϕ:=Qa(x)|x∈X|µj(x, y)|C^{a}(x)∈I|B^{a}(x)∈I|θj(x)∈I|¬ϕ|ϕ∨ϕ| ∃x.ϕ| ∃X.ϕ
wherea∈Σ,xa∈CΣ,xis a first order variable andX is a second order variable.

The models of a formula φ ∈ MSO(Σ) are timed words w over Σ. The semantics of this logic is standard where first order variables are interpreted

over positions of w and second order variables over subsets of positions. We
define the languageL(ϕ) of an MSO sentenceϕas the set of all words satisfying
ϕ. Words in Round(Σ, k), for some k rounds, can be captured by an MSO
formulaBdk(ψ). For instance ifk= 1, andnstacks, the formula∃x1.(Qa^{1}(x1)∧

∀y1(y1 ≤ x1 → Qa^{1}(y1))∧ ∃x2.(x1 < x2∧Qa^{2}(x2)∧ ∀y2(x1 < y2 < x2 →
Q_{a}2(y_{2}))∧. . .∧ ∃xn(x_{n−1}< x_{n}∧Q_{a}n(x_{n})∧last(x_{n})∧ ∀yn(x_{n−1}< y_{n}< x_{n}→
Q_{a}n(y_{n}))))), wherea^{i}∈Σ^{i} andlast(x) denotesxis the last position, captures a
round. This can be extended to capturek-round words. Conjuncting the formula
obtained from adtMVPAM withBd_{k}(ψ) accepts only those words which lie in
L(M)∩Round(Σ, k). Likewise, if one considers any MSO formulaζ=ϕ∧Bd_{k}(ψ),
it can be shown that thedtMVPAM constructed forζ will be ak-dtMVPA. The
two directions, dtMVPAto MSO, as well as MSO todtMVPAcan be handled
using standard techniques, and can be found in Appendix F.

Theorem 11. A languageL overΣ is accepted by an k-dtMVPAiff there is a MSO sentence ϕoverΣ such thatL(ϕ)∩Round(Σ, k) =L.

### References

1. Abdulla, P., Atig, M., Stenman, J.: Dense-timed pushdown automata. In: LICS.

pp. 35–44 (2012)

2. Alur, R., Dill, D.: A theory of timed automata. TCS 126, 183–235 (1994) 3. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: A determinizable class of

timed automata. TCS 211(1-2), 253–273 (1999)

4. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Symposium on Theory of Computing. pp. 202–211 (2004)

5. Atig, M.F.: Model-checking of ordered multi-pushdown automata. Logical Methods in Computer Science 8(3) (2012)

6. Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Zeitschrift f¨ur Phonetik, Sprachwissenschaft und Kommunika- tionsforschung 14, 143–172 (1961)

7. Bhave, D., Dave, V., Krishna, S., Phawade, R., Trivedi, A.: A logical characterization for dense-time visibly pushdown automata. In: LATA. pp. 89–101 (2016)

8. Czerwinski, W., Hofman, P., Lasota, S.: Reachability problem for weak multi- pushdown automata. In: CONCUR, LNCS, vol. 7454, pp. 53–68. Springer (2012) 9. Esparza, J., Ganty, P., Majumdar, R.: A perfect model for bounded verification. In:

LICS. pp. 285–294. IEEE Computer Society (2012)

10. La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS. pp. 161–170 (2007)

11. La Torre, S., Napoli, M., Parlato, G.: Scope-bounded pushdown languages. In: DLT, LNCS, vol. 8633, pp. 116–128. Springer International Publishing (2014)

12. La Torre, S., Napoli, M., Parlato, G.: A unifying approach for multistack pushdown automata. In: MFCS, LNCS, vol. 8634, pp. 377–389. Springer (2014)

13. Salvatore, L., Madhusudan, P., Parlato, G.: The language theory of bounded context-switching. In: LATIN. pp. 96–107 (2010)

14. Trivedi, A., Wojtczak, D.: Recursive timed automata. In: ATVA. LNCS, vol. 6252, pp. 306–324. Springer-Verlag (September 2010)

15. Van Tang, N., Ogawa, M.: Event-clock visibly pushdown automata. In: SOFSEM 2009, LNCS, vol. 5404, pp. 558–569. Springer (2009)

## Appendix

### A An Example of Concurrent Time-Critical Systems

In Android operating system every application has a main thread which is by default responsible for user interface (UI) management and hence can only be blocked for very short durations. If an application needs to perform blocking operations or asynchronous tasks which may block thread for longer durations, it forks additional threads. Android supports event-based architecture for UI management and inter-thread communication. Java class Looper implements incoming message queue and message processing loop which reads the next event in the queue and perform the corresponding action. Main thread maintains message queue for incoming messages using Looper. Other threads can send events likeMessageorRunnable(asynchronous function call) to the Main thread which are queued for processing. Additional threads may also useLooperand have their own incoming message queues.

We model such systems using an abstract event-based system architecture
following Maiya et al. ^{1}. In this architecture, multiple processes communicate
with each other using shared events and events are processed in the order of their
arrival. We assume that each process has constant sized queue to store incoming
events. Each process has event processing loop which reads next queued event
and invoke corresponding event handler function. Additionally, events cannot
remain pending in the queue for unbounded time. Theage of an event is the
time elapsed since an event is queued. When the age of an event exceeds some
predefined threshold, it is dropped from the incoming event queue. Such condition
is desirable to ensure responsiveness of interactive systems.

We propose formal modeling of such abstract multi-process event based
architecture usingdtMVPA. LetP ={P_{1}, P_{2}, . . . , P_{n}}be the set of processes that
communicate among themselves using a shared set of eventsE={e_{1}, e_{2}, . . . , e_{m}}.

Each process inP has its own fixed sized queue to store incoming events. LetQ_{i}
be the incoming event queue for processPi. Any process can send event to any
other process by enqueuing it into receiver’s incoming event queue. Each queued
instance of an event has associated age which increases at the rate of one unit
per unit time. Age is always initialized to zero. An event is dropped from the
queue when its age exceeds some predefined thresholdτ, which is assumed to be
the same for all events.

We now describedtMVPAmodel for the above architecture. We modelk-sized
event queues k-slot circular queues using finite automata control, where contents
of the queue are remembered in the location. Send and receive operations are
captured by introducing additional internal symbols as follows. We use symbol
S_{k}^{e}^{m}^{,i→j} to denote that the process Pi has sent event em to process Pj by
enqueuing it into Q_{j}’s k^{th} slot. Likewise, we use symbol R^{e}_{k}^{m}^{,i→j} to denote

1 Maiya, P., Gupta, R., Kanade, A., Majumdar, R.: Partial order reduction for event- driven multi-threaded programs. In: TACAS. Springer (2016)

F

B aF B a F

a B

a F a B

a

B

F a F B

a B a F a F B

F B

a B a

a F a B

a F a F a

a B

S0 S1

R0

S2

R0 R0

S1 S2

R1 S0

R1

S0

R2

S2

R1

S1

R2 R2

S0k S1k S2

R0k R1k R2

ProcessP1 ProcessP2

QueueQ2

0

1 2

Fig. 2.dtMVPAmodel for Example 12

that the processPj has received eventemfrom processPi by dequeuing it into
Qj’s k^{th} slot. Thus, symbols S_{k}^{e}^{m}^{,i→j} and R^{e}_{k}^{m}^{,i→j} always occur in the pair
along the run and the age of the evente_{m} at the time of dequeuing is the time
difference between global timestamps ofS^{e}_{k}^{m}^{,i→j} and its correspondingR^{e}_{k}^{m}^{,i→j}.
This model permits same event (but different instances)e_{m}to be enqueued more
than once. But different instances of e_{m} occupy different lots in the queue and
can be easily distinguished using their slot number. This is useful for modeling
applications where different instances of the same type of service requests need to
be distinguished. Although the stack is not used for modeling event queue, each
processPi has uses its own stack and is modeled usingdtVPA. Direct product
automaton of these processes and event queues yields desired dtMVPA.

Example 12. Assume we have only two processes P ={P1, P2} and one event
E={e}. We assume the queue sizek= 3. We use internal symbolsS_{i}^{e,1→2} and
R_{i}^{e,1→2} where i ∈ {0,1,2}, to capture send and receive operations. Figure A
illustrates event processing for events sent fromP1 toP2. For brevity we drop
superscript ^{e,1→2} from internal symbols for the further discussion. When P1

sends an event to P2, it is marked by occurrence of any one of symbols S0, S1

or S2. When P2 receives the event, one of the symbols R0, R1 or R2 occur.

Whenever an event is enqueued in thei^{th}slot of the event queue, the occurrence
a symbol Si models this fact. Similarly Ri denotes the fact that an event is
received fromi^{th}slot. Event queue of size three is implemented using stackless
event clock automaton. In figure A, automaton Q2 models the circular queue.

Each of location of Q2 pictorially shows three slot circular queue along with
queue contents. Legends are shown (in red) on the initial location describing
slot numbers and direction of enqueue. Marker F denotes the position of front
pointer from where event is dequeued. Marker B denotes the position of back
pointer. While enqueuing new event, B is first incremented and then new event
is stored. When dequeuing, front element of the queue is read and front pointer
is incremented. Here, processes P_{1} and P_{2} simply send and receive an event
respectively, but they can be any arbitrary dtVPA involving stack operations.

We add guard (not shown) y_{R}_{i} ≤τ? on transition labeledS_{i}. This captures the
requirement that no event waits for more thanτ time units in the queue.

### B Closure of k-dtMVPA under Boolean operators

Consider the same underlying alphabetΣ=hΣ_{c}^{i}, Σ_{r}^{i}, Σ_{int}^{i} i^{n}_{i=1}, for two dtMVPA
M1, M2 with stack alphabets Γ1 = Sn

i=1Γ_{1}^{i} and Γ2 = Sn

i=1Γ_{2}^{i} respectively.

Without loss of generality, assume the locations of M1, M2 to be disjoint. Union then follows simply by taking the union of the (initial and final) locations and transitions ofM1, M2.

For the intersection, we consider the product ofMl= (Ll, Σ, Γl, L^{0}_{l}, L^{f}_{l}, ∆l),
for l in {1,2}, where ∆l = (∆^{i}_{cl}∪∆^{i}_{rl}∪∆^{i}_{intl})^{n}_{i=1}, we construct the dtMVPA
M = (L, Σ, Γ, L^{0}, F, ∆) with initial locationsL^{0}={(l^{0}_{1}, l^{0}_{2})|l_{1}^{0}∈L^{0}_{1}andl_{2}^{0}∈L^{0}_{2}},
with final locationsF ={(f_{1}, f_{2})|f_{1}∈L^{f}_{1}, f_{2}∈L^{f}_{2}} and with stack alphabet
Γ =Sn

i=1(Γ_{1}^{i}×Γ_{2}^{i}), The transition function∆= (∆^{i}_{c}∪∆^{i}_{r}∪∆^{i}_{int})^{n}_{i=1}, is follows:

1. Fora∈Σ_{c}^{i}, transition ((q1, q2), a, ϕ1∧ϕ2,(q_{1}^{0}, q_{2}^{0}),(γ1, γ2))∈∆^{i}_{c}iff transition
(q1, a, ϕ1, q_{1}^{0}, γ1) is in∆^{i}_{c1}and transition (q2, a, ϕ2, q^{0}_{2}, γ2) is in∆^{i}_{c2}. The age
of (γ1, γ2) is initialized to 0. The push operations ofM1, M2 are synchronized.

2. For a∈Σ_{r}^{i}, transition ((q_{1}, q_{2}), a, I_{1}∧I_{2},(γ_{1}, γ_{2}), ϕ_{1}∧ϕ_{2},(q^{0}_{1}, q^{0}_{2}))∈∆^{i}_{r} iff
transition (q_{1}, a, I_{1}, γ_{1}, ϕ_{1}, q_{1}^{0}) is in∆^{i}_{r1} and transition (q_{2}, a, I_{2}, γ_{2}, ϕ_{2}, q_{2}^{0}) is
in∆^{i}_{r2}. Note that the age of (γ_{1}, γ_{2}) must satisfyI_{1}∧I_{2} for popping. The
pop operations ofM1, M2 are synchronized.

3. For a∈Σ_{intl}^{i} , transition ((q1, q2), a, ϕ1∧ϕ2,(q_{1}^{0}, q_{2}^{0}))∈∆^{i}_{l} iff (q1, a, ϕ1, q_{1}^{0})∈

∆^{i}_{int1} and (q2, a, ϕ2, q_{2}^{0})∈∆^{i}_{int2}.

It is easy to see that L(M) =L(M1)∩L(M2). We thus have By Theorem 6 closure under determinizability which gives us closure under complementation.

Lemma 13. The class of languages characterized byk-dtMVPAare closed under Boolean operators.

### C Details of Lemma 7: Round-Switching Lemma

Lemma 14. (Round Switching Lemma forAj) Let A= (k, L, Σ, Γ, L^{0}, F, ∆)be
ak-ECMVPA. Let w=u1u2. . . uk withui =ui1ui2. . . uin,1≤i≤k. Then we
can construct a ECVPAAj overΣ^{j}∪ {#1, . . . ,#k} which reaches a locationVj

on readingκj iffVj is a correct sequence of round switches forAj.