=Paper=
{{Paper
|id=Vol-1949/ICTCSpaper01
|storemode=property
|title=Counter-queue Automata with an Application to a Meaningful Extension of
Omega-regular Languages
|pdfUrl=https://ceur-ws.org/Vol-1949/ICTCSpaper01.pdf
|volume=Vol-1949
|authors=David Barozzini,Dario Della Monica,Angelo Montanari,Pietro Sala
|dblpUrl=https://dblp.org/rec/conf/ictcs/BarozziniMMS17
}}
==Counter-queue Automata with an Application to a Meaningful Extension of
Omega-regular Languages==
https://ceur-ws.org/Vol-1949/ICTCSpaper01.pdf
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)