2 Dense-Time Visibly Pushdown Multistack Automata

Languages

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

1 IIT Bombay and² 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ⁿbⁿ : n≥0}is a VPL withaas call andbas return symbol for the unique stack, whereas L⁰={aⁿ₁a^m₂ bⁿ₁b^m₂ : 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⁰⁰={aⁿbⁿcⁿ : 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₀ start

l₁ l₂

l3

l₄ l₅

a, push¹($)

a, push¹(α) b, push²($)

b, push²(β)

c,x_a≥1, pop¹(α)

c, pop¹($)∈[2,2]

c, pop¹(α)∈[0,2]

c, pop¹($)∈[2,2]

d, pop²(β)

d, pop²($)∈[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^yb^zc^yd^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Γ¹={α,$}and for second stack isΓ²={β,$}. 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₁, t₁),(a₂, t₂), . . . ,(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₁, . . . , a_ni,ht₁, . . . , t_ni). 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₁, t₁),(a₂, t₂), . . . ,(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<sup>`</sup>>0for the setR>0∪ {`}.

Formally, the clock valuation after readingj-th prefix of the input timed word w,ν_j^w:C7→R<sup>`</sup>>0, is defined in the following way:ν<sub>j</sub><sup>w</sup>(xq) =tj−ti if there exists an 0≤i<j such that ai = q andak 6= q for all i<k<j, otherwise ν<sup>w</sup><sub>j</sub>(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 ϕ=ϕ₁∧ϕ₂, thenν_i^w|=ϕiff ν_i^w|=ϕ₁ andν_i^w|=ϕ₂. Likewise, the other boolean combinations are defined.

Definition 3. An event clock automaton is a tuple A= (L, Σ, L⁰, F, E)where L is a set of finite locations,Σ is a finite alphabet,L⁰∈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(`, `⁰, a, ϕ)where `, `⁰ 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⁰, δ, F)whereLis a finite set of locations including a setL⁰⊆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ⁿ_h=1 where Σ_xⁱ ∩Σ_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Γ^hbe 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Σ^his 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ⁿ_h=1 is a tuple (L, Σ, Γ, L⁰, F, ∆=(∆^h_c∪∆^h_r∪∆^h_int)ⁿ_h=1)where

– Lis a finite set of locations including a set L⁰⊆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 (`, ν<sub>i</sub><sup>w</sup>,(((γ<sup>1</sup>σ<sup>1</sup>, age(γ<sup>1</sup>σ<sup>1</sup>)), . . . ,(γ<sup>n</sup>σ<sup>n</sup>, age(γ<sup>n</sup>σ<sup>n</sup>))) where`is the current location of thedtMVPA,ν_i^wgives 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₁, t₂, . . . , t_giand for τ ∈ R≥0 we write age(σ^h) +τ for the sequence ht₁+τ, t₂+τ, . . . , t_g+τi. For a sequenceσ^h=hγ^h₁, . . . , γ_g^hiand a memberγ^h we writeγ^h::σ^h forhγ^h, γ₁^h, . . . , γ^h_gi.

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

– Ifa_i∈Σ^h_c, then there is (`<sub>i</sub>, a<sub>i</sub>, ϕ, `_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, γ<sup>h</sup>, ϕ, `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⊥^hi, 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 (`<sub>i</sub>, a<sub>i</sub>, ϕ, `_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⁰, 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, φ<sub>1</sub>, `⁰, γ₁),(`, a, φ<sub>2</sub>, `⁰⁰, γ₂)∈ ∆^h_c, φ₁∧φ₂ is unsatisfiable; for ev- ery (`, a, I<sub>1</sub>, γ, φ<sub>1</sub>, `⁰),(`, a, I<sub>2</sub>, γ, φ<sub>2</sub>, `⁰⁰) ∈∆^h_r, either φ₁∧φ₂ is unsatisfiable or I₁∩I₂ = ∅; and for every (`, a, φ<sub>1</sub>, `⁰),(`, a, φ<sub>2</sub>, `⁰) ∈ ∆^h_int, φ₁∧φ₂ is unsatis- fiable. An ECMVPA is a dtMVPA where the stacks are untimed. A ECMVPA (L, Σ, Γ, L⁰, F, ∆) is andtMVPAifI= [0,+∞] for every (`, a, I, γ, φ, `⁰)∈∆^h_r.

LetΣ=hΣ_c^h, Σ_r^h, Σ_int^h iⁿ_h=1be 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⁰, F, ∆) whereM = (L, Σ, Γ, L⁰, 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 `⁰₁₁ =`12. Let ν₁₁⁰ = ν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`<sup>0</sup><sub>1n</sub>=`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`<sub>ij+1</sub>. Similarly,A<sub>n</sub> moves from roundito roundi+ 1, by starting in `_in, runs onu_inand computes a location `_i+11. The (i+ 1)th round begins in this location withA₁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¹_j, t¹_ij). . .(a^last_j , t^last_ij ), where t¹_ij, . . . , t^last_ij are the time stamps on reading u_ij. Let κ_j =u_1j(#₁, t^last_1j )u_2j(#₂, 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), `⁰_hj), 2≤h≤k,P1j = ((`1j, ν1j), `⁰_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`<sup>0</sup><sub>1j</sub> with stack contentσ2j and clock valuation ν<sub>1j</sub><sup>0</sup> . The processing of u<sub>2j</sub> 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⁰ 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 (`<sup>0</sup><sub>hj</sub>, ν<sub>hj</sub><sup>0</sup> ) with stack contentσh+1j. The processing ofu<sub>h+1j</sub> starts after timet∈I<sub>h+1</sub> has elapsed since processing u<sub>hj</sub> in a location`_h+1j, and stack content beingσ_h+1j.

Lemma 7. (Round Switching Lemma forAj) LetA= (k, L, Σ, Γ, L⁰, 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⁰, 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`<sup>0</sup><sub>kj</sub>. The locations ofAj areVj∪ {(i, `ij, Vj),(i, `ij, Vj,#),(i, `ij, Vj, a)| 1≤i≤k, `∈L, a∈Σ<sup>j</sup>, V<sub>j</sub> ∈((L×I)×L)<sup>k</sup>},∪((L×I)×L)<sup>k</sup>, 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, `⁰_1j, Vj, a). From this location, only #1 transitions are enabled.

On reading #1, we move from (1, `<sup>0</sup><sub>1j</sub>, Vj, a) to a location (2, `2j, Vj,#), where P2= ((`2j, I2j), `⁰_2j) andP1= ((`1j, ν1j), `⁰_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#₁∈I2j) as given byP2and so on. When roundkis reached, Aj starts processing in some location (k, `kj, Vj,#), and reaches (k, `⁰_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), `⁰_ij) and Pij+1 = ((`ij+1, Iij+1), `⁰_ij+1) for 1 ≤ i ≤ k. The sequence V1V2. . . Vn is globally correct iff`<sup>0</sup><sub>ij</sub> =`ij+1, j≤n−1 and`<sup>0</sup><sub>in</sub>=`i+11 for 1≤i≤k.

Lemma 8. Let w = u1u2. . . uk be a timed word in Round(Σ, k), with A = (k, L, Σ, Γ, L⁰, 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₁V₂. . . V_n is a globally correct sequence forA with`<sub>11</sub>∈L<sup>0</sup> and`⁰_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

`<sup>0</sup><sub>ij</sub> 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⁰₁ = (1, `⁰₁₁, V1, a) where a is the last symbol of u11. When A1

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

is same as the`12 inp2. We then add the transition from (p<sup>0</sup><sub>1</sub>, p2, . . . , pn,1,1) to (p<sup>00</sup><sub>1</sub> = (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⁰⁰₁ is the last symbol ofu11 taken fromp⁰₁= (1, `<sup>0</sup><sub>11</sub>, V1, a), and the`21in p⁰⁰₁ is obtained fromP21= ((`21, I21), `⁰₂₁) of V1. We continue like this till we reach u1n, the last context in round 1, and reach some location (s₁, s₂, . . . , s_n−1, p⁰_n,1,1) withs₁= (2, `<sub>21</sub>, V<sub>1</sub>, a<sub>1</sub>), s<sub>2</sub>= (2, `₂₂, V₂, a₂), . . . , s_n−1= (2, `<sub>2n−1</sub>, V<sub>n−1</sub>, a<sub>n−1</sub>) andp<sup>0</sup><sub>n</sub>= (1, `⁰_1n, V_n, a_n).

Now, to start the second round, that is onu21, we allow the transition from the above location iff`<sup>0</sup><sub>1n</sub> =`21and ifxa₁ ∈I21and we start simulatingA1again, after updatingp⁰_n, the context and round number. That is, we have the transition (s1, . . . , sn−1, p⁰_n,1, n) on the first symbol ofu21 to (r, . . . , sn−1, sn,2,1) where s_n = (2, `<sub>2n</sub>, V<sub>n</sub>, a<sub>n</sub>) iff `⁰_1n=`₂₁andx_a1 ∈I₂₁. Also,r is obtained froms₁by a transition of A₁ on the first symbol ofu₂₁. The checkx_a1 ∈I₂₁ is consistent with the check ofx_#1 ∈I₂₁in A₁. From (r, . . . , s_n−1, s_n,2,1), the processing of u₂₁happens as inA₁, 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₁, . . . , 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₁, . . . , V_n) | P_kn = (`<sup>0</sup><sub>kn</sub>,[0,∞)), `⁰_kn∈F}. Clearly, whenever there is a run inAonw that ends up in `⁰_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⁰ and a morphismhsuch thatL(M) =h(L(M⁰)). We then use the determinizability ofk-ECMVPA (Theorem 9) to obtain a deterministick-ECMVPAM⁰⁰ such that L(M⁰) =L(M⁰⁰). We then show how to obtain ak-dtMVPADfromM⁰⁰preserving the determinism of M⁰⁰such thatL(D) =h(L(M⁰⁰)) =h(L(M⁰)) =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⁰, 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⁰. Thus, for each symbola pushed in stackiof thedtMVPAM, we push in stackiof theECMVPAM⁰, 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⁰. 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⁰)), wherehis the morphism which erases symbols of the form<iκand>iκfrom L(M⁰). This gives anECMVPA preserving emptiness of the dtMVPA. We can determinize theECMVPAM⁰ obtainingdet(M⁰) using Theorem 9. It remains to eliminate the transitions on the new symbols<iκand>iκfromdet(M⁰) 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Σⁱ_c, Σ_intⁱ , Σ_rⁱiⁿ_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¹(x1)∧

∀y1(y1 ≤ x1 → Qa¹(y1))∧ ∃x2.(x1 < x2∧Qa²(x2)∧ ∀y2(x1 < y2 < x2 → Q_a2(y₂))∧. . .∧ ∃xn(x_n−1< x_n∧Q_an(x_n)∧last(x_n)∧ ∀yn(x_n−1< y_n< x_n→ Q_an(y_n))))), whereaⁱ∈Σⁱ 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. ¹. 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₁, P₂, . . . , P_n}be the set of processes that communicate among themselves using a shared set of eventsE={e₁, e₂, . . . , 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^em,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^em,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_mto 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^thslot of the event queue, the occurrence a symbol Si models this fact. Similarly Ri denotes the fact that an event is received fromi^thslot. 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₁ and P₂ simply send and receive an event respectively, but they can be any arbitrary dtVPA involving stack operations.

We add guard (not shown) y_Ri ≤τ? 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ⁱ, Σ_rⁱ, Σ_intⁱ iⁿ_i=1, for two dtMVPA M1, M2 with stack alphabets Γ1 = Sn

i=1Γ₁ⁱ and Γ2 = Sn

i=1Γ₂ⁱ 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⁰_l, L^f_l, ∆l), for l in {1,2}, where ∆l = (∆ⁱ_cl∪∆ⁱ_rl∪∆ⁱ_intl)ⁿ_i=1, we construct the dtMVPA M = (L, Σ, Γ, L⁰, F, ∆) with initial locationsL⁰={(l⁰₁, l⁰₂)|l₁⁰∈L⁰₁andl₂⁰∈L⁰₂}, with final locationsF ={(f₁, f₂)|f₁∈L^f₁, f₂∈L^f₂} and with stack alphabet Γ =Sn

i=1(Γ₁ⁱ×Γ₂ⁱ), The transition function∆= (∆ⁱ_c∪∆ⁱ_r∪∆ⁱ_int)ⁿ_i=1, is follows:

1. Fora∈Σ_cⁱ, transition ((q1, q2), a, ϕ1∧ϕ2,(q₁⁰, q₂⁰),(γ1, γ2))∈∆ⁱ_ciff transition (q1, a, ϕ1, q₁⁰, γ1) is in∆ⁱ_c1and transition (q2, a, ϕ2, q⁰₂, γ2) is in∆ⁱ_c2. The age of (γ1, γ2) is initialized to 0. The push operations ofM1, M2 are synchronized.

2. For a∈Σ_rⁱ, transition ((q₁, q₂), a, I₁∧I₂,(γ₁, γ₂), ϕ₁∧ϕ₂,(q⁰₁, q⁰₂))∈∆ⁱ_r iff transition (q₁, a, I₁, γ₁, ϕ₁, q₁⁰) is in∆ⁱ_r1 and transition (q₂, a, I₂, γ₂, ϕ₂, q₂⁰) is in∆ⁱ_r2. Note that the age of (γ₁, γ₂) must satisfyI₁∧I₂ for popping. The pop operations ofM1, M2 are synchronized.

3. For a∈Σ_intlⁱ , transition ((q1, q2), a, ϕ1∧ϕ2,(q₁⁰, q₂⁰))∈∆ⁱ_l iff (q1, a, ϕ1, q₁⁰)∈

∆ⁱ_int1 and (q2, a, ϕ2, q₂⁰)∈∆ⁱ_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⁰, 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.