In this paper, we introduce a new class of automata over in nite words (counter-queue automata) and we prove the decidability of their emptiness problem. Then, we de ne 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.
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 nite state automata on !-words, provided with a nite number of queues. Their acceptance condition imposes strong requirements on the contents and the management of queues in successful computations. In particular, in nitely many distinct numbers must be inserted in each queue and each of them must be removed and added back in nitely often.
The proof of the decidability of the emptiness problem for CQ automata bene ts from known results about multi-pushdown automata. It can be decomposed into four fundamental steps. We rst show that, without loss of generality, we can restrict ourselves to a proper subclass of CQ automata with a simpli ed 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 veri ed by checking for emptiness a suitable multi-pushdown automaton.
As a matter of fact, the idea of CQ automata came to our mind during
an investigation of possible extensions of regular languages of in nite words
(!-regular languages [
The proposed extensions of !-regular languages pair the Kleene star p:q
with bounding/unbounding variants of it. In particular, the bounding exponent
: B (aka B-constructor) constrains parts of the input word to be of bounded
p q
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) [
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 [
The rest of the paper is organized as follows. In Section 2, we formally de ne 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
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 nite word over N such that all of its elements are di erent. 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 rst 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, 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 de ned as usual: dequeuepqq qr2s : : : qr|q|s. We denote by Q the set of all queues.
A counter-queue automaton (CQ a automaton|see Fig. 1) is a quintuple b sAet opfSs;tat;ess0,; N; isq,awhneriteeSailspahanbiette, ε s1 εε s3 sn0u mPbSeris, tahnedinitialSstatpe, NYits auqnatuSral s0 ε s2 b, (1, chesc4k) pt1; : : : ; N u tno op; inc; checkuq is a ε, (2, inc) transition relation such that, for each a, (1, inc) ε, (2, check) ps; ; s1; pk; no opqq P , it holds that k 1. Given a CQ automaton A pS; ; s0; N; q, a con guration 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 con guration. For i P t1; : : : ; N u, we denote by Cris pni; qiq the i-th component of a counterqueue con guration 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 de ne a ternary relation ÑA over pairs of con gurations and symbols in Y t u such that for all con guration pairs ps; Cq; ps1; C1q and P Y t u, ps; Cq ÑACps1r1k;C1s 1fqorif,alalnkd1 only if, there exists ps; ; s1; pk; opqq P such that Crk1s k, and { if op no op, then Crks C1rks; { if op inc, then counterpC1rksq counterpCrksq 1 and queuepC1rksq queuepCrksq; { if op check, then counterpC1rksq 0; moreover, if counterpCrksq f rontpqueuepCrksqq, then queuepC1rksq enqueuepdequeuepqueuepCrksqq; counterpCrksqq; if counterpCrksq f rontpqueuepCrksqq, then queuepC1rksq enqueuepqueuepCrksq; counterpCrksqq.
In such a case, we say that ps; Cq ÑA ps1; C1q via . Let ÑA be the re exive and transitive closure of ÑA (where we abstract away symbols in Y t u). The initial con guration of A is the pair ps0; C0q, where for each k P t1; : : : ; N u we have C0rks p0; Hq. A computation of A is an in nite sequence of con gurations C ps0; C0qps1; C1q : : :, where, for all i P N, psi; Ciq ÑAi psi 1; Ci 1q for some i P Y t u (see Figure 2). Given two con gurations psi; Ciq and psj ; Cj q in C, with i ¤ j, we say that psj ; Cj q is -reachable from psi; Ciq, written psi; Ciq ÑA psj ; Cj q, if psj1 1; Cj1 1q ÑA psj1 ; Cj1 q for all j1 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; C0q ÑA psfp1q; Cfp1qq, and
wris psfpiq 1; Cfpiq 1q ÑA psfpi 1q; Cfpi 1qq.
{ for all i ¥ 1, psfpiq; Cfpiqq ÑA 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 |queuepCirksq| 8; (ac3) for all k P t1; : : : ; N u, i P N, and n P SetpqueuepCirksqq, 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 in nitely 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, in nitely 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
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 veri ed 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 re exactly one action and those in which it makes a nondeterministic choice. Moreover, for all pairs of con gurations ps; Cq; ps1; C1q such that ps; Cq ÑA ps1; C1q, the transition P that has been red 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 LpA1q.
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 red (checkk states); piiq the set of states s from which only one transition of the form ps; ; s1; pk; incqq can be red (inck states); piiiq the set of states s from which only one transition of the form ps; ; s1; p1; no opqq, with , can be red (sym states); pivq the set of states s from which possibly many transitions of the form ps; ; s1; p1; no opqq can be red (choice states).
Let A pS; ; s0; N; q be a (simple) CQ automaton. A partial computation of A is a nite sequence P ps0; C0q : : : psn; Cnq such that, for all i P t0; : : : ; n 1u, psi; Ciq ÑAi psi 1; Ci 1q, for some i P Y t u. If ps0; C0q is the initial con guration of A, then P is a pre x computation of A. We denote by P artialA and P ref ixesA the sets of all partial computations and prex computations of A, respectively. Clearly, P ref ixesA P artialA. Given a pre x computation P ps0; C0q : : : psn; Cnq and a partial computation P1 ps10; C01q : : : ps1m; Cm1q, we say that P can be extended with P1 if, and only if, P2 P P1 ps0; C0q : : : psn; Cnqps10; C01q : : : ps1m; Cm1q is a pre x computation (P2 is said to be an extension of P).
Let A pS; ; s0; N; q and P ps0; C0q : : : psn; Cnq P P artialA. For all s P S, it holds that if psn; Cnq ÑA ps; Cq, for some counter-queue con guration C and some P Y t u, then C is uniquely determined by sn, s, and Cn, that is, there is no C1 C such that psn; Cnq ÑA1 ps; C1q, 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 con gurations of the game are the pre x computations of A. The initial con guration is the shortest (nonempty) pre x computation of A, namely, P0 ps0; C0q. Let i P N be the current round and Pi ps0; C0q : : : psn; Cnq be the current game con guration. The rst 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; C01q : : : ps1m; Cm1q 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 backpqueuepCj1 1rksqq; (iii) if pi maxk, for some k P t1; : : : ; N u, then there is j P t0; : : : ; m 1u such that backpqueuepCj1 1rksqq ¡ maxpqueuepCj1 rksqq; (iv) if pi sym, then there is j P t0; : : : ; mu such that a non- -transition can be red from s1j.
A play P` of a CQ game is a sequence of pairs pP0; p0qpP1; p1q : : :, 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 nite pre x of P` of length n, and by P`rns the n-th element of P`. Let PlayA be the set of all possible nite pre xes 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 in nite, 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; p0qpP1; p1q : : :, 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.
De nition 1 (winning witness). Let A pS; ; s0; N; q be a CQ automaton and P ps0; C0q : : : psn; Cnq 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 red; 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 J u such that for all j P J , with sj a checkk state, (i) limit bj ej end, (ii) for all j1 j, either ej bj1 or ej1 bj, (iii) sbj and sej are checkk states and there are no other checkk states between them, and (iv) there are exactly counterpCjrksq 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 nite 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 [
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, s0s1 : : : sn P P ref ixesA for ps0; C0q : : : psn; Cnq P P ref ixesA. Given a CQ automaton A, let LwwpAq be the language of nite 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 LwwpAq H. In what follows, for a CQ automaton A we build a multi-pushdown automaton whose language is exactly LwwpAq. 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 [
Let M xn; Q; ; ; ; q0; F; Z0y be an MPDA. A con guration of M is a pn 2q-tuple xq; w; 1; : : : ; ny, where q P Q, w P , and i P , for i P t1; : : : ; nu. We de ne a binary relation $M over pairs of con gurations as follows: xq; aw; "; : : : ; "; A i; : : : ; ny $M xq1; w; 1; : : : ; i 1; i i; : : : ; n ny if and only if pq; a; A; q1; p 1; : : : ; nqq P . Intuitively, the automaton pops the rst symbol from the rst non-empty stack, reads the rst letter of the (current) input word, moves from state q to state q1, 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; "; : : : ; "; Z0y $M xq; "; 1; : : : ; ny 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 ([
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 De nition 1 are ordered. More precisely (we borrow the notation from De nition 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 De nition 1), and piiq for all j1; j2 P J , with j1 j2, such that sbj1 and sbj2 are, respectively, checkk1 and checkk2 states, it holds that bj1 bj2 if and only if k1 k2 (this requirement strengthens the one imposed by item 4 of De nition 1). Notice that if k1 k2, then bj2 bj1 . It is easy to check that, given a CQ automaton A, P ref ixesA contains a winning witness, as speci ed by De nition 1, if and only if it contains a winning witness satisfying q0 0 begin ::
:: I1
IN
C1
CN
J1 ::
JN
1 qend end qF 0 isisaacnheinckckk sstteaalstteee ñññ dppouussnhhoICthkkiniingnssttaacckkkk 11 1 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 de nition of winning witness as well.
Given a CQ automaton A, we build an MPDA M such that LpMq LwwpAq as follows. We rst 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 LwwpAq. is deLenteAd as pfoSl;low;ss.0W;Ne ;setqnbe aNCQ2a,utoM^matoSn,.aMn^d xn;SQY; tIMk^;;Ck;ukN;q01;YFt;ZZ00uy. 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 rst 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.
0 qIk 0 b inck 0z checkk qIk 1 e inck
0z checkk
qCk A Ck-block. b push s'' in stack 1, inck incsk''sitsataen ñ push Ik in stack k 1 ienck and s''s'' ñ push Ikpoinp ss't'a,ck k 1 checkk " decheckk d"einck qJk d"echeckk qJk 0 1 d1echeckk qJk 2
1
1 decheckk deinck " and
Ck ñ do nothing decheckk is a checkk state and
Ck ñ pop Ck 0z checkk
is an inck state ñ push Ik in stack k 1 is neither an inck nor a checkk state ñ do nothing checkk is a checkk state ñ push Ck in stack k 1 d1echeckk is a checkk state ñ do nothing and Ik " deinck " and
Ik ñ pop Ik deinck is neither an inck nor a checkk staItke ññ pdoopnoIkthing is an inck state and
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; Ciu (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; Ciu (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; Ciu.
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 De nition 1: rst, it pops the increments that were not checked yet from stack k 1, and then it nondeterministically checks whether the condition can be satis ed by trying to empty stack k 1.
Theorem 2. The emptiness problem for CQ automata is decidable in 2ETIME. 4
In this section, we rst introduce !T -regular languages and then we show how to encode them into CQ automata. !T -regular languages. A standard way to de ne !-regular languages is via !regular expressions. An !-word can be seen as the concatenation of a nite pre x, belonging to a regular language, and an in nite sequence of nite words (we call each of them an !-iteration), also belonging to a regular language. We focus on !iterations consisting of nite 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 in nite sequence of nite words consisting of one b followed by a nite (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 di erent !-iterations as the (sequence of ) exponents of R in (the !-iterations of ) w. As an example, the !-word w bbabaabaaa : : : p ba0ba1ba2ba3 : : :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., [
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 in nite number of distinct exponents, and piiq every exponent occurring
in the sequence occurs in nitely often. Hence, the distinctive features of these
!-words is that they feature in nitely many exponents occurring in nitely often.
It can be easily checked that the complement of L above can be de ned 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
Band the S-constructor as, when paired with them, it makes it possible to de ne
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 [
The class of !T -regular languages is the class of languages de ned 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 nite, nonempty alphabet. A T -regular expression over is de ned by the grammar: e :: H | a | e e | e e | e | eT ; with a P . T -regular expressions di er 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 de ne the semantics of T -regular expressions in terms of languages of ( nite) words, and then to obtain !T -regular languages through in nitely many, unrelated iterations of such words. We give their semantics in terms of languages of in nite sequences of nite words; suitable constraints are then imposed to such sequences to capture the intended meaning of p:qT .
Let Lpeq be the language de ned by an expression e. Moreover, let N be the set of natural numbers, N¡0 Nzt0u, and, given an in nite sequence u of nite words over , let ui, with i P N , be the i-th element of u. The semantics of T -regular expressions over is de ned as follows (hereafter we assume f p0q 1): { LpHq H; { for a P , Lpaq is the in nite sequence of the one-letter word a tpa; a; a; : : :qu; { Lpe1 e2q tw | @i:wi ui vi; u P Lpe1q; v P Lpe2qu; { Lpe1 e2q tw | @i:wi P tui; viu; u; v P Lpe1q Y Lpe2qu;5 { Lpe q tpufp0qu2 : : : ufp1q 1; ufp1q : : : ufp2q 1; : : :q | u P Lpeq and f : N Ñ N¡0 is an unbounded and nondecreasing functionu; { LpeT q tpufp0qu2 : : : ufp1q 1; ufp1q : : : ufp2q 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 pufp0qu2 : : : ufp1q 1; ufp1q : : : ufp2q 1; : : :q P top, with op P t ; T u, we de ne the sequence of exponents of t in v, denoted by N pvq, as the sequence f piq f pi 1 . While the semantics of p:q does not q iPN¡0 impose any constraint on N pvq, the semantics of p:qT guarantees the existence of in nitely many distinct exponents in N pvq (item piq) and forces each exponent occurring at least once in N pvq to occur in nitely often (item piiq).
The !-constructor turns languages of in nite sequences of words into languages
of in nite words. Let e be a T -regular expression. The semantics of p:q! is
de ned as: Lpe!q tw | w u1u2u3 : : : for some u P Lpequ. !T -expressions are
de ned 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 E2q LpE1q Y LpE2q
and LpE1 E2q tu v | u P LpE1q; v P LpE2qu).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 Lpt1q Y Lpt2q Lpt1 t2q.
6 Notice the abuse of notation with the previous de nition of the operators and
over languages of in nite word sequences.
that LpAq LpEq. We build A in a compositional way: for each sub-expression
E1 of E, starting from the atomic ones, we introduce a set SE1 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 [
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 de ned 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.