Counter-queue automata with an application to a meaningful extension of ω-regular languages‹ David Barozzini1 , Dario Della Monica2,3 , Angelo Montanari1 , and Pietro Sala4 1 Dept. of Mathematics, Computer Science, and Physics, University of Udine, Italy dbaro13@gmail.com,angelo.montanari@uniud.it 2 Dept. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, Spain ddellamo@ucm.es 3 Dept. of Electrical Engineering and Information Technology, University “Federico II” of Napoli, Italy dario.dellamonica@unina.it 4 Dept. of Computer Science, University of Verona, Italy pietro.sala@univr.it Abstract. In this paper, we introduce a new class of automata over infinite words (counter-queue automata) and we prove the decidability of their emptiness problem. Then, we define an original extension of ω- regular languages, called ωT -regular languages, that captures meaningful languages that neither belong to the class of ω-regular languages nor to other extensions of it proposed in the literature, and we show that counter-queue automata are expressive enough to encode them. 1 Introduction In this paper, we introduce a new class of automata, called counter-queue automata (CQ automata for short), and we show that their emptiness problem is decidable in 2ETIME. CQ automata are finite state automata on ω-words, provided with a finite number of queues. Their acceptance condition imposes strong requirements on the contents and the management of queues in successful computations. In particular, infinitely many distinct numbers must be inserted in each queue and each of them must be removed and added back infinitely often. The proof of the decidability of the emptiness problem for CQ automata ben- efits from known results about multi-pushdown automata. It can be decomposed into four fundamental steps. We first show that, without loss of generality, we can restrict ourselves to a proper subclass of CQ automata with a simplified transition function (we call them simple CQ automata). Then, we introduce a new two-player game (CQ game) and we show that we can associate a CQ game with each simple CQ automaton. Next, we introduce the notion of winning witness and we prove that CQ games can be decided by checking the existence of winning witnesses. Finally, we show that the existence of such a witness can be verified by checking for emptiness a suitable multi-pushdown automaton. ‹ D. Della Monica acknowledges the financial support from a Marie Curie INdAM- COFUND-2012 Outgoing Fellowship. A. Montanari acknowledges the support from the Italian GNCS Project “Logics and Automata for Interval Model Checking”. As a matter of fact, the idea of CQ automata came to our mind during an investigation of possible extensions of regular languages of infinite words (ω-regular languages [8,9,11]). Recent work by Bojańczyk, Colcombet, and others made it clear that ω-regular languages can actually be extended in various ways, preserving their decidability and some of their closure properties [4,5,6]. As an example, ω-regular languages can be extended to allow one to constrain the distance between consecutive occurrences of a given symbol to be bounded, a promptness condition which turns out to be fairly natural in a number of application domains [1,10]. The proposed extensions of ω-regular languages pair the Kleene star p.q˚ with bounding/unbounding variants of it. In particular, the bounding exponent p.qB (aka B-constructor) constrains parts of the input word to be of bounded size, while the unbounding exponent p.qS (aka S-constructor) forces parts of the input word to be arbitrarily large. These two extensions have been studied both in isolation (ωB- and ωS-regular expressions) and in conjunction (ωBS-regular expressions) [6]. Among other things, it has been shown that the complement of an ωB-regular language is an ωS-regular one and vice versa; moreover, ωBS- regular languages, featuring B- and S-constructors, strictly extend both ωB- and ωS-regular languages and are not closed under complementation. Here, we focus on those ω-languages which are complements of ωBS-regular ones, but do not belong to the class of ωBS-regular languages. Starting with a paradigmatic example of one such language given in [6], we identify a meaningful extension of ω-regular languages, that includes such a language, which is obtained by adding a new, fairly natural constructor p.qT (named T -constructor) to the standard constructors of ω-regular expressions. Then, we show that CQ automata are expressive enough to capture the resulting class of ω-languages, called ωT - regular languages, by providing an encoding of ωT -regular expressions into them. The rest of the paper is organized as follows. In Section 2, we formally define CQ automata. Then, in Section 3 we prove that their emptiness problem is decidable in 2ETIME. Finally, in Section 4, we introduce the class of ωT -regular languages and provide their encoding into CQ automata. Conclusions give a short assessment of the work done and illustrate future research directions. 2 Counter-queue automata In this section, we introduce CQ automata; then, in the next section we will show that their emptiness problem is decidable. To start with, we introduce the notion of queue (of natural numbers) devoid of repetitions: a queue q is a finite word over N such that all of its elements are different. We denote the empty queue by H. Given a queue q, we denote by qris the i-th number in q. Moreover, we denote the set of the elements of q and the maximum among them by Setpqq and maxpqq, respectively. Formally, Setpqq “ tn P N : Di.qris “ nu and maxpqq “ maxpSetpqqq if Setpqq ‰ H, maxpqq “ ´1 otherwise. The first and the last element of q can be selected by means of the usual f ront and back operations: f rontpqq “ qr1s and backpqq “ qr|q|s if Setpqq ‰ H, q2 ∅ 0 0, 1 1, 0 c2 0 1 0 q1 ∅ 3 3, 2 3, 2 2, 3 c1 0 1 2 3 0 1 2 0 0 1 2 0 1 2 3 0 s0  s a s b s  s a s a s a s b s  s  s a s a s b s  s  s a s a s b s  s  s a s a s a s b s  s 1 1 3 2 2 2 2 i1 i1 i1 c1 4 c2 0 2 i1 2 i1 2 c1 4 i2 0 2 i1 2 i1 2 c1 4 c2 0 2 i1 2 i1 2 i1 2 c1 4 c2 0 Fig. 2. A prefix of a computation of the automaton in Figure 1. A configuration is characterised by a circle (state) and the rounded-corner rectangles above it (counter- queue configuration). For each i, with 1 ď i ď N “ 2, ci (resp., qi ) is one of its counter (resp., queue) components. f rontpqq “ backpqq “ ´1 otherwise. The enqueue operation has to satisfy the uniqueness constraint on the elements of q: for every n P N, enqueuepq, nq “ q ¨ n if n R Setpqq, enqueuepq, nq “ q otherwise. The dequeue operation is defined as usual: dequeuepqq “ qr2s . . . qr|q|s. We denote by Q the set of all queues. a A counter-queue automaton (CQ b automaton—see Fig. 1) is a quintuple s1 ε s3 A “ pS, Σ, s0 , N, ∆q, where S is a finite ε ε set of states, Σ is a finite alphabet, b, (1, check) s0 P S is the initial state, N is a natural s0 ε s2 number, and ∆ Ď S ˆ pΣ Y tuq ˆ S ˆ s4 pt1, . . . , N u ˆ tno op, inc, checkuq is a ε, (2, inc) a, (1, inc) ε, (2, check) transition relation such that, for each 1 ps, σ, s , pk, no opqq P ∆, it holds that k “ 1. Given a CQ automaton A “ pS, Σ, s0 , N, ∆q, a configuration of A is Fig. 1. An example of a CQ automaton. a pair c “ ps, Cq, where s P S and C P pN ˆ QqN is a counter-queue configuration. For i P t1, . . . , N u, we denote by Cris “ pni , qi q the i-th component of a counter- queue configuration C, where ni and qi are its counter and queue components, respectively. In the following, we will often refer to ni as counterpCrisq and to qi as queuepCrisq. Let A “ pS, Σ, s0 , N, ∆q. We define a ternary relation ÑA over pairs of configurations and symbols in Σ Y tu such that for all configuration pairs ps, Cq, ps1 , C 1 q and σ P Σ Y tu, ps, Cq ÑσA ps1 , C 1 q if, and only if, there exists δ “ ps, σ, s1 , pk, opqq P ∆ such that Crk 1 s “ C 1 rk 1 s for all k 1 ‰ k, and – if op “ no op, then Crks “ C 1 rks; – if op “ inc, then counterpC 1 rksq “ counterpCrksq ` 1 and queuepC 1 rksq “ queuepCrksq; – if op “ check, then counterpC 1 rksq “ 0; moreover, ‚ if counterpCrksq “ f rontpqueuepCrksqq, then queuepC 1 rksq “ enqueuepdequeuepqueuepCrksqq, counterpCrksqq; ‚ if counterpCrksq ‰ f rontpqueuepCrksqq, then queuepC 1 rksq “ enqueuepqueuepCrksq, counterpCrksqq. In such a case, we say that ps, Cq ÑσA ps1 , C 1 q via δ. Let Ñ˚A be the reflexive and transitive closure of ÑσA (where we abstract away symbols in Σ Y tu). The initial configuration of A is the pair ps0 , C0 q, where for each k P t1, . . . , N u we have C0 rks “ p0, Hq. A computation of A is an infinite sequence of configurations C “ ps0 , C0 qps1 , C1 q . . ., where, for all i P N, psi , Ci q ÑσAi psi`1 , Ci`1 q for some σi P Σ Y tu (see Figure 2). Given two configurations psi , Ci q and psj , Cj q in C, with i ď j, we say that psj , Cj q is -reachable from psi , Ci q, written psi , Ci q  Ñ˚ 1 A psj , Cj q, if psj 1 ´1 , Cj 1 ´1 q ÑA psj 1 , Cj 1 q for all j P ti ` 1, . . . , ju. Given a ω computation C of A and an ω-word w P Σ , we say that w is C-induced if there is an increasing function f : Nzt0u Ñ N such that: – ps0 , C0 q Ñ˚ A psf p1q , Cf p1q q, and wris – for all i ě 1, psf piq , Cf piq q ÑA psf piq`1 , Cf piq`1 q Ñ˚ A psf pi`1q , Cf pi`1q q. A computation C of A is accepting if and only if: (ac1) there exists a C-induced ω-word w; (ac2) for all k P t1, . . . , N u, limiÑ`8 |queuepCi rksq| “ `8; (ac3) for all k P t1, . . . , N u, i P N, and n P SetpqueuepCi rksqq, it holds that |ti1 P N | backpqueuepCi1 rksqq “ nu| “ `8. In such a case, we say that w is accepted by A. Notice that condition (ac2) forces the insertion of infinitely many (distinct) numbers in each queue and condition (ac3), together with condition (ac2), guarantees that each of them occurs, that is, is removed and added back, infinitely often. We denote by LpAq the set of all ω-words w P Σ ω that are accepted by A, and we say that A accepts the language LpAq. 3 Decidability of the emptiness problem for CQ automata We now prove that the emptiness problem for CQ automata is decidable in 2ETIME. The proof consists of four main steps: (i) we replace general CQ automata by simple ones; (ii) we associate a two-player game (CQ game) with each simple CQ automaton; (iii) we prove that CQ games can be decided by checking the existence of winning witnesses; (iv) we show that the latter condition can be verified by checking for emptiness a suitable multi-pushdown automaton. From CQ automata to simple CQ automata. W.l.o.g., from now on we restrict our attention to simple CQ automata. A CQ automaton A “ pS, Σ, s0 , N, ∆q is simple if, and only if, for each s P S either |tps, σ, s1 , pk, opqq P ∆u| “ 1 or op “ no op, k “ 1, and σ “  for all ps, σ, s1 , pk, opqq P ∆. Basically, a simple CQ automaton has two kinds of state: those in which it can fire exactly one action and those in which it makes a nondeterministic choice. Moreover, for all pairs of configurations ps, Cq, ps1 , C 1 q such that ps, Cq ÑσA ps1 , C 1 q, the transition δ P ∆ that has been fired in ps, Cq is uniquely determined by s and s1 . By exploiting -transitions, that is, transitions of the form ps, , s1 , pk, opqq, and by adding a suitable number of states, it can be easily shown that every CQ automaton A may be turned into a simple one A1 such that LpAq “ LpA1 q. The set of states of a simple CQ automaton can be partitioned in four subsets: piq the set of states s from which only one transition of the form ps, σ, s1 , pk, checkqq can be fired (checkk states); piiq the set of states s from which only one transition of the form ps, σ, s1 , pk, incqq can be fired (inck states); piiiq the set of states s from which only one transition of the form ps, σ, s1 , p1, no opqq, with σ ‰ , can be fired (sym states); pivq the set of states s from which possibly many transitions of the form ps, , s1 , p1, no opqq can be fired (choice states). Let A “ pS, Σ, s0 , N, ∆q be a (simple) CQ automaton. A partial compu- tation of A is a finite sequence P “ ps0 , C0 q . . . psn , Cn q such that, for all i P t0, . . . , n ´ 1u, psi , Ci q ÑσAi psi`1 , Ci`1 q, for some σi P Σ Y tu. If ps0 , C0 q is the initial configuration of A, then P is a prefix computation of A. We de- note by P artialA and P ref ixesA the sets of all partial computations and pre- fix computations of A, respectively. Clearly, P ref ixesA Ď P artialA . Given a prefix computation P “ ps0 , C0 q . . . psn , Cn q and a partial computation P 1 “ ps10 , C01 q . . . ps1m , Cm 1 q, we say that P can be extended with P 1 if, and only if, P “ P ¨ P “ ps0 , C0 q . . . psn , Cn qps10 , C01 q . . . ps1m , Cm 2 1 1 q is a prefix computation 2 (P is said to be an extension of P). Let A “ pS, Σ, s0 , N, ∆q and P “ ps0 , C0 q . . . psn , Cn q P P artialA . For all s P S, it holds that if psn , Cn q ÑσA ps, Cq, for some counter-queue configuration C and some σ P Σ Y tu, then C is uniquely determined by sn , s, and Cn , that 1 is, there is no C 1 ‰ C such that psn , Cn q ÑσA ps, C 1 q, for any σ 1 . From simple CQ automata to CQ games. We now associate a two-player game, called CQ game, with every CQ automaton A. The configurations of the game are the prefix computations of A. The initial configuration is the shortest (non- empty) prefix computation of A, namely, P0 “ ps0 , C0 q. Let i P N be the current round and Pi “ ps0 , C0 q . . . psn , Cn q be the current game configuration. The first player (Spoiler ) moves by choosing a priority pi P tcheckk , maxk |1 ď k ď N u Y tsymu; the second one (Duplicator ) replies with a partial computation Qi “ ps10 , C01 q . . . ps1m , Cm 1 q such that (i) Pi can be extended with Qi ; (ii) if pi “ checkk , for some k P t1, . . . , N u, then there is j P t0, . . . , m ´ 1u such that f rontpqueuepCj1 rksqq “ backpqueuepCj`1 1 rksqq; (iii) if pi “ maxk , for some 1 k P t1, . . . , N u, then there is j P t0, . . . , m´1u such that backpqueuepCj`1 rksqq ą 1 maxpqueuepCj rksqq; (iv) if pi “ sym, then there is j P t0, . . . , mu such that a non--transition can be fired from s1j . A play P` of a CQ game is a sequence of pairs pP0 , p0 qpP1 , p1 q . . ., where, at each round i P N, pi is Spoiler’s move and Pi`1 is the result of the extension of Pi with Duplicator’s move Qi . Given a play P`, we denote by P`pnq the finite prefix of P` of length n, and by P`rns the n-th element of P`. Let PlayA be the set of all possible finite prefixes of all possible plays of the CQ game on A. Duplicator wins a play of the CQ game if, and only if, the play is infinite, that is, she is able to reply to Spoiler’s move at every round. A strategy for Duplicator in the CQ game on A is a function str : PlayA Ñ P artialA . In a play P` “ pP0 , p0 qpP1 , p1 q . . ., Duplicator acts according to str if for all i P N, Pi`1 “ Pi ¨ strpP`piqq, that is, Pi`1 is the result of the extension of Pi with strpP`piqq. A strategy str for Duplicator is winning if, and only if, Duplicator wins every play in which she acts according to str. The proof of Lemma 1 below is straightforward, and thus omitted. Lemma 1. Let A be a CQ automaton. It holds that LpAq ‰ H if and only if there is a winning strategy for Duplicator in the CQ game on A. From CQ games to winning witnesses. We show now how to decide CQ games making use of the notion of winning witness. Definition 1 (winning witness). Let A “ pS, Σ, s0 , N, ∆q be a CQ automaton and P “ ps0 , C0 q . . . psn , Cn q P P ref ixesA . P is a winning witness if, and only if, there exist 2N ` 3 indexes begin ă b1 ă e1 ă . . . ă bN ă eN ă limit ă end such that 0 ď begin, end ď n, and the following conditions hold: 1. sbegin is a state from which a non--transition can be fired; 2. sbegin “ send and, for each k P t1, . . . , N u, sbk is an inck state, sbk “ sek , and sj is not a checkk state for any j with bk ď j ď ek ; 3. for each k P t1, . . . , N u, there is j, with eN ă j ă limit, such that sj is a checkk state; 4. let J “ tj | 0 ď j ď limit and sj is a checkk state for some ku; there exists a set of indexes J “ tbj , ej | j P Ju such that for all j P J, with sj a checkk state, (i) limit ă bj ă ej ă end, (ii) for all j 1 ‰ j, either ej ă bj 1 or ej 1 ă bj , (iii) sbj and sej are checkk states and there are no other checkk states between them, and (iv) there are exactly counterpCj rksq inck states between sbj and sej . Indexes begin, b1 , e1 , . . . , bN , eN , limit, and end are referred to as the milestones of a winning witness. A winning witness can be seen as a finite representation of a winning strategy, as stated by the following lemma, which links the existence of a winning strategy for Duplicator in the CQ game on A to the existence of a winning witness (the proof can be found in [3]). Lemma 2. Let A be a CQ automaton. Then, Duplicator has a winning strategy in the CQ game on A if and only if P ref ixesA contains a winning witness. From winning witnesses to multi-pushdown automata. Thanks to Lemma 1 and Lemma 2, deciding the emptiness problem for a CQ automaton A amounts to searching P ref ixesA for a winning witness. Since we restricted ourselves to simple CQ automata, we can safely identify elements of P ref ixesA with their sequence of states and thus, by slightly abusing the notation, we write, for instance, s0 s1 . . . sn P P ref ixesA for ps0 , C0 q . . . psn , Cn q P P ref ixesA . Given a CQ automaton A, let Lww pAq be the language of finite words over the alphabet S (the set of states of A) that are winning witnesses in P ref ixesA . It is easy to see that LpAq ‰ H if and only if Lww pAq ‰ H. In what follows, for a CQ automaton A we build a multi-pushdown automaton whose language is exactly Lww pAq. Since the emptiness problem for multi-pushdown automata is decidable, so is the one for CQ automata. Multi-pushdown automata generalize pushdown ones by featuring more than one stack [7]. At each transition, the automaton can write on any stack, possibly more than one, but it reads only from the first non-empty one. Formally, a multi- pushdown automaton (MPDA for short) is a tuple M “ xn, Q, Σ, Γ, δ, q0 , F, Z0 y, where n ě 1 is the number of stacks, Q is a finite set of states, Σ and Γ are finite alphabets, referred to as the input and the stack alphabet, respectively, δ Ď Q ˆ pΣ Y tεuq ˆ Γ ˆ Q ˆ pΓ ˚ qn is the transition relation, q0 P Q is the initial state, F Ď Q is the set of final states, and Z0 P Γ is the initial stack symbol. Let M “ xn, Q, Σ, Γ, δ, q0 , F, Z0 y be an MPDA. A configuration of M is a pn ` 2q-tuple xq, w, γ1 , . . . , γn y, where q P Q, w P Σ ˚ , and γi P Γ ˚ , for i P t1, . . . , nu. We define a binary relation $M over pairs of configurations as follows: xq, aw, ε, . . . , ε, Aγi , . . . , γn y $M xq 1 , w, α1 , . . . , αi´1 , αi γi , . . . , αn γn y if and only if pq, a, A, q 1 , pα1 , . . . , αn qq P δ. Intuitively, the automaton pops the first symbol from the first non-empty stack, reads the first letter of the (current) input word, moves from state q to state q 1 , and pushes strings α1 , . . . , αn in the stacks. We denote by $˚M the transitive closure of $M . A word w P Σ ˚ is accepted by M if, and only if, xq0 , w, ε, . . . , ε, Z0 y $˚M xq, ε, γ1 , . . . , γn y for some q P F . The language of M, denoted by LpMq, is the set of words accepted by M. From now on, we denote by σ the symbol (in Σ) read from the input word w and by γ the symbol (in Γ ) read from the stack. Moreover, unless we explicitly say the opposite, we assume that the symbol popped from the stack is immediately pushed back in. In particular, by saying “do nothing” we mean “push γ back in the same stack you read it from and do nothing else” (notice that this is possible because we will make use of an MPDA whose stacks store, to a large extent, disjoint subsets of symbols in Γ ). Theorem 1 ([2,7]). The emptiness problem for MPDA is 2ETIME-complete. Lemma 3 ([7]). Let L “ LpMq for some MPDA M and L1 be a regular language. Then, there exists an MPDA M1 such that LpM1 q “ L X L1 . W.l.o.g., in what follows we restrict our attention to winning witnesses for which the sets of indexes required by items 3 and 4 of Definition 1 are ordered. More precisely (we borrow the notation from Definition 1), we assume that piq there are N indexes c1 ă . . . ă cN , with eN ă c1 and cN ă limit, such that sck is a checkk state for each k P t1, . . . , N u (this requirement strengthens the one imposed by item 3 of Definition 1), and piiq for all j 1 , j 2 P J, with j 1 ă j 2 , such that sbj1 and sbj2 are, respectively, checkk1 and checkk2 states, it holds that bj 1 ă bj 2 if and only if k 1 ă k 2 (this requirement strengthens the one imposed by item 4 of Definition 1). Notice that if k 1 “ k 2 , then bj 2 ă bj 1 . It is easy to check that, given a CQ automaton A, P ref ixesA contains a winning witness, as specified by Definition 1, if and only if it contains a winning witness satisfying δ0 δ1 I1 IN C1 CN J1 JN δend q0 .. .. .. qend qF δbegin σ is an inck state ñ push Ik in stack k ` 1 δ0 σ is a checkk state ñ push Ck in stack k ` 1 δ1 do nothing else ñ do nothing δbegin σ “ s’ has a non--transition ñ push s’ in stack N ` 2 δend σ “ s’ and γ “ s’ ñ pop s’ Fig. 3. A graphical account of M̂ (part 1). the additional ordering properties above. Thus, Lemma 2 holds with the new definition of winning witness as well. Given a CQ automaton A, we build an MPDA M such that LpMq “ Lww pAq as follows. We first build an MPDA M̂, whose input alphabet is the set of states of A, which accepts winning witnesses. Unfortunately, such an automaton might also accept winning witnesses not belonging to P ref ixesA . However, since P ref ixesA is a regular language, thanks to Lemma 3, there exists an MPDA M such that LpMq “ LpM̂q X P ref ixesA “ Lww pAq. Let A “ pS, Σ, s0 , N, ∆q be a CQ automaton. M̂ “ xn, Q, ΣM̂ , Γ, δ, q0 , F, Z0 y is defined as follows. We set n “ N `2, ΣM̂ “ S, and Γ “ S YtIk , Ck uN k“1 YtZ0 u. The remaining components of M̂ are described in Figures 3 and 4. In particular, the transition relation δ forces the automaton to behave as follows (steps 1-5): 1. it nondeterministically guesses begin and it stores sbegin in the last stack in order to check, at a later stage, that sbegin “ send ; 2. for each k P t1, . . . , N u, it nondeterministically guesses bk and ek and it stores sbk in the first stack in order to check that sbk “ sek ; 3. it checks for the existence, after eN , of checkk states, for k “ 1, . . . , N , in the desired order; 4. until limit is reached, whenever it reads an inck (resp., checkk ) state for some k P t1, . . . , N u, it pushes Ik (resp., Ck ) in the pk ` 1q-th stack; 5. once limit is reached, it checks whether the stacks can be emptied, by popping Ik , when an inck state is read, and Ck , when a checkk state is read. ε δdeinc δ1 k ε δ0 δ0 zδcheckk δ0 zδcheckk δdecheck k δ1 J J q0 k q1 k b e 1 δinc k δinc k δcheckk δdecheck k δdecheckk I I q0 k q1 k q Ck J q2 k An Ik -block. A Ck -block. A Jk -block. δdeinck b ε δinc σ “ s’’ is an k inck state ñ push s’’ in stack 1, push Ik in stack k ` 1 δdecheck k σ “ ε and γ “ Ck ñ do nothing e δdecheckk σ is a checkk state and γ “ Ck ñ pop Ck δinc σ “ s’’ k and γ “ s’’ ñ pop s’’, push Ik in stack k ` 1 δ0 zδcheckk σ is neither an inck nor σ is an inck state ñ push Ik in stack k ` 1 a checkk state ñ do nothing 1 δcheckk σ is a checkk state ñ push Ck in stack k ` 1 δdecheck k σ is a checkk state and γ ‰ Ik ñ do nothing ε δdeinc k σ “ ε and γ “ Ik ñ pop Ik δdeinck σ is neither σ is an inck state and γ “ Ik ñ pop Ik an inck nor a checkk state ñ do nothing Fig. 4. A graphical account of M̂ (part 2): Ik -, Ck -, and Jk -blocks, for k P t1, . . . , N u. Figure 3 gives a high-level pictorial account of the behavior of the MPDA. Steps 1 and 4 above are easy to implement; steps 2, 3, and 5 are dealt with by separate modules, namely, I-, C-, and J -blocks, respectively (Figure 4). Transitions of M̂ are depicted by labeled edges, whose labels have the form δx , which denote sets of transitions. An explicit account of their intended meaning is given in the pictures. Transitions labeled with δbegin and δend (see Figure 3) force the automaton to behave exactly as described in step 1 above, while δ0 in both Figure 3 and Figure 4 captures the behavior described in step 4. Let us consider, for instance, the loop edge labeled with δ0 in Figure 3. It denotes the following transitions: – for each inck state σ of A, pq0 , σ, λi , q0 , p, . . . , , λi , , . . . , , Ik , , . . . , qq P δ, for i P t1, . . . , N u and λi P tIi , Ci u (we are assuming that i ă k; similar transitions exist for i ą k and i “ k); – for each checkk state σ of A, pq0 , σ, λi , q0 , p, . . . , , Ck λi , , . . . , qq P δ, for i P t1, . . . , N u and λi P tIi , Ci u (for the sake of completeness, we are assuming here, unlike the previous item, that i “ k; similar transitions exist for i ă k and i ą k); – for each state σ of A that is neither an inck nor a checkk state, pq0 , σ, λi , q0 , p, . . . , , λi , , . . . , qq P δ, for i P t1, . . . , N u and λi P tIi , Ci u. The internal structure of I-, C-, and J -blocks is depicted in Figure 4. An Ik -block, with k P t1, . . . , N u, is used to check whether there is a cycle that starts and ends at an inck state, and visits no checkk states. A Ck -block, with k P t1, . . . , N u, is used to verify whether there is a checkk state before limit. Finally, a Jk -block, with k P t1, . . . , N u, is used to check item 4 of Definition 1: first, it pops the increments that were not checked yet from stack k ` 1, and then it nondeterministically checks whether the condition can be satisfied by trying to empty stack k ` 1. Theorem 2. The emptiness problem for CQ automata is decidable in 2ETIME. 4 Encoding of ωT -regular languages into CQ automata In this section, we first introduce ωT -regular languages and then we show how to encode them into CQ automata. ωT -regular languages. A standard way to define ω-regular languages is via ω- regular expressions. An ω-word can be seen as the concatenation of a finite prefix, belonging to a regular language, and an infinite sequence of finite words (we call each of them an ω-iteration), also belonging to a regular language. We focus on ω- iterations consisting of finite sequences of symbols generated by an occurrence of the Kleene star operator p.q˚ , aka ˚-constructor, in the scope of the ω-constructor p.qω . As an example, the ω-regular expression pb ¨ a˚ qω generates the language of ω-words featuring an infinite sequence of finite words consisting of one b followed by a finite (possibly empty) sequence of a’s. Given an ω-regular expression E featuring an occurrence of the ˚-constructor (sub-expression R˚ ) in the scope of the ω-constructor and an ω-word w belonging to the language of E, we refer to the sequence of the sizes of the (maximal) blocks of consecutive iterations of R in the different ω-iterations as the (sequence of ) exponents of R in (the ω-iterations of ) w. As an example, the ω-word w “ bbabaabaaa . . . p“ ba0 ba1 ba2 ba3 . . .q, generated by pb ¨ a˚ qω , is characterized by the sequence of exponents 0, 1, 2, 3, . . .. A limitation of ω-regular languages is that there is no way to constrain the behaviour (in the limit) of such a sequence of exponents. Some extensions of ω-regular expressions have been proposed in the last decade to overcome this limitation (see, e.g., [6]). ωB-regular expressions are obtained from ω-regular ones by adding a variant of p.q˚ , called B-constructor and denoted by p.qB , to be used in the scope of p.qω . The B-constructor constrains the argument R of the expression RB to be repeated in each ω-iteration a number of times less than a given bound fixed for the whole ω-word (boundedness). As the bound may vary from word to word, the language is not ω-regular. Similarly, ωS- regular expressions are obtained from ω-regular ones by adding another variant of p.q˚ , called S-constructor and denoted by p.qS , to be used in the scope of p.qω . For every ωS-regular expression containing the sub-expression RS and every k ą 0, the S-constructor constrains the number of ω-iterations in which the argument R is repeated exactly k times to be finite. It follows that the sequence of exponents of R in ω-words that feature an infinite number of ω-iterations including a sequence of consecutive R’s generated by RS tends towards infinity (strong unboundedness). ωBS-regular expressions are built by using the operators of ω-regular expressions and both p.qB and p.qS . The class of ωBS-regular languages strictly includes the classes of ωB- and ωS-regular ones, as witnessed by the ωBS-regular language L “ paB ¨b`aS ¨bqω , which is neither ωB- nor ωS-regular (the constructor ` must not be thought of as performing the union of the two different (sub-)languages, but rather as a “shuffling operator” that mixes ω-iterations belonging to them), and it is not closed under complementation. A counter-example is given precisely by L, whose complement is not ωBS-regular. Here, we focus on a new variant of p.q˚ , that we call (strong) T -constructor and denote by p.qT , to be used in the scope of p.qω . An expression RT occurring (in the scope of p.qω ) in some ω-expression E forces two conditions on the ω-words w belonging to E: piq the sequence of exponents of R in w features an infinite number of distinct exponents, and piiq every exponent occurring in the sequence occurs infinitely often. Hence, the distinctive features of these ω-words is that they feature infinitely many exponents occurring infinitely often. It can be easily checked that the complement of L above can be defined as ppa˚ ¨ bq˚ ¨ aT ¨ bqω ` pa˚ ¨ b˚ q˚ ¨ aω , and thus it belongs to the class of ωT -regular languages. As for the relationship between ωBS- and ωT -regular languages, it is easy to devise an ωT -regular language whose complement is not ωBS-regular and, vice versa, an ωBS-regular language whose complement is not ωT -regular. Despite of that, we can say that the T -constructor somehow complements the B- and the S-constructor as, when paired with them, it makes it possible to define p.q˚ : for every BST -regular expression e, it indeed holds that e˚ “ eB ` eS ` eT (BST -regular expressions are obtained from BS-regular ones by enriching them with the T -constructor). The proof can be found in [3]. The class of ωT -regular languages is the class of languages defined by ωT - regular expressions, which are built on top of T -regular expressions, just as ω-regular expressions are built on top of regular ones. Let Σ be a finite, non- empty alphabet. A T -regular expression over Σ is defined by the grammar: e ::“ H | a | e ¨ e | e ` e | e˚ | eT , with a P Σ . T -regular expressions differ from standard regular ones for the presence of p.qT . Since p.qT constrains the behavior of the sequence of ω-iterations to the limit, it is not possible to simply define the semantics of T -regular expressions in terms of languages of (finite) words, and then to obtain ωT -regular languages through infinitely many, unrelated iterations of such words. We give their semantics in terms of languages of infinite sequences of finite words; suitable constraints are then imposed to such sequences to capture the intended meaning of p.qT . Let Lpeq be the language defined by an expression e. Moreover, let N be the set of natural numbers, Ną0 “ Nzt0u, and, given an infinite sequence u of finite words over Σ, let ui , with i P N` , be the i-th element of u. The semantics of T -regular expressions over Σ is defined as follows (hereafter we assume f p0q “ 1): – LpHq “ H; – for a P Σ, Lpaq is the infinite sequence of the one-letter word a tpa, a, a, . . .qu; – Lpe1 ¨ e2 q “ tw | @i.wi “ ui ¨ vi , u P Lpe1 q, v P Lpe2 qu; – Lpe1 ` e2 q “ tw | @i.wi P tui , vi u, u, v P Lpe1 q Y Lpe2 qu;5 – Lpe˚ q “ tpuf p0q u2 . . . uf p1q´1 , uf p1q . . . uf p2q´1 , . . .q | u P Lpeq and f : N Ñ Ną0 is an unbounded and nondecreasing functionu; – LpeT q “ tpuf p0q u2 . . . uf p1q´1 , uf p1q . . . uf p2q´1 , . . .q | u P Lpeq and f : N Ñ Ną0 is an unbounded and nondecreasing function such that piq @nDi.f pi ` 1q ´ f piq ą n, and piiq @n.rif Di.f pi ` 1q ´ f piq “ n, then @kDj ą k.f pj ` 1q ´ f pjq “ nsu. Given a sequence v “ puf p0q u2 . . . uf p1q´1 , uf p1q . . . uf p2q´1 , . . .q P top , with op P t˚, T u, we define ´ the sequence ¯ of exponents of t in v, denoted by N pvq, as the sequence f piq ´ f pi ´ 1q . While the semantics of p.q˚ does not iPNą0 impose any constraint on N pvq, the semantics of p.qT guarantees the existence of infinitely many distinct exponents in N pvq (item piq) and forces each exponent occurring at least once in N pvq to occur infinitely often (item piiq). The ω-constructor turns languages of infinite sequences of words into languages of infinite words. Let e be a T -regular expression. The semantics of p.qω is defined as: Lpeω q “ tw | w “ u1 u2 u3 . . . for some u P Lpequ. ωT -expressions are defined by the grammar: E ::“ E ` E | R ¨ E | eω , where R is a regular expression, e is a T -regular expression, and ` and ¨ respectively denote union and concatenation of word languages (formally, LpE1 ` E2 q “ LpE1 q Y LpE2 q and LpE1 ¨ E2 q “ tu ¨ v | u P LpE1 q, v P LpE2 qu).6 The mapping of ωT -regular languages into CQ automata. We now show how to map an ωT -regular expression E into a corresponding CQ automaton A such 5 Unlike the case of word languages, when applied to languages of word sequences, the operator ` does not return the union of the two argument languages. As an example, Lpaq Y Lpbq Ĺ Lpa ` bq, as witnessed by the word sequence pa, b, a, b, a, b, . . .q. In general, for all t1 , t2 , it holds that Lpt1 q Y Lpt2 q Ď Lpt1 ` t2 q. 6 Notice the abuse of notation with the previous definition of the operators ` and ¨ over languages of infinite word sequences. that LpAq “ LpEq. We build A in a compositional way: for each sub-expression E 1 of E, starting from the atomic ones, we introduce a set SE 1 of CQ automata; then, we show how to produce the set of automata for complex sub-expressions by suitably combining automata in the sets associated with their sub-expressions. Eventually, we obtain a set of automata for the ωT -regular expression E. A results from a suitable merge of the automata in such a set (due to lack of space, the proof of the following result is omitted; it can be found in [3]). Theorem 3. For every ωT -regular expression E, there exists a CQ automaton A such that LpAq “ LpEq. 5 Conclusions In this paper, we introduced and studied a new class of counter automata, called counter-queue automata (CQ automata), and we proved the decidability of their emptiness problem in 2ETIME. Then, we applied them to the analysis of extended ω-regular languages. We defined a new extension of ω-regular languages, called ωT -regular languages, that captures meaningful languages not belonging to the well-known class of ωBS-regular ones, and we provided an encoding of ωT -regular expressions into CQ automata. Whether or not ωT -regular languages are expressively complete with respect to CQ automata is an open problem. References 1. Alur, R., Henzinger, T.A.: Finitary fairness. ACM Trans. Program. Lang. Syst. 20(6), 1171–1194 (1998) 2. Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Developments in Language Theory. pp. 121–133 (2008) 3. Barozzini, D., Della Monica, D., Montanari, A., Sala, P.: Extending ω-regular languages with a strong T -constructor: ωT -regular languages and counter-queue automata, Research Report 2017/01, Dept. of Mathematics, Computer Science, and Physics, University of Udine, Italy 4. Bojańczyk, M.: A bounding quantifier. In: CSL. LNCS, vol. 3210, pp. 41–55 (2004) 5. Bojańczyk, M.: Weak MSO with the unbounding quantifier. Theory of Computing Systems 48(3), 554–576 (2011) 6. Bojańczyk, M., Colcombet, T.: Bounds in ω-regularity. In: LICS. pp. 285–296 (2006) 7. Breveglieri, L., Cherubini, A., Citrini, C., Crespi-Reghizzi, S.: Multi-push-down Languages and Grammars. Int. J. of Foundations of Computer Science 7(03), 253–291 (1996) 8. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the 1960 Int. Congress on Logic, Methodology and Philosophy of Science. pp. 1–11 (1962) 9. Elgot, C.C., Rabin, M.O.: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. J. Symb. Log. 31(2), 169–181 (1966) 10. Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods in System Design 34(2), 83–103 (2009) 11. McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9(5), 521–530 (1966)