=Paper=
{{Paper
|id=Vol-3072/paper6
|storemode=property
|title=Extended ω-Regular Languages and Interval Temporal Logic
|pdfUrl=https://ceur-ws.org/Vol-3072/paper6.pdf
|volume=Vol-3072
|authors=Dario Della Monica,Angelo Montanari,Pietro Sala
|dblpUrl=https://dblp.org/rec/conf/ictcs/MonicaMS21
}}
==Extended ω-Regular Languages and Interval Temporal Logic
==
https://ceur-ws.org/Vol-3072/paper6.pdf
Extended ω-Regular Languages
and Interval Temporal Logic? ??
Dario Della Monica1 , Angelo Montanari1 , and Pietro Sala2
1
University of Udine, Italy {dario.dellamonica|angelo.montanari}@uniud.it
2
University of Verona, Italy pietro.sala@univr.it
Abstract. Some extensions of ω-regular languages have been proposed
in the literature to express asymptotic properties of ω-words which are
not captured by ω-regular languages. Formal definitions of extended ω-
regular languages have been given in terms of both suitable classes of
automata and extended ω-regular expressions. On the contrary, satisfac-
tory temporal logic counterparts are still missing. In this paper, we give
a characterization of them in terms of interval temporal logics.
1 Introduction
In this paper, we explore the relationships between extended ω-regular lan-
guages and temporal logic by providing a characterization of language expres-
sions in terms of formulas of suitable interval temporal logics.
ω-regular languages are a natural setting for the specification and verifica-
tion of nonterminating finite-state systems. Since the seminal work by Büchi,
McNaughton, and Rabin in the sixties, much has been done on the theory and
the applications of ω-regular languages. Equivalent characterizations of ω-regular
languages have been given in terms of formal languages, automata, classical and
temporal logic. However, while the consensus on what features regular languages
of finite words must exhibit is unanimous (it largely relies on Myhill-Nerode the-
orem), the notion of ω-regular languages is more controversial. In the last years,
it has been shown that ω-languages can be extended in meaningful ways, preserv-
ing their decidability and (some of their) closure properties [3–6]. The proposed
extensions pair the Kleene star (.)∗ with some variants of it. The bounding ex-
ponent B of ωB-regular languages, denoted by (.)B , constrains the language
L in the expression LB to be iterated only a bounded number of times, the
bound being fixed for the whole ω-word [6].3 The unbounding exponent S of
ωS-regular languages, denoted by (.)S , when applied to a language L, forces
?
Partially supported by the GNCS 2020 project “Ragionamento Strategico e Sintesi
Automatica di Sistemi Multi-Agente”.
??
Copyright c 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
3
We are obviously assuming that there are no other occurrences of L in the ωB-regular
expression. The same holds for the other extended ω-regular languages.
2 D. Della Monica et al.
the number of iterations of L to tend to infinity, i.e., for every k > 0, it con-
strains the number of times the argument L is repeated at most k times to
be finite [6]. (.)B and (.)S can be freely mixed in ωBS-regular languages (the
combination of ωB- and ωS-regular ones) [6]. ωB- and ωS-regular languages
are properly included in ωBS-regular ones [5], as witnessed by the ωBS-regular
language L = (aB b + aS b)ω consisting of those ω-words w featuring infinitely
many occurrences of b and such that there are only finitely many numbers oc-
curring infinitely often in the sequence of exponents of a in w. The existence
of non-ωBS-regular languages that are the complements of some ωBS-regular
ones and express natural asymptotic behaviours motivated the search for other
classes of extended ω-regular languages. In [2], ωT -regular languages, which are
based on a different extension of (.)∗ , denoted by (.)T , and include meaningful
non-ωBS-regular languages, like, e.g., the complement of L above, have been
studied. Besides those in terms of ωB-, ωS-, ωBS-, and ωT -regular expressions,
equivalent characterizations of the above languages have been given in terms of
automata and classical logic (extensions of the monadic second-order theory of
one successor S1S). Temporal logic counterparts are still missing. As a matter
of fact, interval temporal logic counterparts of ωB- and ωS-regular languages
were proposed in [15] and [14], respectively. Unfortunately, both of them are
flawed. Here, we provide a fix, and, in addition, give an interval temporal logic
characterization of ωT -regular languages.
Interval temporal logic (ITL) is a general framework for representing and
reasoning about time. ITLs are characterized by high expressiveness (they over-
come various limitations of point-based temporal logics) and high computational
complexity (formulas translate into binary relations over the underlying linear
order). One of the first ITLs proposed in the literature is Moszkowski’s Propo-
sitional ITL (PITL), which was successfully applied to hardware specification
and verification [17]. The application of interval-based formalisms to temporal
reasoning in AI was first investigated by Allen [1]. A systematic logical study of
interval reasoning started with Halpern and Shoham’s work on the logic HS fea-
turing one modality for each Allen relation [10]. While decidability is a common
feature of point-based temporal logics, undecidability rules over ITLs. The first
such undecidability results were obtained for PITL by Moszkowski [16]. General
undecidability results for HS are given in [10] and further sharpened in [11]. For
a long time, these results have discouraged the search for practical applications
and further theoretical investigation on ITLs. This bleak picture started light-
ening up in the last few years when various non-trivial decidable fragments of
HS have been identified (see, e.g., [7, 8]). In this paper, we focus on the interval
logic AB, whose modalities correspond to Allen’s relations meets (modality hAi)
and begun by (modality hBi) [13], and some extensions of it with modalities for
the inverse relations met by (modality hĀi) and begins (modality hB̄i). In [15],
Montanari and Sala have proved that regular (resp., ω-regular) languages can be
defined in AB B̄, interpreted over finite linear orders (resp., N).4 Here, we show
that extended ω-regular languages can be captured by suitable extensions of AB.
4
In fact, hB̄i simplifies the encoding, but it is not necessary; thus, we do not use it.
Extended ω-Regular Languages and Interval Temporal Logic 3
In particular, we show that (i) ωB-regular languages can be expressed in AB Ā,
that extends AB with the past modality hĀi corresponding to Allen’s relation
met by [12], (ii) ωS-regular languages can be encoded in AB enriched with an
equivalence relation ∼ (AB∼) [14], and (iii) ωT -regular languages are captured
by AB Ā∼. A distinctive feature of the encodings is that they do not resort to
any counter, that is, checking the satisfaction of boundedness/unboundedness
conditions in interval temporal logic does not require the precision in length
measurements given by counters (in fact, some abstraction over counters, that
allows one to consider orders of magnitude rather than exact values, is applied
also in the automaton-based characterizations of extended ω-regular languages).
The paper is organized as follows. First, we provide some background knowl-
edge. Then, we enrich the encoding of ω-regular languages into AB given in [15]
to capture the increased expressive power of extended ω-regular languages.
2 Preliminaries
Extended ω-regular languages. We give a short account of extended ω-
regular languages in terms of the extended ω-regular expressions that define
them. For a detailed one, we refer the reader to [2]. Extended ω-regular ex-
pressions are built on top of the corresponding extended regular ones, just as
ω-regular expressions are built on top of regular ones. Let Σ be a finite, nonempty
alphabet. An extended regular expression over Σ is defined by (a subset of) the
grammar: e ::= ∅ | a | e · e | e + e | e∗ | eB | eS | eT , where a ∈ Σ.
Extended regular expressions differ from regular ones as they allow construc-
tors from the set {(.)B , (.)S , (.)T }. Their semantics is given in terms of languages
of infinite sequences of finite words, by imposing suitable constraints that capture
the intended meaning of (.)B , (.)S , and (.)T .
Let N be the set of natural numbers and N+ = N \ {0}. For an infinite
sequence u of finite words over Σ and i ∈ N+ , we denote by ui its i-th element.
The basic shuffle operation is defined as follows [2]. Let v 1 = (v11 , v21 , . . .) and
v 2 = (v12 , v22 , . . .) be two infinite word sequences, and let g : N+ → {1, 2} be
a selection function. We define the g-shuffle of v 1 and v 2 as the word v =
g(i)
(v1 , v2 , . . .), where vi = v|{j∈N+ |j≤i and g(j)=g(i)}| for all i ∈ N+ . We say that an
infinite word sequence v is a shuffle of v 1 and v 2 if there is a selection function
g such that v is the g-shuffle of them. Notice that the set of selection functions
includes those g where there exists k ∈ N+ such that g(x) = 1 (resp., g(x) = 2),
for all x > k.
The semantics of extended regular expressions over Σ is defined as follows:
– L(∅) = ∅;
– for a ∈ Σ, L(a) only contains the infinite sequence of the one-letter word a,
that is, L(a) = {(a, a, a, . . .)};
– L(e1 · e2 ) = {w | ∀i.wi = ui · vi , u ∈ L(e1 ), v ∈ L(e2 )};
– L(e1 + e2 ) = {w | w is a shuffle of u and v, for some u, v ∈ L(e1 ) ∪ L(e2 )};
– L(e∗ ) = {(uf (0) u2 . . . uf (1)−1 , uf (1) . . . uf (2)−1 , . . .) | u ∈ L(e) and f : N →
N+ is a nondecreasing function with f (0) = 1};
4 D. Della Monica et al.
– L(eB ) = {(uf (0) u2 . . . uf (1)−1 , uf (1) . . . uf (2)−1 , . . .) | u ∈ L(e) and f : N →
N+ is a nondecreasing function, with f (0) = 1, such that ∃n ∈ N ∀i ∈
N.(f (i + 1) − f (i) < n)};
– L(eS ) = {(uf (0) u2 . . . uf (1)−1 , uf (1) . . . uf (2)−1 , . . .) | u ∈ L(e) and f : N →
N+ is a nondecreasing function, with f (0) = 1, such that ∀n ∈ N ∃k ∈
N ∀i > k(f (i + 1) − f (i) > n)};
– L(eT ) = {(uf (0) u2 . . . uf (1)−1 , uf (1) . . . uf (2)−1 , . . .) | u ∈ L(e) and f : N →
N+ is a nondecreasing function, with f (0) = 1, such that ∃ω n ∈ N ∀k ∈
N ∃i > k.(f (i + 1) − f (i) = n)}.
Given a sequence v = (uf (0) u2 . . . uf (1)−1 , uf (1) . . . uf (2)−1 , . . .) ∈ eop , with
u ∈ L(e) and op ∈ {∗, B, S, T }, we define the sequence of exponents of e in v, de-
noted by N (v), as the sequence f (i+1)−f (i) i∈N . While the ∗-constructor does
not impose any constraint on N (v), the B-constructor forces it to be bounded,
the S-constructor forces it to be strongly unbounded, that is, its limit inferior is
infinite (equivalently, no exponent occurs infinitely often in the sequence), and
the T -constructor requires infinitely many exponents to occur infinitely often.
Let e be a BST -regular expression. The ω-constructor turns languages of
infinite word sequences into languages of ω-words (flattening) as follows:
– L(eω ) = {w | |w| = ∞ and w = u1 u2 u3 . . . for some u ∈ L(e)}.
ωBST -expressions are defined by the following grammar, where we denote
languages of word sequences (resp., words) by lowercase (resp., uppercase) letters
e, e1 , . . . , (resp., E, E1 , . . . , R, R1 , . . . ): E ::= E+E | R·E | eω where R is a reg-
ular expression, e is a BST -regular expression, and + and · respectively denote
union and concatenation of word languages (formally, L(E1 +E2 )=L(E1 )∪L(E2 )
and L(E1 ·E2 )={u·v | u ∈ L(E1 ), v ∈ L(E2 )}).5 As we did for languages of word
sequences, we will sometimes omit the operator · between word languages.
Interval temporal logics AB, AB Ā, AB∼, and AB Ā∼. Syntax and seman-
tics of AB, AB Ā, AB∼, and AB Ā∼ are defined as follows. AB features modali-
ties hAi and hBi, that correspond to Allen’s relations meets (denoted by A) and
begun by (B), respectively. Its satisfiability problem is EXPSPACE-complete over
both finite linear orders and N [13]. Formally, given a set Prop of proposition
letters, formulas of AB are defined as follows: ϕ := p | ϕ ∨ ϕ | ¬ϕ | hAiϕ | hBiϕ,
where p ∈ Prop. We use the shorthands ϕ ∧ ψ for ¬(¬ϕ ∨ ¬ψ), [X]ϕ for
¬hXi(¬ϕ), with X ∈ {A, B}, ⊥ for p ∧ ¬p, and > for p ∨ ¬p. Formulas of AB
are interpreted in interval temporal structures over N endowed with Allen’s rela-
tions A and B. We identify any given ordinal N ≤ ω with the prefix of length N
of N, and we accordingly define I(N ) as the set of all closed intervals [i, j], with
i, j ∈ N and i ≤ j. A special role will be played by point intervals (intervals [i, i],
for each i ∈ N ) and unit intervals (intervals [i, i + 1]), which are captured by the
formulas π = [B]⊥ and unit = hBi> ∧ [B][B]⊥, respectively. Allen’s relations
A and B are defined as follows. Given two intervals [i, j], [i0 , j 0 ] ∈ I(N ), we say
that: (a) [i, j]A[i0 , j 0 ] if and only if j = i0 ; (b) [i, j]B[i0 , j 0 ] if and only if i = i0 and
j > j 0 . AB semantics is given in terms of interval models M = hI(N ), A, B, V i,
5
Notice the abuse of notation with the previous definition of the operators + and ·
over languages of word sequences.
Extended ω-Regular Languages and Interval Temporal Logic 5
where V : I(N ) → P(Prop) is the valuation function that assigns to every in-
terval the set of proposition letters that are true on it. Truth of AB formulas
is inductively defined as follows: (i) clauses for proposition letters and Boolean
connectives are defined as usual; (ii) M, [i, j] |= hXiϕ, for X ∈ {A, B}, if and
only if there exists an interval [i0 , j 0 ] such that [i, j]X[i0 , j 0 ] and M, [i0 , j 0 ] |= ϕ.
Given M = hI(N ), A, B, V i and ϕ, M satisfies ϕ if there is [i, j] ∈ I(N ) such that
M, [i, j] |= ϕ, and ϕ is satisfiable if there is an interval model M that satisfies it.
AB Ā is obtained from AB by adding the (past) modality hĀi for the Allen
relation met by (Ā). Unlike what happens with point-based temporal logics,
the addition of past operators to interval ones usually increases both their ex-
pressiveness and their computational complexity (see, e.g., [9]). This is the case
with AB Ā: its satisfiability problem is still decidable, but non-primitive recur-
sive, over finite linear orders, and undecidable over N [12]. AB Ā syntax extends
that of AB in the obvious way. As for its semantics, for any pair of intervals
[i, j], [i0 , j 0 ] ∈ I(N ), [i, j]Ā[i0 , j 0 ] if and only if i = j 0 . AB Ā formulas are inter-
preted on models M = hI(N ), A, B, Ā, V i. The semantics is defined as expected.
AB∼ is obtained from AB by adding an equivalence relation ∼ over the
points of the model. Similarly to AB Ā, the satisfiability problem for AB∼ re-
mains decidable over finite linear orders, but it becomes non-primitive recur-
sive, while decidability is lost over N [14]. Formally, the language of AB is ex-
tended with a new symbol ∼, and formulas are built according to the syntax:
ϕ := p | ∼ | ϕ ∨ ϕ | ¬ϕ | hAiϕ | hBiϕ | hB̄iϕ, where p ∈ Prop. AB∼ formulas
are interpreted on models M = hI(N ), A, B, ∼, V i, where ∼ is an equivalence
relation on N . Truth is defined as for AB formulas, with an additional semantic
clause for ∼: M, [i, j] |=∼ if and only if i ∼ j. Syntax and semantics of AB Ā∼
are obtained from those of AB Ā and AB∼ by merging them in the obvious way.
Hereafter, we use modalities [G] (globally in the future) and [init](every ini-
tial interval ), which are defined as follows: (i) [G]ϕ iff [B][A]ϕ∧[A][A]ϕ, and
(ii) [init]ϕ iff [B](π → [A]ϕ) ∧ (π → [A]ϕ). Both of them are definable in all the
above logics. When evaluated on [x, y], [G]ϕ forces ϕ to be true over all [w, z]
with w ≥ x; in particular, when evaluated on [0, y], it forces ϕ to be true on all
intervals. When evaluated on [x, y], [init]ϕ forces ϕ to be true on all [x, z]; in
particular, when evaluated on [0, y], it forces ϕ to be true on all initial intervals.
3 Encoding ωB-, ωS-, and ωT -regular languages
Building on the encoding of regular and ω-regular expressions in AB given
in [15] (for the convenience of the reader, they are reported in the appendix), we
provide an encoding of ωB-, ωS-, and ωT -regular ones into suitable extensions of
AB. As already noticed, an encoding of ωB-regular (resp., ωS-regular) expres-
sions in AB B̄ Ā (resp., AB B̄ ∼) was proposed in [15] (resp., [14]). Unfortunately,
both encodings are flawed. Let us focus on ωB-regular expressions. Let E be an
expression and ei be a sub-expression of the form eB j . In [15], two formulas of
AB B̄ Ā are exploited to encode the B-constructor: a local one, which is basically
the same used for the Kleene star, and a global one, that constrains the size of ei
6 D. Della Monica et al.
blocks to be bounded. The latter formula says that, for any ω-word belonging to
the language, it is possible to define an infinite sequence of positions (milestones)
such that (i) no milestone is properly contained in an ei block, and (ii) the win-
dow between two consecutive milestones contains a non-increasing number of
occurrences of ej . In the following, we show that such a claim is wrong.
Let σ = (an )n∈N be a sequence of natural numbers. We define a group-
ing of σ as a sequence ρ of natural numbers (bn )n∈N such that bn =
Pf (n+1)−1
i=f (n) ai , where f : N → N, with f (0) = 0, is an increasing func-
tion (that identifies the milestones). The above claim can be reformulated
as follows: every bounded sequence admits a non-increasing grouping. Since
we are dealing with N, the only sequences that satisfy such a condition are
the definitively constant ones. A counterexample is given by the sequence
σ = 1, 2, 1, 2, 2, 1, 2, 2, 2, 1, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 1, . . . (we would like to thank
David Barozzini for it). By contradiction, assume that there is a non-increasing
grouping ρ = (bn )n∈N of σ. Then, for every i ∈ N, it holds that f (i+1)−f (i) ≤ b0 .
We show that ρ is not definitively constant. Suppose that, for some i, bi is odd.
For i large enough, we can assume that the sequence af (i) , af (i)+1 , . . . , af (i+1)−1
contains exactly one occurrence of 1 (as the difference between of two consecutive
terms of f is bounded, while the distance between two consecutive occurrences
of 1 is not). Moreover, if i is large enough, we can also assume that the se-
quence af (i+1) , af (i+1)+1 , . . . , af (i+1)+b0 contains no occurrence of 1. It follows
that bi+1 is even, and thus bi+1 < bi . Suppose now that, for some i, bi is even.
For i large enough, we can assume that the sequence af (i) , af (i)+1 , . . . , af (i+1)−1
contains no occurrence of 1. It follows that there exists j > 0 such that
af (i+j) , af (i+j)+1 , . . . , af (i+j+1)−1 contains exactly one occurrence of 1. Thus,
bi+j is odd, and bi+j < bi .
Let us consider now ωB-, and ωS-, and ωT -regular expressions. Given an
expression E, we list its sub-expressions e1 , . . . , en (= E) in increasing order
of complexity. Then, for all i, we introduce two proposition letters expr i and
expriend , and then we define inductivelyVa formula ϕexpr Vin. Finally, weVcapture the
n n 6∩
language L(E) with the formula ϕE = i=1 ϕexpr i ∧ i=1 ϕend expr i ∧ i=1 ϕexpr i .
The only missing ingredient is a way to recursively define formulas ϕexpr i for ei of
the forms eB S T
j , ej , and ej . These formulas are conjunctions of two sub-formulas,
a local one, that is the same we defined in the case ei = e∗j , and a global one,
which guarantees the constraints imposed by the B-, S-, and T -constructors.
It is worth remarking that if, for a sub-expression ei = eB j of E, there are
only finitely many occurrences of expr i intervals in the model, then we do not
need to guarantee the satisfaction of the boundedness constraint imposed by
the B-constructor (the same holds for ei = eSj and ei = eTj ). This is the case,
for instance, with expressions like (aB b + a∗ b)ω , which is, in fact, equivalent to
(a∗ b)ω due to the shuffle operator that, from a given position on, can postpone
forever the selection of occurrences of aB b. Thus, formulas we are going to build
in the next sections are assumed to be (and, in the end, will be) guarded by the
requirement that infinitely many expr i intervals occur.
Extended ω-Regular Languages and Interval Temporal Logic 7
exprn exprn exprn exprn
expri expri expri expri expri
… … … … … … … … … … … … … … … … … … … … … … … … … … … … …
pj pj pj pj pj
pj pj pj
exprnend hAiexpri exprjend expriend hAiexpri exprjend expriend
exprjend phj hAipj exprjend blj
(i,j)
Fig. 1: Example of the structure we are enforcing by means of formula ΦB for an
expression E = (en )ω , where en contains the sub-expression ei = eB
j (dashed intervals
represent expr j intervals).
ωB-regular languages in AB Ā. Let B(E)={(i,j) : ei =eB j is a sub-expression
of E}. To force the proper behaviour of the B-constructor, for every (i,j)∈B(E),
we introduce the additional proposition letters phj , blj , and pj , which can be ex-
ploited to express (by means of suitable AB Ā formulas) the following properties:
1. phj and blj may only label left endpoints of expr j intervals which are not
left endpoints of expr i ones, but they cannot label the same points:
[G](phj ∨blj → π ∧hAiexpr j ∧¬hAiexpr i )∧[G]((phj → ¬blj )∧(blj → ¬phj ));
2. there exists n ∈ N such that every n0 > n which is the left endpoint of an
expr j interval, but not the left endpoint of an expr i interval, is labeled with
either phj or blj : [G](hAi[A](hAiexpr j ∧ [A]¬expr i → hAi(phj ∨ blj )));
3. in between two consecutive blj points x, y, with x < y, there exists at least
one point z, with x < z < y, such that z is the left endpoint of an expr i
interval: [G](hBiblj ∧ hAiblj → hBihAiexpr i );
4. every phj point is the left endpoint of exactly one pj interval: [G](phj →
hAipj ) ∧ [G](pj → ¬hBipj );
5. every pj interval is begun by a phj point and strictly contains exactly one
blj point: [G](pj → hBiphj ∧ hBihAiblj ∧ [B](hAiblj → ¬hBihAiblj ));
6. every phj point x for which there exists a blj point y such that y < x is the
right endpoint of at least one pj interval: [G](hAiphj ∧ hBiblj → hAihĀipj ).
Fig. 1 gives a graphical account of the above properties. Let us assume that
infinitely many expr i intervals occur. Properties 1–2 guarantee that, from a point
on, say it n, every point which is the left endpoint of an expr j interval, but not of
an expr i one, is labeled with either phj or blj . By properties 4–5, every phj point
is followed by a blj one. Thus, the suffix starting at n can be seen as a (possibly
finite or even empty) sequence of slices [n0 , n1 ], [n1 , n2 ] . . ., where {n0 , n1 , . . .} is
the set of blj points greater than n. Now, let [nk , nk+1 ]phj be the set of all and
only those phj points x, with nk < x < nk+1 , that, by properties 1–2, are left
endpoints of expr j intervals, but not of expr i ones. By properties 4–6, pj encodes
a series of surjective functions fk : [nk , nk+1 ]phj → [nk+1 , nk+2 ]phj , with k ≥ 0,
linking the phj points of pairs of consecutive slices.6 It follows that |[n0 , n1 ]phj | ≥
|[n1 , n2 ]phj | ≥ . . ., i.e., the sequence is not increasing. Finally, property 3 imposes
that, for every k, there is at least one point x, with nk < x < nk+1 , which is
6
As a matter of fact, the image of one such function fk might also include elements not
belonging to [nk+1 , nk+2 ]phj ; however, properties 4–6 guarantee that [nk+1 , nk+2 ]phj
is included in the image, which is enough for our purposes.
8 D. Della Monica et al.
the left endpoint of an expr i interval. Then, every expr i interval starting after
n spans at most two adjacent slices, and thus it contains at most |[n0 , n1 ]phj | ∗ 2
many expr j intervals, thus providing a bound, as required by the B-constructor.
(i,j)
Now, for every (i, j) ∈ B(E), let ΨB be the conjunction of the above
(i,j) (i,j)
formulas and ΦB = [G]hAihAiexpr i → ΨB .
Theorem 1. Let E be an ωB-regular expression over Σ. Then, L(E) =
{w ∈ Σ ω : w ≈ M for some model M such that M, [0, n] |= ϕE ∧ ϕΣ ∧
V (i,j)
(i,j)∈B(E) ΦB for some n ∈ N}.
ωS-regular languages in AB∼. Let S(E)={(i,j) : ei =eSj is a sub-expression of
E}. To force the proper behaviour of the S-constructor, we make use of the
equivalence relation ∼ and, for all (i, j) ∈ S(E), we introduce the proposition
letters phj and newj , that allow us to express (by means of suitable AB∼
formulas) the following properties:
1. phj may only label left endpoints of expr j intervals which are neither left nor
right endpoints of expr i ones (this implies that a phj point must occur inside
an expr i interval): [G](phj → π ∧ hAiexpr j ∧ ¬hAiexpr i ∧ ¬hAiexpriend );
2. if two phj points x and y, with x < y, belong to the same expr i interval,
then x 6∼ y, or, equivalently, if x ∼ y, then they belong to two distinct expr i
intervals: [G](∼ ∧hBiphj → hAiphj ∧ hBihAiexpr end i );
3. for every expr i interval [n, n0 ] that contains at least one phj point, there is
an expr i interval [n, n0 ] with n ≥ n0 . Moreover, if n is the smallest point such
that n ≥ n0 and there is n0 > n for which [n, n0 ] is an expr i interval, then, for
every phj point x, with n < x < n0 , there is a phj point y, with n < y < n0 ,
such that x ∼ y (notice that property 2 forces such a point y to be uniquely
determined): [G](phj → hAi(¬π∧ ∼ ∧[B](hAiexpriend → [B][A]¬expriend )));
4. for all expr i interval [n, n0 ], let |[n, n0 ]|phj = |{x : n < x <
n0 , x is a phj point }| be the number of phj points inside [n, n0 ]. If the model
features an infinite sequence [n0 , n00 ], [n1 , n01 ], . . . of expr i intervals, then the
sequence |[n0 , n00 ]|phj , |[n1 , n01 ]|phj , . . . is non-decreasing and unbounded. It
follows that there are infinitely many classes of phj points. This is expressed
by means of the auxiliary proposition letter newj as follows: (i) newj may
only appear in a labeling that already contains phj ; (ii) for a newj point x,
there is no point y, with y < x, such that y ∼ x; (iii) for every phj point x
we have that there exists a newj point y > x:
[G](newj → phj ) ∧ [G](¬π ∧ ∼ → [A]¬newj ) ∧ [G](phj →
hAi(¬π ∧ hAinewj )).
A graphical account of the properties imposed by the above formulas is given
in Fig. 2. First, we observe that expr i intervals may contain a different number
of expr j intervals. From one expr i interval to the next one, such a number may
increase, decrease, or remain the same. However, according to the semantics of
the S-constructor, for every n ∈ N, such a number is forced to be greater than n
for a suffix of the model. This is done by means of proposition letter phj . Once
the left endpoint of an expr j interval included in an expr i one is labeled with
phj , properties 2 and 3 guarantee that, in every future expr i interval, there is
Extended ω-Regular Languages and Interval Temporal Logic 9
exprn exprn
expri expri expri expri expri
… … … … … … … … … … … … … … … … … … … … … … … …
⇠ ⇠ ⇠ ⇠ ⇠
⇠ ⇠ ⇠
exprnend hAiexpri exprjend expriend hAiexpri exprjend expriend
exprjend exprjend phj exprjend phj newj
(i,j)
Fig. 2: Example of the structure we are enforcing by means of formula ΦS for an
expression E = (en )ω , where en contains the sub-expression ei = eS
j (dashed intervals
represent expr j intervals).
exactly one phj point belonging to the same equivalence class. Every equivalence
class can thus be seen as an infinite chain (with a starting point) of phj points
belonging to consecutive expr i intervals. It follows that the number n of distinct
phj points belonging to an expr i interval forces all the following expr i intervals
to contain at least n distinct phj points, and thus, by property 1, at least n expr j
intervals. Now, let us observe, as shown in Fig. 2, that not all the left endpoints
of the expr j intervals belonging to an expr i one must be labeled with phj . In this
way, their number may fluctuate, while phj points ensure that such a number
does not go below a certain threshold. Finally, property 4 guarantees that the
equivalence relation of phj points is of infinite index, and thus the behaviour of
the S-constructor is correctly captured.
To complete the encoding, we need to guarantee the presence of phj points
and the behaviour induced by them whenever there are infinitely many expr i
intervals in the model. Indeed, if ej is matched to ε infinitely often, i.e., if there
are infinitely many occurrences of point intervals labeled with expr j , then there
is no need to guarantee the satisfaction of the unboundedness constraint imposed
by the S-constructor, because ε can “hide” arbitrarily many repetitions of ej .
To this end, it suffices to add a formula that constrains the model to feature at
least one phj point if it features infinitely many expr i intervals, but only finitely
many point intervals labeled with expr j . Last but not least, we need to prevent
the case in which there are infinitely many occurrences of point intervals labeled
with expr i but not expr j , which corresponds to infinitely many instantiations of
ei with zero repetitions of ej . Such a condition is encoded by the second conjunct
of the consequent of the implication: [G]hAihAiexpr i ∧ hAi[A][A](expr j →
¬π) → hBihAihAiphj ∧ hAi[A][A](expr i → ¬π).
(i,j)
For all (i, j) ∈ S(E), let ΦS be the conjunction of the above formulas.
Theorem 2. Let E be an ωS-regular expression over Σ. Then, L(E) =
{w ∈ Σ ω : w ≈ M for some model M such that M, [0, n] |= ϕE ∧ ϕΣ ∧
V (i,j)
(i,j)∈S(E) ΦS for some n ∈ N}.
ωT -regular languages in AB Ā∼. Let T (E)={(i, j) : ei =eTj is a sub-expres-
sion of E}. To encode ωT -regular languages in AB Ā∼, we first show that a
(i,j)
particular class of models over N can be captured by AB Ā∼ formulas Φ∞ , for
(i, j) ∈ T (E). Then, we use such a formula to constrain the behaviour of (.)T .
10 D. Della Monica et al.
By making use of proposition letters phj , blj , pj , qj , and conf j , and of the
proposition letter ∼, representing an equivalence relation over N, we want to
(i,j)
characterize, through Φ∞ , the models that satisfy the following properties:
1. phj , blj , and conf j only appear as labels of points, phj and blj never occur
together in the same labeling, and conf j only appears in a labeling containing
also blj , that is, a configuration (an interval whose endpoints are consecutive
conf j points) features one or more blocks (intervals whose endpoints are
consecutive blj points): [G]((blj ∨ phj → π) ∧ (conf j → blj ) ∧ (phj → ¬blj ));
2. there are infinitely many conf j points, that is, there are infinitely many
configurations: [G]hAihAiconf j ;
3. between two consecutive blj points there is at least one phj point and all of
them belong to the same equivalence class, that is, each block is associated
with exactly one equivalence class of phj points: [G](hBiblj ∧ hAiblj →
hBihAiphj ) ∧ [G](hBiphj ∧ hAiphj ∧ [B][A]¬blj →∼);
4. let x, y, and z, with x < y < z, be three consecutive blj points and y be not
labeled with conf j ; then, there are more phj points between x and y than
between y and z, that is, the sequence of the numbers of phj points featured
in blocks of the same configuration is strictly decreasing:
[G](pj → hBiphj ∧ hAiphj ∧ [B]¬pj ∧ [B][A]¬conf j ∧
hBihAiblj ∧ [B](hAiblj → [B][A]¬blj )) ∧
[G](phj ∧ [A](¬π∧ ∼→ hBihAiblj ) → [A]¬pj ) ∧
[G](phj ∧ hĀi(hBiblj ∧ [B][A]¬conf j ) → hĀipj );
5. for every pair of phj points x and y, with x < y, if there is a blj point but
no conf j point between them, then x 6∼ y, that is, pairs of distinct blocks in
the same configuration represent distinct equivalence classes of phj points:
[G](∼ → (hBiphj ↔ hAiphj )) ∧
[G](∼ ∧hBiphj ∧ hBihAiblj → hBihAiconf j );
6. for every phj point x there is a phj point y > x such that x ∼ y and there
is exactly one conf j point between x and y, that is, an equivalence class in
a configuration is witnessed in all the following configurations:
[G](phj → hAi(∼ ∧hBihAiconf j ∧ [B](hAiconf j → [B][A]¬conf j )));
7. let x, y, and z be three consecutive conf j points, with x < y < z; then,
there are less blj points between x and y than between y and z, that is, the
sequence of the numbers of blocks in configurations is strictly increasing:
[G](conf j → hAi(hAiphj ∧ [B](¬π → [A]¬conf j ) ∧ hAi[Ā]¬ ∼));
8. if (x, y) and (x0 , y 0 ) are two pairs of blj points, with x < y < x0 < y 0 ,
both witnessing the same equivalence class, then the number of phj points
between x and y is greater than or equal to the number of those between x0
and y 0 , that is, the sequence of blocks of phj points in the same equivalence
class is non-increasing in the number of phj points in every block:
[G](qj → ∼ ∧[B]¬qj ∧ hBihAiconf j ∧ [B](hAiconf j → [B][A]¬conf j )) ∧
[G](phj ∧ hĀi(∼ ∧hBihAiblj ) → hĀiqj ).
(i,j)
Let Φ∞ be the conjunction of the above formulas. A graphical account of
(i,j)
the structure enforced by Φ∞ is given in Fig. 3. Notice that there may be points
whose labeling do not contain any of the proposition letters phj , blj , and conf j .
Extended ω-Regular Languages and Interval Temporal Logic 11
⇠
⇠
> > > > > >
… ... ... ... ... ... ... ... ...
phj phj phj phj phj phj phj phj …
blj blj
0 confj
blj blj blj
confj
blj blj blj blj
confj
⇠
(i,j)
Fig. 3: Example of the type of structure we enforce by means of formula Φ∞ .
(i,j)
Thanks to Φ∞ , a model can be seen as an infinite sequence of configurations
[conf 0j , conf 1j ], [conf 1j , conf 2j ], ... For every x ∈ N, conf xj contains a finite sequence
x,n(x)
of n(x) + 1, with n : N → N, sets Sbljx,0 , . . . , Sblj of phi points each one
associated with exactly one equivalence class, i.e., points in Sbljx,y belong to the
same equivalence class, for every y ∈ {0, . . . , n(x)}. Formally, Sbljx,y = {n ∈ N :
M, [n, n] |= phj , |{n0 < n : M, [n0 , n0 ] |= conf j }| = x + 1, |{n0 < n : M, [n0 , n0 ] |=
blj , ∀n00 (n0 < n00 < n → M, [n00 , n00 ] 6|= conf j )}| = y}. Intuitively, n(x) + 1 is the
number of blocks in [conf x , conf x+1 ] and |Sbljx,y | is the number of phj points in
the yth block of [conf x , conf x+1 ]. The following properties hold:
(P1) the function n(x) is strictly increasing (property 7);
0
(P2) for all x, y, y 0 ∈ N, with 0 ≤ y < y 0 ≤ n(x), |Sbljx,y | > |Sbljx,y | (property 4);
(P3) for every phj point w it is possible to identify an infinite sequence of pairs of
indexes (x, y0 ), (x + 1, y1 ), . . . such that [w]∼ = k∈N Sbljx+k,yk (property 6)
S
and |Sbljx,y0 | ≥ |Sbljx+1,y1 | ≥ . . . (property 8);
(P 3) states that, for every equivalence class [w]∼ of phj points, there is a config-
uration such that [w]∼ is witnessed exactly in all the successive configurations.
Moreover, it states that the blocks that witness [w]∼ feature a non-increasing
number of points. Let (x, y0 ), (x + 1, y1 ), . . . be such that [w]∼ = k∈N Sbljx+k,yk .
S
Since the number of points in each block is finite, there is k 0 ∈ N for which
x+k0 ,yk0 x+k0 +1,yk0 +1
|Sblj | = |Sblj | = . . ., i.e., the sequence of Sbljx+k,yk cardinal-
ities converges to a single value (we call it the value of the equivalence class),
denoted by val([w]∼ ). By (P 2), it holds that for any two distinct equivalence
classes [w]∼ and [w0 ]∼ of phj points, val([w]∼ ) 6= val([w0 ]∼ ); otherwise, it would
be possible to find a configuration featuring two distinct blocks with the same
number of phj points, which contradicts (P 2). Finally, (P 1) guarantees that the
number of distinct equivalence classes is infinite. The following lemma holds.
(i,j)
Lemma 1. If M, [0, 0] |= Φ∞ , then there exists an infinite subset N of N such
that for every n ∈ N there is w ∈ N with val([w]∼ ) = n.
An instantiation of an equivalence class with an expr i interval is a correspon-
dence between the number of phj points in a block associated with that class
and the number of expr j intervals in the expr i interval. This is the case when
the set of phj points in the block and the set of points starting an expr j interval
within the expr i interval coincide. The T -constructor forces all the equivalence
classes to be instantiated infinitely many times. Indeed, if an equivalence class is
instantiated infinitely often, the infinitely many expr i intervals are matched by
12 D. Della Monica et al.
repetitions of val([w]∼ ) many expr j intervals in an ω-iteration. Since the number
of equivalence classes is infinite and all of them feature distinct values val([w]∼ ),
the behaviour of the T -constructor is correctly encoded.
However, there are cases in which we do not need to satisfy the constraint
imposed by the T -constructor or it suffices to satisfy a weaker version of it. This
is the case when (i) there are only finitely many expr i intervals, as for B- and
S-constructors; (ii) there are infinitely many point intervals labeled with both
expr i and expr j ; this corresponds to ei being matched by occurrences of expr j
matched, in turn, by the empty string ε; in this case, such an expr i interval can
be thought of as featuring any possible number of expr j intervals; (iii) there are
infinitely many expr j point intervals but only finitely many labeled with both
expr i and expr j ; in this case, it suffices to impose that at least one equivalence
class of phj points is instantiated infinitely often.
When none of the cases above applies, we force all the equivalence classes
to be instantiated infinitely many times. For an expr i interval [x, y], let
points j ([x, y]) = {z : x ≤ z ≤ y, ∃z 0 (M, [z, z 0 ] |= expr j )}, and, for a phj point
w, let Seq([w]∼ ) = (x, y0 ), (x + 1, y1 ), . . . be the sequence such that [w]∼ =
x+k,yk
. In what follow, we define a formula Φinj , which uses proposi-
S
k∈N Sblj
tion letter inj to force that, for every equivalence class [w]∼ of phj points, there
is an infinite sub-sequence (x0 , y 0 ), (x1 , y 1 ), . . . of Seq([w]∼ ) such that for every
x ,y
h ∈ N there is a distinct expr i interval [x0h , yh0 ] with points j ([x0h , yh0 ]) = |Sblj h h |,
i.e., each equivalence class is instantiated infinitely many times:
– inj appears only as the label of phj points that begin expr j intervals:
[G](inj → phj ∧ hAiexpr j );
– phj points that share the same block of an inj point are labeled with inj :
[G]((hBiphj ∧ hAiphj ∧ [B][A]¬blj ) → (hAiinj ↔ hBiinj ));
– every block of inj labeled points encloses exactly an expr i labeled interval:
[G](expr i ∧ hBihAiinj → [B][A]¬blj ∧ [Ā]([B][A]¬blj →
[B][A]¬inj ) ∧ [A]([B][A]¬blj → [B][A]¬inj ));
– if an expr i interval contains an inj point, then the expr j intervals within it
begin with an inj point: [G](expr i ∧ hBihAiinj → [B](hAiexpr j → hAiinj )).
(i,j)
For (i, j)∈S(E), let Φinj be the conjunction of the above
formulas and ΦT be
hAi[A][A]¬expr i ∨ [G]hAihAi(π ∧ expr i ∧ expr j ) ∨
(i,j)
Φ∞ ∧ Φinj ∧ [G]hAihAi(π ∧ expr j ) ∧ hBihAihAiinj ∧
∧ [G](inj → hAi(hBihAiconf j ∧ inj )) ∨
(i,j)
Φ∞ ∧ Φinj ∧ hAi[A][A](expr j → ¬π) ∧ [G](phj → hAi(¬π ∧ ∼ ∧hAiinj ))
Theorem 3. Let E be a ωT -regular expression over Σ. Then, L(E) =
{w ∈ Σ ω : w ≈ M for some model M such that M, [0, n] |= ϕE ∧ ϕΣ ∧
V (i,j)
(i,j)∈T (E) ΦT for some n ∈ N}.
4 Conclusions
In this paper, we filled a gap in the study of extended ω-regular languages
by providing a temporal logic characterization of ωB-, ωS-, and ωT -regular
Extended ω-Regular Languages and Interval Temporal Logic 13
languages. We showed how to turn ωB-, ωS-, and ωT -regular expressions into
formulas of suitable interval temporal logics. As for future work, we are looking
for syntactic and/or semantic fragments of the considered interval temporal log-
ics, that preserve (un)satisfiability of the resulting formulas and behave better
from a computational point of view.
References
1. Allen, J.F.: Maintaining knowledge about temporal intervals. Comm. of the ACM
26(11), 832–843 (1983). https://doi.org/10.1145/182.358434
2. Barozzini, D., de Frutos-Escrig, D., Della Monica, D., Montanari, A., Sala, P.:
Beyond ω-regular languages: ωT -regular expressions and their automata and logic
counterparts. Theor. Comput. Sci. 813, 270–304 (2020)
3. Bojańczyk, M.: A bounding quantifier. In: CSL. LNCS, vol. 3210, pp. 41–55.
Springer (2004). https://doi.org/10.1007/978-3-540-30124-0_7
4. Bojańczyk, M.: Weak MSO with the unbounding quantifier. Theory of Computing
Systems 48(3), 554–576 (2011). https://doi.org/10.1007/s00224-010-9279-2
5. Bojańczyk, M., Colcombet, T.: Bounds in ω-regularity. In: LICS. pp. 285–296
(2006). https://doi.org/10.1109/LICS.2006.17
6. Bojańczyk, M., Colcombet, T.: Boundedness in languages of infinite words. Logical
Methods in Computer Science Volume 13, Issue 4 (Oct 2017)
7. Bresolin, D., Della Monica, D., Montanari, A., Sala, P., Sciavicco, G.: Interval
temporal logics over strongly discrete linear orders: Expressiveness and complexity.
Theor. Comput. Sci. 560, 269–291 (2014)
8. Bresolin, D., Della Monica, D., Montanari, A., Sala, P., Sciavicco, G.: Decidability
and complexity of the fragments of the modal logic of allen’s relations over the ra-
tionals. Inf. Comput. 266, 97–125 (2019). https://doi.org/10.1016/j.ic.2019.02.002
9. Della Monica, D., Montanari, A., Sala, P.: The importance of the past in in-
terval temporal logics: The case of propositional neighborhood logic. In: Logic
Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the
Occasion of His 60th Birthday. LNCS, vol. 7360, pp. 79–102. Springer (2012).
https://doi.org/10.1007/978-3-642-29414-3_6
10. Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. Journal
of the ACM 38(4), 935–962 (Oct 1991). https://doi.org/10.1145/115234.115351
11. Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Proc. of
the 6th Asian Computing Science Conference – Advances in Computing Science –
ASIAN. LNCS, vol. 1961, pp. 290–298. Springer (2000). https://doi.org/10.1007/3-
540-44464-5_21
12. Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of Halpern and
Shoham’s modal logic of intervals. In: Proc. of the 37th ICALP, Part II. LNCS,
vol. 6199, pp. 345–356. Springer (2010). https://doi.org/10.1007/978-3-642-14162-
1_29
13. Montanari, A., Puppis, G., Sala, P., Sciavicco, G.: Decidability of the interval
temporal logic ABB over the natural numbers. In: Proc. of the 27th STACS. LIPIcs,
vol. 5, pp. 597–608. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010).
https://doi.org/10.4230/LIPIcs.STACS.2010.2488
14. Montanari, A., Sala, P.: Adding an equivalence relation to the interval logic ABB:
complexity and expressiveness. In: Proc. of the 28th LICS. pp. 193–202. IEEE
Computer Society (2013). https://doi.org/10.1109/LICS.2013.25
14 D. Della Monica et al.
15. Montanari, A., Sala, P.: Interval logics and ωb-regular languages. In:
Proc. of the 7th LATA. LNCS, vol. 7810, pp. 431–443. Springer (2013).
https://doi.org/10.1007/978-3-642-37064-9_38
16. Moszkowski, B.C.: Reasoning About Digital Circuits. Ph.D. thesis, Department of
Computer Science, Stanford University, Stanford, CA (1983)
17. Moszkowski, B.C., Manna, Z.: Reasoning in interval temporal logic. In: Proc. of
Workshop on Logic of Programs. LNCS, vol. 164, pp. 371–382. Springer (1983).
https://doi.org/10.1007/3-540-12896-4_374
Extended ω-Regular Languages and Interval Temporal Logic 15
A Encoding regular and ω-regular languages in AB
In the following, we describe the encoding of regular and ω-regular languages
in AB (they are basically those given in [15]).
To begin with, we show how to interpret words and ω-words as interval
temporal models, and vice versa. For a word w = w0 w1 . . . over a finite alphabet
Σ and a model M = hI(N ), A, B, V i, we say that M and w are compatible,
denoted by w ≈ M (or, equivalently, M ≈ w), if N = |w| + 1, Σ ⊆ Prop, and
V : I(N ) → P(Prop) is such that on each unit interval only the proper letter
holds, that is, V ([i, i + 1]) ∩ Σ = {wi } for every i < |w|.
Let R be a regular expression on Σ. We show how to encode R into an AB-
formula over the finite set of proposition letter Prop, which includes Σ. First, we
force proposition letters in Σ to hold true only on unit intervals, and constrain
each unit interval to satisfy exactly one proposition letter in Σ:
W V V
ϕΣ = [G] unit ↔ a∈Σ a ∧ a∈Σ a → b∈Σ\{a} ¬b .
The regular expression R can be given a tree structure, whose leaves and
internal nodes belong to Σ and {+, ·, ∗ }, respectively. Each sub-tree identifies
a sub-expression of R. Let e1 , . . . , en be all the sub-expressions of R, includ-
ing elements in Σ. For each ei , we introduce two new proposition letters expr i
and expriend . Notice that two occurrences ei and ej of the same sub-expression
are associated with two different pairs of proposition letters (expr i /expriend and
expr j /exprjend ). For each i, we force expriend to hold only at point intervals,
and if there is an interval where expr i holds true, then expriend holds on its
right endpoint, and on no point strictly included in the interval. Moreover, ev-
ery expriend is the ending point of an expr i interval. This is formalized by the
following formula:
ϕend
expr i = [G]((expri
end
→ π) ∧ (expr i → hAiexpriend ∧
[B](¬π → [A]¬expriend ))) ∧
[init](hAiexpriend → hAi(π ∧ expr i ) ∨ hBihAi(¬π ∧ expr i )) ∧
[G](hAiexpriend ∧ hBi(¬π ∧ expr i ) →
hBi(¬π ∧ hAi(¬π ∧ expr i ))).
Finally, we prevent two expr i intervals from intersecting (except for intersec-
tions of a single point):
ϕ6∩expr i = [G](expr i → [B](¬π → [A](¬expr i ∧ ¬expri
end
))).
Let e1 , . . . , en be ordered according to their complexity with en = R, that is,
if ei is a sub-expression of ej , then i ≤ j. We define formulas ϕexpr i by induction
on the complexity of expressions ei .
– If ei = a for some a ∈ Σ, we put ϕexpr i = [G](expr i → a).
– If ei = ε, we put ϕexpr i = [G](expr i → π).
– If ei = ej + ek , we put ϕexpr i = [G](expr i ↔ (expr j ∨ expr k )).
– If ei = ej ek , we distinguish two cases, depending on whether or not the string
matched by ej is the empty string. The first conjunct of the formula below
states that every interval on which expr i holds can be split in two ordered
parts on which expr j and expr k respectively hold. It distinguishes two cases:
either expr j holds on the left sub-interval (possibly a point interval) and
16 D. Della Monica et al.
expr k holds over the right one (necessarily not a point interval), or expr j
holds on the whole interval and expr k holds on its right endpoint (a point
interval). Notice that the latter covers the case where both ei and ej match
the empty string. The second conjunct constrains every expr j interval to
occur as a (not necessarily strict) prefix of an expr i interval and to be followed
by an expr k one. Similarly, the third conjunct constrains every expr k interval
to occur as a (not necessarily strict) suffix of an expr i interval and to be
preceded by an expr j one. In addition, the formula guarantees that expr j
and expr k do not intersect (except for intersections of a single point).
ϕexpr i = [G](expr i → hBi(expr j ∧ hAi(expr k ∧ hAiexpriend ∧
[B][A]¬expriend )) ∨ (expr j ∧ hAi(π ∧ expr k ))) ∧
[G]((hAiexpr j → hAiexpr i ) ∧ (hAi(expr j ∧ ¬π) →
hAi(expr i ∧ ¬π)) ∧ (expr j → [B](¬π → [A]¬expriend ) ∧
hAiexpr k )) ∧
[G](expr k → hAiexpriend ∧
[B](¬π → [A](¬expriend ∧ ¬expr j ∧ ¬exprjend )) ∧
(π ↔ exprjend ) ∧ (¬π ↔ hBiexprjend ) ∧
(hBiexpriend → expr i )).
∗
– If ei = ej , we distinguish three cases, depending on the number of repetitions
of the sub-string matched by ej in the string matched by ei , namely zero,
one, or more than one. They are encoded by the three disjuncts in the first
conjunct of the formula below. The rest of the formula guarantees that every
interval on which expr j holds occurs inside an interval on which expr i holds.
ϕexpr i = [G](expr i → π ∨ expr j ∨ (hBiexpr j ∧ [B](hAiexprjend →
hAi(¬π ∧ expr j )) ∧ hAiexprjend )) ∧
[init](hAiexpr j → hAiexpr i ∨ hBihAi(¬π ∧ expr i )) ∧
[G](hAiexpr j ∧ hBi(¬π ∧ expr i ) → hBi(¬π ∧ hAi(¬π ∧ expr i )))
∧ [G](hAiexpr j ∧ hAiexpriend → hAiexpr i )
∧ [G](hAi(¬π ∧ expr j ) ∧ hAiexpr i → hAi(¬π ∧ expr i ))
∧ [G](expr j → [B](¬π → [A]¬expriend )).
Vn Vn end
Let ϕR be the formula: expr n ∧ [A]π ∧ i=1 ϕexpr i ∧ i=1 ϕexpr i ∧
Vn 6∩
i=1 ϕexpr i . The following theorem holds [15].
Theorem 4. Let R be a regular expression over Σ. Then, L(R) = {w ∈ Σ ∗ :
w ≈ M for some model M such that M, [0, N ] |= ϕR ∧ ϕΣ }.
The encoding of regular expressions can be lifted to ω-regular ones. Let E
be an ω-regular expression. We can give it a finite tree structure in the same
way we did it for regular ones. As before, we list all the regular and ω-regular
sub-expressions e1 , . . . , en in increasing order of complexity with en = E.
Since we are forced to work with finite intervals, the formula encoding an
ω-regular expression intuitively behaves as follows. An ω-regular expression E
can be seen as the alternation (+) of a finite number of expressions of the form
Reω , i.e., E = R1 eω ω
1 + . . . + Rk ek , where, for all i, Ri is regular. The formula
ω
encoding the expression Ei = Re holds true on a certain finite prefix of N, that
represents the finite word captured by R, and it uses modality hAi to describe
Extended ω-Regular Languages and Interval Temporal Logic 17
properties of the infinite suffix. The encoding of E consists of the disjunction of
the formulas encoding the sub-expressions Ei . Formally, the encoding of an ω-
regular expression E into an AB formula is inductively defined as follows. As for
the regular sub-expressions, we proceed as above. Thus, we only need to specify
how to handle the ω-constructor, and alternation and concatenation when one
of the operands is an ω-regular expression.
– If ei = ej + ek , where ej and ek are ω-regular expressions, then ϕexpr i =
ϕexpr j ∨ ϕexpr k .
– If ei = ej ek , where ej is a regular expression and ek is an ω-regular one, then
ϕexpr i = ϕexpr j ∧ hAiϕexpr k .
– If ei = eωj , where ej is a regular expression, then
ϕexpr i = expr j ∧ hAi(¬π ∧ expr j ) ∧ [A](hAiexprjend → hAi(¬π ∧ expr j )).
Vn Vn Vn 6∩
Now, let ϕE be the formula: i=1 ϕexpr i ∧ i=1 ϕend expr i ∧ i=1 ϕexpr i . The
following theorem holds [15].
Theorem 5. Let E be an ω-regular expression over Σ. Then, L(E) = {w ∈ Σ ω :
w ≈ M for some model M such that M, [0, n] |= ϕE ∧ ϕΣ for some n ∈ N}.