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}.