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, satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics.
Introduction
the number of iterations of L to tend to infinity, i.e., for every k > 0, it
constrains the number of times the argument L is repeated at most k times to
be finite [
Interval temporal logic (ITL) is a general framework for representing and
reasoning about time. ITLs are characterized by high expressiveness (they
overcome 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
Propositional ITL (PITL), which was successfully applied to hardware specification
and verification [
The paper is organized as follows. First, we provide some background
knowledge. Then, we enrich the encoding of !-regular languages into AB given in [
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 [
Extended regular expressions differ from regular ones as they allow constructors from the set f(:)B; (:)S; (:)T g. 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 n f0g. For an infinite
sequence u of finite words over and i 2 N+, we denote by ui its i-th element.
The basic shuffle operation is defined as follows [
The semantics of extended regular expressions over is defined as follows: – L(;) = ;; – for a 2 , L(a) only contains the infinite sequence of the one-letter word a, that is, L(a) = f(a; a; a; : : :)g; – L(e1 e2) = fw j 8i:wi = ui vi; u 2 L(e1); v 2 L(e2)g; – L(e1 + e2) = fw j w is a shuffle of u and v, for some u; v 2 L(e1) [ L(e2)g; – L(e ) = f(uf(0)u2 : : : uf(1) 1; uf(1) : : : uf(2) 1; : : :) j u 2 L(e) and f : N !
N+ is a nondecreasing function with f (0) = 1g; – L(eB) = f(uf(0)u2 : : : uf(1) 1; uf(1) : : : uf(2) 1; : : :) j u 2 L(e) and f : N ! N+ is a nondecreasing function, with f (0) = 1, such that 9n 2 N 8i 2 N:(f (i + 1) f (i) < n)g; – L(eS ) = f(uf(0)u2 : : : uf(1) 1; uf(1) : : : uf(2) 1; : : :) j u 2 L(e) and f : N ! N+ is a nondecreasing function, with f (0) = 1, such that 8n 2 N 9k 2 N 8i > k(f (i + 1) f (i) > n)g; – L(eT ) = f(uf(0)u2 : : : uf(1) 1; uf(1) : : : uf(2) 1; : : :) j u 2 L(e) and f : N ! N+ is a nondecreasing function, with f (0) = 1, such that 9!n 2 N 8k 2 N 9i > k:(f (i + 1) f (i) = n)g.
Given a sequence v = (uf(0)u2 : : : uf(1) 1; uf(1) : : : uf(2) 1; : : :) 2 eop , with u 2 L(e) and op 2 f ; B; S; T g, we define the sequence of exponents of e in v, denoted by N (v), as the sequence f (i+1) f (i) i2N. 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!) = fw j jwj = 1 and w = u1u2u3 : : : for some u 2 L(e)g.
!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 j R E j e! where R is a
regular 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)=fu v j u 2 L(E1); v 2 L(E2)g).5 As we did for languages of word
sequences, we will sometimes omit the operator between word languages.
Interval temporal logics AB, ABA, AB , and ABA . Syntax and
semantics of AB, ABA, AB , and ABA are defined as follows. AB features
modalities 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 [
ABA is obtained from AB by adding the (past) modality hAi for the Allen
relation met by (A). Unlike what happens with point-based temporal logics,
the addition of past operators to interval ones usually increases both their
expressiveness and their computational complexity (see, e.g., [
AB is obtained from AB by adding an equivalence relation over the
points of the model. Similarly to ABA, the satisfiability problem for AB
remains decidable over finite linear orders, but it becomes non-primitive
recursive, while decidability is lost over N [
Hereafter, we use modalities [G] (globally in the future) and [init ](every initial 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 [
Let = (an)n2N be a sequence of natural numbers. We define a grouping of as a sequence of natural numbers (bn)n2N such that bn = Pif=(nf+(n1)) 1 ai, where f : N ! N, with f (0) = 0, is an increasing function (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)n2N of . Then, for every i 2 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 sequence 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 inductively a formula 'expri . Finally, we capture the language L(E) with the formula 'E = Vin=1 'expri ^ Vin=1 'eexnpdri ^ Vin=1 '6e\xpri : The only missing ingredient is a way to recursively define formulas 'expri for ei of the forms ejB, ej , and ejT . These formulas are conjunctions of two sub-formulas,
S a local one, that is the same we defined in the case ei = ej , 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 = ejB 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 = ejS and ei = ejT ). This is the case, for instance, with expressions like (aBb + 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 aBb. 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. exprn exprn exprn exprn expri expri expri expri expri
pj pj pj pj pj pj… p…j … … pj… … … … … … … … … … … … … … … … … … … … … … … … … exprnend hAiexpri exprjend expriend hAiexpri exprjend phj hAipj exprjend blj exprjend expriend Fig. 1: Example of the structure we are enforcing by means of formula (Bi;j) for an expression E = (en)!, where en contains the sub-expression ei = ejB (dashed intervals represent expr j intervals). !B-regular languages in ABA. Let B(E)=f(i;j) : ei=ejB is a sub-expression of Eg. To force the proper behaviour of the B-constructor, for every (i;j)2B(E), we introduce the additional proposition letters phj ; blj ; and pj , which can be exploited to express (by means of suitable ABA 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 2 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 ! hAihAipj ): 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 fn0; n1; : : :g 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 j[n0; n1]phj j j[n1; n2]phj j : : :, 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. 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 j[n0; n1]phj j 2 many expr j intervals, thus providing a bound, as required by the B-constructor.
Now, for every (i; j) 2 B(E), let formulas and (i;j) = [G]hAihAiexpr i ! B (i;j) be the conjunction of the above B (i;j).
B (i;j) for some n 2 Ng: (i;j)2B(E) B Theorem 1. Let E be an !B-regular expression over . Then, L(E) = fw 2 ! : w M for some model M such that M; [0; n] j= 'E ^ ' ^ V !S-regular languages in AB . Let S(E)=f(i;j) : ei=ejS is a sub-expression of Eg. To force the proper behaviour of the S-constructor, we make use of the equivalence relation and, for all (i; j) 2 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 iend); 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 j[n; n0]jphj = jfx : n < x < n0; x is a phj point gj 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 j[n0; n00]jphj ; j[n1; n01]jphj ; : : : 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 2 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 exprn expri expri expri
exprn expri expri 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 ! : ).
For all (i; j) 2 S(E), let (Si;j) be the conjunction of the above formulas. Theorem 2. Let E be an !S-regular expression over . Then, L(E) = fw 2 ! : w M for some model M such that M; [0; n] j= 'E ^ ' ^ V(i;j)2S(E) (Si;j) for some n 2 Ng: !T -regular languages in ABA . Let T (E)=f(i; j) : ei=ejT is a sub-expression of Eg. To encode !T -regular languages in ABA , we first show that a particular class of models over N can be captured by ABA formulas (1i;j), for (i; j) 2 T (E). Then, we use such a formula to constrain the behaviour of (:)T .
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 characterize, through (1i;j), 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 ^ hAi(hBiblj ^ [B][A]:conf j ) ! hAipj ); 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[A]: )); 8. if (x; y) and (x0; y0) are two pairs of blj points, with x < y < x0 < y0, 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 y0, 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 ^ hAi( ^hBihAiblj ) ! hAiqj ):
Let (1i;j) be the conjunction of the above formulas. A graphical account of the structure enforced by (1i;j) 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 . (1i;j).
Thanks to (1i;j), a model can be seen as an infinite sequence of configurations [conf j0; conf j1]; [conf j1; conf j2]; ::. For every x 2 N, conf jx contains a finite sequence of n(x) + 1, with n : N ! N, sets Sbljx;0; : : : ; Sbljx;n(x) 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 2 f0; : : : ; n(x)g. Formally, Sbljx;y = fn 2 N : M; [n; n] j= phj ; jfn0 < n : M; [n0; n0] j= conf j gj = x + 1; jfn0 < n : M; [n0; n0] j= blj ; 8n00(n0 < n00 < n ! M; [n00; n00] 6j= conf j )gj = yg. Intuitively, n(x) + 1 is the number of blocks in [conf x; conf x+1] and jSbljx;yj 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); (P2) for all x; y; y0 2 N, with 0 y < y0 n(x), jSbljx;yj > jSbljx;y0 j (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] = Sk2N Sbljx+k;yk (property 6) and jSbljx;y0 j jSbljx+1;y1 j : : : (property 8); (P 3) states that, for every equivalence class [w] of phj points, there is a configuration 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] = Sk2N Sbljx+k;yk . Since the number of points in each block is finite, there is k0 2 N for which jSbljx+k0;yk0 j = jSbljx+k0+1;yk0+1 j = : : :, i.e., the sequence of Sbljx+k;yk cardinalities 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. Lemma 1. If M; [0; 0] j= (1i;j), then there exists an infinite subset N of N such that for every n 2 N there is w 2 N with val([w] ) = n.
An instantiation of an equivalence class with an expr i interval is a correspondence 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 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 pointsj([x; y]) = fz : x z y; 9z0(M; [z; z0] j= expr j)g, and, for a phj point w, let Seq([w] ) = (x; y0); (x + 1; y1); : : : be the sequence such that [w] = Sk2N Sbljx+k;yk . In what follow, we define a formula inj , which uses proposition letter inj to force that, for every equivalence class [w] of phj points, there is an infinite sub-sequence (x0; y0); (x1; y1); : : : of Seq([w] ) such that for every h 2 N there is a distinct expr i interval [x0h; yh0] with pointsj([x0h; yh0]) = jSbljxh;yh j, 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 ^ [A]([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) be T For (i; j)2S(E), let inj be the conjunction of the above formulas and hAi[A][A]:expr i _ [G]hAihAi( ^ expr i ^ expr j) _ (1i;j) ^ inj ^ [G]hAihAi( ^ expr j) ^ hBihAihAiinj^
^ [G](inj ! hAi(hBihAiconf j ^ inj)) _ (1i;j) ^ inj ^ hAi[A][A](expr j ! : ) ^ [G](phj ! hAi(: ^ ^hAiinj)) (i;j) for some n 2 Ng: V(i;j)2T (E) T Theorem 3. Let E be a !T -regular expression over . Then, L(E) = fw 2 ! : w M for some model M such that M; [0; n] j= 'E ^ ' ^ 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 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 logics, that preserve (un)satisfiability of the resulting formulas and behave better from a computational point of view.
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 [
To begin with, we show how to interpret words and !-words as interval temporal models, and vice versa. For a word w = w0w1 : : : 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 = jwj + 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]) \ = fwig for every i < jwj.
Let R be a regular expression on . We show how to encode R into an ABformula 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 :
' = [G] unit $ Wa2 a ^ Va2 a ! Vb2 nfag :b :
The regular expression R can be given a tree structure, whose leaves and internal nodes belong to and f+; ; g, respectively. Each sub-tree identifies a sub-expression of R. Let e1; : : : ; en be all the sub-expressions of R, including 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, every expriend is the ending point of an expr i interval. This is formalized by the following formula: 'eexnpdri = [G]((expriend ! ) ^ (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 intersections of a single point):
'6e\xpri = [G](expr i ! [B](: ! [A](:expr i ^ :expriend ))):
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 'expri by induction on the complexity of expressions ei.
– If ei = a for some a 2 , we put 'expri = [G](expr i ! a). – If ei = ", we put 'expri = [G](expr i ! ). – If ei = ej + ek, we put 'expri = [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 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). 'expri = [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. 'expri = [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(: ^ [G](hAiexpr j ^ hAiexpriend ! hAiexpr i) ^ [G](hAi(: ^ expr j) ^ hAiexpr i ! hAi(: ^ expr i)) ^ [G](expr j ! [B](: ! [A]:expriend )): Let 'R be the formula: expr n ^ [A] Vin=1 'eexnpdri ^ ^ expr i))) Theorem 4. Let R be a regular expression over . Then, L(R) = fw 2 w M for some model M such that M; [0; N ] j= 'R ^ ' g: :
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 = R1e1! + : : : + Rkek , 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 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 'expri =
'exprj _ 'exprk .
– If ei = ejek, where ej is a regular expression and ek is an !-regular one, then
'expri = 'exprj ^ hAi'exprk .
– If ei = ej!, where ej is a regular expression, then
'expri = expr j ^ hAi(: ^ expr j) ^ [A](hAiexprjend ! hAi(: ^ expr j)):
Now, let 'E be the formula: Vin=1 'expri ^ Vin=1 'eexnpdri ^ Vin=1 '6e\xpri . The
following theorem holds [
Theorem 5. Let E be an !-regular expression over . Then, L(E) = fw 2 w M for some model M such that M; [0; n] j= 'E ^ ' for some n 2 Ng. ! :