9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Vectorial languages and linear temporal logic

Theoretical Computer Science 310 (2004) 79 – 116

www.elsevier.com/locate/tcs

Vectorial languages and linear temporal logic

Olivier Serre

LIAFA, Universit? e Paris VII 2, place Jussieu, case 7014 F-75251 Paris Cedex 05, France Received 1 June 2002; received in revised form 15 May 2003; accepted 27 May 2003 Communicated by D. Perrin

Abstract Determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. The main di culty is to do this computation e ciently. Considering words as vectors and working on them using vectorial operations allows to solve the problem faster than using local operations. In this paper, we show ?rst that the set of vectorial operations needed by an algorithm representing a given automaton depends on the language accepted by the automaton. We give precise characterizations for star-free, solvable and regular languages using vectorial algorithms. We also study classes of languages associated with restricted sets of vectorial operations and relate them with languages de?ned by fragments of linear temporal logic. Finally, we consider the converse problem of constructing an automaton from a given vectorial algorithm. As a byproduct, we show that the satis?ability problem for some extensions of LTL characterizing solvable and regular languages is PSPACE-complete. c 2003 Elsevier B.V. All rights reserved.

Keywords: Parallel automata simulation; Linear temporal logic and extensions

1. Introduction Given a deterministic complete automaton and an input word, a classical question is to decide whether or not the automaton accepts the word. A more detailed information is the sequence of visited states while processing the word. Computing this sequence is the core of important problems such as approximate string matching. An easy way to solve this problem consists in simulating the run of the automaton (which is

E-mail address: serre@liafa.jussieu.fr (O. Serre). 0304-3975/03/$ - see front matter c 2003 Elsevier B.V. All rights reserved. doi:10.1016/S0304-3975(03)00346-3

80

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

deterministic and complete) on the input word. However, approximate string matching is generally used on very long sequences (as genomic ones) and the natural algorithm, which is linear in the length of the input word, is not performing enough. A natural solution to accelerate the computation is to consider words as vectors and therefore to compute the sequence of visited states using vectorial operations, that can be e ciently achieved using parallelism. In this paper, we are interested in vectorial algorithms, that were introduced and investigated by Bergeron and Hamel [2,3]. Such an algorithm computes the sequence of visited states while reading a word using a ?nite number (independent of the length of the word) of vectorial operations. The existence of an algorithm for a given automaton depends on the automaton and on the kind of vectorial operations we allow. The problem can also be studied from the language point of view: can we ?nd a deterministic complete automaton recognizing a given language and an associated vectorial algorithm? We ?rst exhibit a very tight connection between temporal logic operators and some vectorial operations, that will therefore be called PTL-vectorial operations. This leads to an alternative proof of the equivalence between star-free languages and vectorial algorithms, whose direct inclusion was ?rst established in [3]. Then, we describe extensions of these algorithms, ?rst to capture a larger subclass of regular languages, the solvable ones, and ?nally for the whole class of regular languages. In the second part of the paper, we investigate fragments of algorithms based on the set of PTL-vectorial operations. Here, we want to know which subset of star-free languages can be characterized by forbidding certain vector operations. We show that these fragments are closely related with the fragments of past temporal logic de?ned and characterized in [4,14,15]. Finally, we consider the converse problem, that is we want to check for a given vectorial algorithm whether there exists an automaton associated with it. To solve this problem, we show how to decide the satis?ability of formulas belonging to extensions of linear temporal logic introduced in [1]. Our constructions are based on alternating automata. 2. Notations and de?nitions Throughout the paper, vectors are noted in bold characters (e.g. u) and are considered as words. Conversely, vectorial operations can be applied to words, considering them as vectors. Therefore, a word u is associated with a canonical vectorial representation u and a vector v is associated with a canonical word representation v. Let A = (Q; A; ·; q0 ; F ) be a deterministic complete automaton. With each input vector u = a1 a2 · · · am we associate the output vector r = r1 r2 · · · rm representing the sequence of states reached reading u (we omit the leading initial state). Therefore, u and r have the same length. For instance, consider the automaton given in Example 1. With the input vector u = bbaabbbababab we associate the output vector r = 2311233121212. A vectorial algorithm for A consists of a sequence of vectorial operations of ?xed length (i.e., a straight-line expression of length which is independent on u) computing r from u.

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

81

Given a word u = a1 a2 · · · am , we consider for every letter a ∈ A, the boolean vector (u = a) = (a1 = a) · · · (am = a), where (a1 = a) is a boolean whereas the equality sign after (u = a) represents an assignment. Hence, (u = a) is the characteristic boolean vector of the letter a in the word u. Just as for words, for any state q ∈ Q, with an output vector r = r1 r2 · · · rm we associate the boolean vector (r = q) = (r1 = q) · · · (rm = q), that is the characteristic vector of state q. For example, (bbaabbbababab = a) = 0011000101010 and (2311233121212 = 1) = 0011000101010. The sequence (u = a)a∈A (respectively, the sequence (r = q)q∈Q ) is an equivalent boolean representation for the input word u (respectively, for the output vector r). In fact, in order to work only on boolean vectors, the vectorial algorithms presented in this paper compute the sequence of characteristic vectors (r = q)q∈Q from the sequence of characteristic vectors (u = a)a∈A . Let be a class of vectorial operations. Vectorial algorithms based on this set of operations and on the bit-wise logical operations (combinations of ∨; ∧ and ?) are called -vectorial algorithms. A deterministic complete automaton is called -vectorial if there is an -vectorial algorithm computing the sequence (r = q)q∈Q from the sequence (u = a)a∈A . Finally, a language is -vectorial if it is recognized by a deterministic complete -vectorial automaton. Proposition 1 below shows that minimization preserves the property of being an -vectorial automaton. Therefore, a language is -vectorial if and only if its minimal automaton is -vectorial (by minimal automaton we always mean the minimal complete automaton). This property is very useful, because to decide whether or not a language is -vectorial, it su ces to know how to decide whether or not a given automaton (the minimal one) is vectorial. Proposition 1. Let A be a deterministic complete automaton. If A is then its minimal automaton Amin is also -vectorial. -vectorial,

Proof. As A is deterministic and complete, the states of Amin correspond to the Nerode equivalence classes of states of A. An expression characterizing a state of the minimal automaton is obtained as the disjunction of the expressions for the states of the associated equivalence class. To make our algorithms precise we have to state which vectorial operations are allowed. As in [3], we ?rst consider a basic set of vectorial operations: ? Bit-wise logical operations such as ∨; ∧; ? and the atomic formulas (u = a) = (u1 = a) · · · (um = a). ? Right shift: ↑i u1 · · · um = iu1 · · · um?1 ; i ∈ {0; 1}. ? Binary addition between two vectors of same length: we perform the usual binary addition from left to right but we do not keep the highest bit (carry) if the length of the result exceeds the initial vectors’ ones. For example ↑0 110101 + 101011 = 110100. vectorial algorithms using only these operations will be called in this paper PTLvectorial algorithms. PTL stands for Past Temporal Logic and we will show that there exists a close relation between vectorial operations of this kind and past temporal logic operators. A language is therefore a PTL-vectorial language if its minimal automaton is PTL-vectorial.

82

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

Example 1 (Bergeron and Hamel [2]). The language recognized by the following automaton is a PTL-vectorial language.

Actually, the state to which a word leads depends only on the last two letters of the word: if the last letter is a the state is 1, if the length 2 su x is ab or if we are working on the ?rst letter of the word and this letter is b (in this case we cannot consider the length 2 su x) the state is 2 and otherwise it is 3. Therefore, we have the following PTL-vectorial algorithm for this automaton: ? ? ? (r = 1) = (u = a) r = (r = 2) = (u = b)∧ ↑1 (u = a) ? ? (r = 3) = (u = b)∧ ↑0 (u = b) 3. Past temporal logic The main result of the next section states that a language is a PTL-vectorial language if and only if it is star-free. Recall that a language is star-free if and only if its syntactic monoid is aperiodic [9]. Furthermore a language is star-free if and only if it can be de?ned by ?rst-order logic of the linear order FO[?] [5,6]. Our proof relies a third characterization in terms of past temporal logic (PTL). We ?rst recall the syntax of PTL: We use atomic propositions pa for each letter a ∈ A of a given alphabet A, boolean connectives (∨ and ?) and past temporal operators (Yesterday, denoted Y, and Since, denoted S). The formulas are constructed inductively according to the following rules: (1) For every a ∈ A; pa is a formula. (2) If ’1 and ’2 are formulas, so are ’1 ∨ ’2 ; ?’1 ; Y’1 and ’1 S’2 . Semantics is de?ned by induction on the rules. Given a word w ∈ A+ and an integer n ∈ {1; 2; : : : ; |w|}, we de?ne that “w satis?es ’ at position n”, denoted (w; n) |= ’, as follows: (1) (w; n) |= pa if the nth letter of w is a. (2) (w; n) |= ’1 ∨ ’2 if (w; n) |= ’1 or (w; n) |= ’2 . (3) (w; n) |= ?’1 if (w; n) |= ’1 . (4) (w; n) |= Y’1 if n?1 and (w; n ? 1) |= ’1 .

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

83

(5) (w; n) |= ’1 S’2 if there exists m6n such that (w; m) |= ’2 and, for every k such that m?k 6n; (w; k ) |= ’1 . With each PTL-formula ’, we associate the language of ?nite words satisfying ’: L’ = {u ∈ A+ | (u; |u|) |= ’}: Recall that a regular language L is star-free if and only if there exists a PTL-formula ’ such that L = L’ (see for instance [4]), i.e. if and only if L is PTL-de?nable. 4. PTL-vectorial languages are equivalent to star-free languages Our aim in this section is to prove the following characterization: Theorem 1. A regular language is star-free if and only if it is PTL-vectorial. The equivalence between PTL-de?nable languages and star-free languages implies that Theorem 1 is equivalent with the following result: Theorem 2. A regular language is PTL-vectorial if and only if it is PTL-de?nable. The proof of this result is splitted into two parts: passing from PTL-formulas to PTLvectorial algorithms and from PTL-vectorial algorithms to PTL-formulas. The ?rst part is done in Section 4.1 and the second one in Section 4.2. 4.1. Star-free languages are PTL-vectorial Let L be a star-free language and let A = (Q; A; ·; q0 ; F ) be its minimal automaton. Since L is star-free, A is counter-free (note that this property is independent from the ?nal states). Let q be a state of A, then the language Lq = {u | (u; |u|) |= ’} is recognized by an automaton obtained from A by letting q be the unique ?nal state. Therefore, Lq is star-free (because it is recognized by a counter-free automaton) and thus PTL-de?nable: there exists a PTL-formula ’q such that q0 · u = q if and only if (u; |u|) |= ’q . We will show that for any input vector u = a1 · · · am and any PTL-formula ’, the computation of the binary vector v = v1 · · · vm , where vi = 1 if and only if (e1 · · · ei ; i) |= ’, can be performed by a PTL-vectorial algorithm . The de?nition of is given by induction on ’: (1) If ’ = pa then = (u = a). (2) If ’ = ’1 ∨ ’2 then = 1 ∨ 2 , where 1 and 2 are associated, respectively, with ’1 and ’2 . (3) If ’ = ?’1 then = ? 1 , where 1 is associated with ’1 . (4) If ’ = Y’1 then = ↑0 1 , where 1 is associated with ’1 . (5) If ’ = ’1 S’2 , then = 2 ∨ [(↑0 2 ) ∧ 1 ] ∨ [ 1 ∧ carry( 1 ; (↑0 2 ) ∧ 1 )], where 1 and 2 are associated, respectively, with ’1 and ’2 .

84

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

The formula carry(v; w) is an abbreviation for: ?[(v ⊕ w) = (v + w)], where ⊕ is the exclusive-or operator. Therefore, carry(v; w) represents the value of the carry bit when adding v and w. For instance, carry(101101; 100110) = 010011. Let us justify the construction for the since operator, (5). A word u is such that (u; n) |= ’1 S’2 in one of the three cases: (i) (u; n) |= ’2 . This case is treated by the algorithm 2 . (ii) (u; n?1) |= ’2 and (u; n) |= ’1 . This case is treated by the algorithm [(↑0 2 ) ∧ 1 ]. (iii) There is an integer m?n ? 1 (which is chosen maximal) such that (u; m) |= ’2 and, for all k such that m?k 6n; (u; k ) |= ’1 . The vector carry( 1 ; (↑0 2 ) ∧ 1 ] is such that its nth position is 1 if and only if there exists m?n ? 1 such that (u; m) |= ’2 and, for all k such that m?k 6n ? 1; (u; k ) |= ’1 . Consequently, the algorithm 1 ∧ carry( 1 ; (↑0 2 ) ∧ 1 ) exactly characterizes our case. Note that the ?rst component 1 is necessary because the carry has a non-immediate e ect: it a ects the ?rst position after it is generated. For the same reason, the second case had to be treated separately. This inductive construction concludes the proof that any star-free language is PTLvectorial. The following example illustrates the preceding cases for the value (u) of applied to a vector u: ↑0 [

2 (u)] 2 (u)

1 (u) [(↑0 2 ) ∧ 1 ] (u) [carry( 1 ; (↑0 2 ) ∧ 1 )] (u) [ 1 ∧ carry( 1 ; (↑0 2 ) ∧ 1 )] (u) (u)

= = = = = = =

00100100; 00010010; 11011101; 00010000; 00001110; 00001100; 00111100:

4.2. PTL-vectorial languages are star-free Let L be a PTL-vectorial language. By Proposition 1, its minimal automaton A = (Q; A; ·; q0 ; F ) is a PTL-vectorial automaton. To prove that L is star-free (equivalently, PTL-de?nable) we construct for each state q of A, a PTL-formula ’q such that for any word u ∈ A+ ; q0 · u = q if and only if (u; |u|) |= ’q . Therefore, L will be characterized by the disjunction q∈F ’q , which is a PTL-formula. For each state q of A we have a PTL-vectorial algorithm q computing, from each input vector u, the characteristic output vector of state q; (r = q). The formula ’q which “translates” q is de?ned by induction on the structure of q . Moreover, the logical formula ’ as de?ned below for a vectorial algorithm , satis?es the following property: the ith entry of the vector obtained by applying to u is 1 if and only if (u; i) |= ’. (1) If = (u = a), where a is a letter, then ’ = pa . (2) If = 1 ∨ 2 then ’ = ’1 ∨ ’2 , where ’1 and ’2 are associated, respectively, with 1 and 2 . (3) If = ? 1 then ’ = ?’1 , where ’1 is associated with 1 .

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

85

(4) If = ↑0 1 then ’ = Y’1 , where ’1 is associated with 1 . The case follows from the preceding one, because ↑1 1 = ?(↑0 ? 1 ). (5) If = 1 + 2 , we let c = Y{[’1 ∨ ’2 ] S [’1 ∧ ’2 ]};

= ↑1

1

where ’1 and ’2 are associated, respectively, with 1 and 2 . Note that the formula c characterizes the value of the carry bit while summing the vectors obtained from 1 and 2 . Thus, the translation of 1 + 2 is the logical formula: ’ = [’1 ⊕ ’2 ] ? ?c: Finally, the global formula for L is ’A =

q∈F

’q ;

and for each word u, we have u ∈ L = L(A) if and only if (u; |u|) |= ’A . This concludes the proof. 5. Extensions of PTL-vectorial algorithms A natural question is to extend PTL-vectorial algorithms, in order to capture larger classes of regular languages by parallel operations. To achieve this goal we need to introduce new operations that are strictly more powerful than the PTL operations. In a ?rst extension we will characterize solvable regular languages (a regular language is called solvable if its syntactic monoid does not contain any non-solvable group) and in a second extension all regular languages. 5.1. A vectorial characterization of solvable languages The crucial point in de?ning extensions of PTL-vectorial algorithms is the choice of the new operations allowed. To determine them, let us give another proof of the fact that PTL-vectorial languages are star-free. A well known example of non-star-free language is L1 = (aa)? whereas, on the alphabet A = {a; b}; L2 = (ab)? = A? \[bA? + A? a + A? (aa + bb)A? ] is a star-free one. Is there a “vectorial” di erence between them? L1 and L2 are recognized by the following automata:

Recall that a period of a word u = a1 a2 · · · an is an integer p6n= 2 such that for any position i; 16i6n ? p; ai+p = ai . A word having period p is said to be of periodicity p. For example abbaabbaabbaab is of periodicity 4. Finally, a word is ultimately pe-

86

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

riodic of period p if it has a su x of periodicity p. For instance, abbbababababababab is ultimately periodic of period 2. Words recognized by A1 are of periodicity 1 whereas the associated sequence of states is of periodicity 2. This is not the case for the automaton A2 . One can show that any PTL-vectorial algorithm applied to an ultimately periodic word gives an ultimately periodic result of the same period (PTL-vectorial operations preserve periods). With any non-counter-free automaton one can associate an ultimately periodic word of period p such that the associated sequence of states is not of ultimate period p. Thus, a PTLvectorial language has to be star-free. To extend PTL-vectorial algorithms, we need to introduce operators that do not preserve the period. For every integers k; l such that 06l?k , the modular operator Sl; k is de?ned by ? i ? ? 1 if xj = l (mod k ); j =1 Sl;k (x1 x2 · · · xm ) = (s1 · · · sm ) where si = ? ? 0 otherwise: vectorial algorithms using only the PTL-vectorial operations plus the modular operations Sl; k will be called MTL-vectorial algorithms. A language is an MTL-vectorial language if there is an MTL-vectorial algorithm for a deterministic complete automaton which recognizes it. With modular operators, one can easily de?ne MTL-vectorial algorithms for the minimal automaton of languages of the form L(a; k; pn ) = {u ∈ A? | |u|a ≡ k (mod pn )}, where a is a letter, |u|a is the number of occurrences of a ∈ A in u; p a prime number and k; n strictly positive numbers. Since MTL-vectorial languages are a boolean algebra (just consider the product automaton to compute an algorithm for intersection or union of two MTL-vectorial languages) and languages of the form K (a; r ) = {u ∈ A? | |u|a = r } are PTL-vectorial (since star-free), the boolean algebra MCom generated by languages K (a; r ) and L(a; k; pn ), which is the set of languages whose syntactic monoid is commutative [7], is a subset of MTL-vectorial languages. For characterizing the family of solvable languages we need a further operation on automata, the cascade product. Let A be a ?nite alphabet and let B1 = (Q1 ; A; 1 ) and B2 = (Q2 ; Q1 × A; 2 ) be two ?nite automata. Their cascade product C = (Q; A; ), denoted B1 ? B2 is de?ned as follows: ? Q = Q1 × Q2 , ? ( q1 ; q2 ; a) = 1 (q1 ; a); 2 (q2 ; q1 ; a ) . We can also de?ne the cascade product of more than two automata by the following recursive formula: B1 ? B2 ? · · · ? Bk = (: : : ((B1 ? B2 ) ? B3 ) ? · · ·) ? Bk : This automata version of the wreath product [8] of aperiodic semigroups, combined with the Krohn–Rhodes Decomposition Theorem [12], was used to construct PTLvectorial algorithms from counter-free automata [2]. It is not di cult to prove that a family of automata corresponding to a class of vectorial algorithms, for instance

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

87

counter-free automata or automata recognizing MTL-vectorial languages, is closed under cascade product and under homomorphisms. Therefore, as all star-free languages are MTL-vectorial languages, any language recognized by an automaton obtained by applying a homomorphism to a cascade product of counter-free automata and automata recognizing languages in MCom is an MTL-vectorial language. In addition, any solvable language is recognized by an automaton obtained by applying an homomorphism to a cascade product of counter-free automata and automata recognizing languages in MCom [11], and therefore this proves that solvable languages are MTL-vectorial languages. In fact, the converse is true as well, any MTL-vectorial language is a solvable language. We have thus the following result: Theorem 3. A regular language is solvable if and only if it is MTL-vectorial. For the proof, we use an extension of the past temporal logic introduced in [1], the modular temporal logic (MTL). By modular temporal logic we mean past temporal logic augmented with the unary operators Mod l; k for integers 06l?k . The new modular operators have the following natural semantics: given an MTL formula ’, we have (u; i) |= Mod l; k ’ if, there are l positions i ; 16i 6i (mod k ) such that (u; i ) |= ’. It was shown in [1] that a language is expressible in modular temporal logic if and only if it is solvable. But, with an MTL-vectorial language one can associate an MTL formula in a straightforward way. This shows that MTL vectorial languages are solvable languages and achieves the proof of the equivalence between MTL-vectorial languages and solvable languages. Moreover, as solvability is a syntactic property, the property of being an MTL-vectorial language does not depend actually on a speci?c automaton recognizing the language. 5.2. A vectorial characterization of regular languages MTL-vectorial algorithms do not characterize all regular languages. Therefore, we propose an extension to MTL-vectorial algorithms, which we denote as GTL-vectorial algorithms, which captures all regular languages. We will use again an extension of modular temporal logic introduced in [1]. This extension of temporal logic is obtained by augmenting modular temporal logic with group temporal operators g;G for any ?nite group G and any element g ∈ G . The operator g;G always binds |G | ? 1 formulas. Let us now explain the semantics of g;G for a given ?nite group G and an element g ∈ G . We ?rst have to order the elements of the group G (this order will not be modi?ed afterward), say as g1 ; g2 ; : : : ; gq = id. Let u be an element of A+ and let ’1 ; ’2 ; : : : ; ’q?1 be GTL-formulas. With each j; 16j 6|u| we associate an element of G , denoted ’1 ; ’2 : : : ’q?1 u; j , de?ned by ’1 ; ’2 ; : : : ; ’q?1 u; j = gk ; where k = min{l | (u; j ) |= ’l } with the convention that min ? = q.

88

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

Finally, we de?ne (u; i) |=

i j =1

g;G

’1 ; ’2 ; : : : ; ’q?1 to mean that

’1 ; ’2 ; : : : ; ’q?1 u; j = g:

It was shown in [1] that a language is expressible in group temporal logic if and only if it is regular. Thus, to have a vectorial characterization of all regular languages it su ces to ?nd vectorial operations equivalent to g;G for all ?nite groups G . Let G be a ?nite group of cardinality q. We consider an isomorphic copy H of G de?ned as follows. The elements of H are boolean vectors of length q containing exactly one 1. Therefore, (1; 0; : : : ; 0) is associated with g1 ; (0; 1; 0; : : : ; 0) with g2 and so on. The product × on H is de?ned by the isomorphism between G and H . For each group G and each element g ∈ G , we introduce the operator P g;G de?ned by ? i ? ? 1 if (v1;j ; v2;j ; : : : ; vq;j ) = (g); j =1 Pg;G (v1 ; v2 ; : : : ; vq ) = (s1 : : : sm ) with si = ? ? 0 otherwise; where we mean by an iteration of × and by vk; j the j th bit of vector vk .

Remark 1. In our de?nition of P g;G , we implicitly suppose that for each j; 16j 6i , there is exactly one vector vk such that vk; i = 1. If this is not the case, we have a problem in de?ning the product because some (v1; j ; v2; j ; : : : ; vq; j ) do not belong to H . The solution consists in de?ning the product ×, and thus the iterated product , for all boolean vectors of length q. To achieve this we de?ne an equivalence relation ? for boolean vectors saying that x ? y if and only if x and y have their ?rst 1 in the same position. In addition, the vector (0; 0; : : : ; 0) is equivalent to the neutral element (0; 0; : : : ; 0; 1). Finally we de?ne × for all vectors using the equivalence relation ?. The equivalence relation ? works like the operator ’1 ; ’2 ; : : : ; ’q?1 , it just looks for the ?rst 1 (validate formula) that appears on the vector. Therefore, with ’ = g;G (’1 ; : : : ; ’q?1 ) we associate = Pg;G (

1; 2; 3; : : : ; q?1 ; ? 1

∧ ··· ∧ ?

i j

q?1 );

where i is the translation of ’i . Denoting by algorithm i applied to u we then have ( ’1 ; ’2 ; : : : ; ’q?1 u; j ) ?(

j 1 (u); j 2 (u); j 3 (u); : : : ; j q?1 (u); ?

(u) the j th bit of the result of the

j 1 (u)

∧ ··· ∧ ?

j q?1 (u))

and therefore we have (u; i) |= ’ if and only if the ith bit of the result of to u is 1. Conversely, with = P g;G ( 1 ; : : : ; q ) we associate ’=

g;G [’1 ; ’2 ; ’3 ; : : : ; ’q?1 ];

applied

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

89

where ’i is the translation of i applied to u we obtain

j 1 (u); j 2 (u); j 3 (u); : : : ;

i.

Denoting again by

j 1 (u)

i

j

(u) the j th bit of the result of

j q?1 (u))

j q?1 (u); ?

∧ ··· ∧ ?

? ( ’1 ; ’2 ; : : : ; ’q?1 u; j ) and therefore the ith bit of the result of applied to u is 1 if and only if (u; i) |= ’. Thus, the operators g;G and P g;G have the same expressive power. We can now characterize all regular languages by vectorial algorithms. Vectorial algorithms using only the MTL-vectorial operations plus the group operations P g;G will be called GTLvectorial algorithms. A language is a GTL-vectorial language if there is a GTLvectorial algorithm for a deterministic complete automaton which recognizes it. Combining the preceding results, we have the following characterization of regular languages: Theorem 4. A language is regular if and only if it is GTL-vectorial. E ectively, a GTL-vectorial language is regular (because it is recognized by a ?nite automaton). Conversely, to any regular language one can associate a ?nite deterministic complete recognizing it. To any state of the automaton, one can associate a regular language (and thus a GTL-formula) representing the set of words that lead to this state in the automaton. Translating these GTL-formulas gives us a GTL-vectorial algorithm for the automaton. Hence any regular language is a GTL-vectorial language. Regularity being a syntactic property, the property of being a GTL-vectorial language does not depend actually on a speci?c automaton. 6. Fragments of PTL-vectorial languages In the preceding sections we attempted to extend PTL-vectorial algorithms to characterize regular languages more complex than star-free ones. For that we needed new vectorial operators. However, the price to pay is that the extended vectorial operations are not obviously realizable from a hardware point of view. A dual investigation is to study fragments of PTL-vectorial languages: given a set of vectorial operators (that can be e ciently performed) we want to determine which kind of (deterministic complete) automata can be characterized by algorithms using the given set of vectorial operations. A similar problem has been studied for temporal logic in [4,14,15] and we will relate it to our problem. 6.1. De?nitions We ?rst introduce a new vectorial operation called right, denoted by → and de?ned as: → v = v ∨ [?(v + 1)]. It is easily seen that → 0 = 0 and that → 0 · · · 01? · · ·? = 0 · · · 01 · · · 1. That is, right matches the ?rst one (from the left) by completing the vector with

90

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

ones (to the right) after the ?rst one. We note that → is the vectorial equivalent of the past temporal operator P (past) whose semantics is de?ned by: (w; n) |= P’ if there exists m6n such that (w; m) |= ’. We also de?ne a strict version of the → operation, the strict right, denoted by and de?ned by v = ↑0 (→ v). Thus, it is easily seen that 0 = 0 and that 0 · · · 0 1? · · ·? = 0 · · · 0 01 · · · 1. For example, we have: 0001101001 = 0000111111 and 001 = 000. operator is the vectorial equivalent of the strict version YP of the operator P, The de?ned by: (w; n) |= YP’ if there exists m?n such that (w; m) |= ’. Given a class of vectorial operations, we write VA[ ] for the set of vectorial algorithms using only bit-wise logical operations and operations in . For convenience, we omit the braces: we write VA[→; +] instead of VA[{→; +}]. For example PTLvector algorithms are exactly the ones in VA[↑0 ; +]. We use the same notation for languages: we will denote by VL[ ] the set of languages for which there is an automaton and a corresponding algorithm in VA[ ]. Therefore, VL[↑0 ; +] describes the PTL-vectorial languages. For each fragment of PTL-vectorial languages, we would like to have an e cient algorithm to decide whether or not a given language belongs to the fragment. For this, we will use characterizations of fragments of past temporal logic given in [4,14,15]. A fragment of past temporal logic is de?ned as follows: given a class of temporal modalities, we write PTL[ ] for the set of temporal formulas in which modalities other than ones from N do not occur. For convenience, we omit the braces, e.g., we write PTL[Y; YP] instead of PTL[{Y; YP}]. We can also associate with a set of languages noted L[ ] such that a language L belongs to L[ ] if and only if there exists a formula ’ ∈ PTL[ ] such that L is de?nable by ’. 6.2. Characterizing fragments of PTL-vectorial languages 6.2.1. Preliminaries Intuitively, there exists a tight link between languages de?ned by logical conditions and languages de?ned by “equivalent” vectorial conditions. For example, in Section 4 we have seen that PTL-vectorial languages are the same as languages de?ned by past temporal logic. But, whereas logical satis?ability depends exclusively on the language, vectorial characterizations seem to be closely related with a speci?c automaton. Vectorial characterizations are stronger than logical characterizations because in order to have a vectorial algorithm for a given automaton one must be able to characterize any state, hence any language recognized by the automaton obtained by setting a given state as unique ?nal state. For a logical formula one just needs to exhibit the set of ?nal states needed for the given language. But under some assumptions, logical fragments and vectorial fragments de?ne the same class of languages. Let us be more explicit. Given a set of vectorial operations and a set of logical operators, we will say that and are equivalent if they satisfy the following conditions: (1) To any vectorial algorithm using only operations in one can associate a PTLformula ’ using only operators in such that for any word u and any positive

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

91

integer i smaller than |u|, the ith entry of the vector obtained by applying to u is 1 if and only if (u; i) |= ’. (2) To any PTL-formula ’ using only operators in , one can associate a vectorial algorithm using only operators in such that for any word u = u1 · · · um , the computation of the binary vector v’ = v1 · · · vm , where vi = 1 ? (u1 · · · ui ; i) |= ’, is performed by the algorithm . For example, we have seen in Section 4 that the set of vectorial operations = {↑0 ; +} is equivalent to the set of logical operators = {Y; S}. Moreover, in this case we have that VL[ ] = L[ ]. Several fragments of temporal logic have been studied and characterized in [4,14,15] and therefore to characterize a fragment of PTL-vectorial languages, a solution consists in ?nding an equivalent fragment in temporal logic. We have to ?nd a condition on two equivalent sets and to have VL[ ] = L[ ]. A set of logical operators will be called ?nally stable if for every language L that belongs to L( ), any language recognized by an automaton obtained from the minimal automaton of L by letting some arbitrary state to be the unique ?nal state, belongs to L( ). For example, any set such that L( ) is a variety of languages is ?nally stable. Formally, if L is a language in L( ) and A its minimal automaton, any automaton A obtained by modifying the ?nal states of A recognizes a language L of L( ) because the syntactic monoid of A divides the syntactic monoid of A. The notion of ?nal stability gives us the following lemma: Lemma 1. Let be a set of vectorial operations and let be an equivalent set of logical operators. Then is ?nally stable if and only if VL( ) = L( ). Proof. First assume that is a ?nally stable set of logical operators equivalent to a set of vectorial operations. The inclusion VL( ) ? L( ) is not di cult. To prove the converse inclusion, VL( ) ? L( ), let us consider a language L ∈ L( ) and its minimal automaton A = (Q; A; ·; qi ; F ). For any state q of A, the automaton Aq obtained from A by letting q be the unique ?nal state, recognizes the language Lq that belongs to L( ). Therefore, we have a formula ’q in PTL( ) that de?nes Lq . Therefore, we have that qi · u = q if and only if (u; |u|) |= ’q . We obtain a simple algorithm in VA( ) characterizing the state q in the automaton A just by translating ’q (and this is possible by the equivalence between and ). Conversely, let us assume that and are equivalent and such that L( ) = VL( ) and let us show that is ?nally stable. For this, consider a language L ∈ L( ). Then L also belongs to VL( ), and therefore its minimal automaton Amin is -vectorial. We have thus an algorithm for any state q of Amin (such that its translation into a PTL-formula belongs to PTL( )) that characterizes the language recognized by the automaton obtained from Amin by choosing q as unique ?nal state. Therefore, these languages belong to L( ), what proves the ?nal stability of and achieves the proof. Remark 2. The preceding lemma and the results about temporal logic given in [1] yield a generic proof of the results of the preceding sections by noting that star-

92

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

free languages, solvable languages and regular languages are varieties and that their associated sets of logical operators are ?nally stable. In [4,14,15] several characterizations of fragments of past temporal logic are stated. We will use them to characterize fragments of PTL-vectorial languages. But ?rst of all we need some de?nitions. The characterizations of fragments of past temporal logic use the minimal automaton and the presence, or absence, of speci?c structures, called forbidden patterns. For instance for star-free languages we consider a characterization that forbids counting patterns. Given a set N , an N -labeled digraph is a tuple (V; E ) where V is an arbitrary ?nite set and E a subset of V × N × V . The closure of a deterministic ?nite automaton A, denoted CA , is the A+ -labeled digraph (V; E ) where E = {(q; u; q · u) | q ∈ Q and u ∈ A+ }. Therefore, the closure of any deterministic ?nite automaton is an in?nite graph (it has in?nitely many edges, but only ?nitely many vertices). Finally, a pattern is a labeled digraph whose vertices are state variables, usually denoted p; q; : : :, and whose edges are labeled with variables for labels of two di erent types: variables for non-empty strings, usually denoted u; v; : : :, and variables for letters, usually denoted a; b; : : : : In addition, a pattern comes with side conditions stating which state variables are to be interpreted by distinct states. We draw patterns just as we draw graphs and adopt the convention that all states drawn solid must be distinct. We say that an A+ -labeled digraph matches a pattern if there is an assignment to the variables obeying the type constrains and the side conditions, so that the digraph obtained by replacing each variable by the value assigned to it is an induced subgraph of the given digraph. 6.2.2. Characterizing VL[ ] We are now ready to characterize our ?rst fragment of PTL-vectorial languages: Theorem 5. Let L be a regular language over some alphabet A. Then the following assertions are equivalent: (1) L belongs to VL[ ]. (2) L belongs to L[YP]. (3) The closure of the minimal automaton Amin (L) of L does not match the following pattern:

The equivalence between (2) and (3) is shown in [14,15]. The other equivalences come from Lemma 1, from the equivalence between YP and , and from the following lemma (which implies that YP is ?nally stable):

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

93

Lemma 2. Let us consider a deterministic complete automaton that does not match the pattern of Theorem 5. Then its minimal automaton does not match it either. Proof. We show the result by contradiction. Let us consider a deterministic complete automaton A that does not match the pattern of Theorem 5 and let us assume that its minimal automaton Amin contains the pattern. Thus there exist four states P; Q; P and Q of Amin , a letter a and two words u and v such that P · a = Q; P · a = Q ; P · u = P ; P · v = P and Q = Q . As A is a deterministic complete automaton, we can identify the states of Amin with the Nerode equivalence classes of A. In the following we will not make any distinction between the states of Amin and the Nerode equivalence classes of A. We have the following consequences: (1) For any states q ∈ Q; q ∈ Q we have q = q . (2) For any state p ∈ P , we have p · u ∈ P . (3) For any state p ∈ P , we have p · v ∈ P . (4) For any state p ∈ P we have p · a ∈ Q and for any state p ∈ P we have p · a ∈ Q . Therefore, for any states p ∈ P; p ∈ P we have p · a = p · a. Our aim is to prove the existence of two words z and t , of four states p; p ; q and q where p ∈ P; p ∈ P ; q ∈ Q and q ∈ Q such that p · a = q; p · a = q ; p · z = p and p · t = p. Therefore, we will have a contradiction with the fact that A does not contain the pattern. Let us assume that |P |6|P | (the symmetric case is identical) and consider a state p1 ∈ P . Thus the state p1 = p1 · u belongs to P and p2 = p1 · v belongs to P . As A does not contain the pattern, we have p2 = p1 . For the same reason the state p2 = p2 · u belongs to P and is di erent from p1 , the state p3 = p2 · v belongs to P and is di erent from p2 and p1 (because we have p1 · uvu = p2 and p2 · v = p3 ). Iterating this reasoning orders the states of P = {p1 ; p2 ; : : : ; pn } and the states of a subset R = {p1 ; p2 ; : : : ; pn } of P . Moreover, this order is such that for any i6j 6n, there exists a word u ? such that pi · u ? = pj and for any i?j 6n there exists a word v ? such that pi · v ? = pj . Let us now consider the state p = pn · v ∈ P : there exists i, 16i6n such that p = pi . We thus have a contradiction because there exists a non-empty word z such that pi · z = pn and pn · v = pi and pi · a = pn · a, hence A contains the pattern. The proof can be resumed by the following diagram:

6.2.3. Characterizing VL(↑0 ; →) The class VL(↑0 ; →) corresponds to the logical fragment that uses only yesterday and past as operators:

94

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

Theorem 6. Let L be a regular language over some alphabet A. Then the following assertions are equivalent: (1) L belongs to VL[↑0 ; →]. (2) L belongs to L[Y; P]. (3) The closure of the minimal automaton Amin (L) of L does not match the following pattern:

The equivalence between (2) and (3) can be found in [14,15]. The other equivalences come from Lemma 1 and from the following lemma, that implies that {Y; P} is ?nally stable: Lemma 3. Consider a deterministic complete automaton that does not match the pattern of Theorem 6, then its minimal automaton does not match the pattern, either. As for the proof of Lemma 2 we reason by contradiction. Let us consider a deterministic automaton A that does not match the pattern and assume that its minimal automaton Amin matches the pattern. We thus have two distinct states P and Q of Amin and three words u; v and w such that: P · u = P; Q · u = Q; P · v = Q and Q · w = P . As in the preceding proofs, we identify the states of Amin with Nerode equivalence classes of states of A and therefore we obtain that: (1) For each state p ∈ P we have p · u ∈ P and p · v ∈ Q. (2) For each state q ∈ Q we have q · u ∈ Q and q · w ∈ P . Let us consider the Nerode equivalence class associated with state P (the reasoning is the same for Q). Since P · u = P , we can decompose it into components of states that are obtained by iterating the action of word u on a beginning state (as in Pollard’s method). So an equivalence class can be seen as a union of components having the following form:

Now, let us consider a state p1 ∈ P . There exist k; k ?0 and a state p1 ∈ P such that p1 · uk = p1 and p1 · uk = p1 (p1 belongs to the loop of the component containing p1 ).

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

95

The state q1 = p1 · v belongs to Q. Let us consider the state q1 de?ned from q1 ; v as we have de?ned p1 from p1 : there exists a word v ? such that p1 · v ? = q1 and a word u ? = uh (where h is the least common multiple of the lengths of the loops containing ? = p1 and q1 · v ? = q1 . Therefore, as A does not the states p1 and q1 ) such that p1 · u match the pattern, q1 · w must not belong to the component of p1 . We can iterate this reasoning as in the proof of Lemma 2 and we ?nd a similar contradiction. In fact this proof is analogous but we must work on components instead of states. 6.2.4. Characterizing VL(↑0 ) To characterize VL(↑0 ), we can use either a result about languages de?nable using the yesterday operator, or give a direct proof (which gives us therefore a characterization of L(Y)). We begin with the direct proof because it illustrates the use of vectorial languages. Intuitively, if we have for a given deterministic complete automaton an algorithm using only the right-shift operation ↑0 , let us say k times, this means that for any word and for any position in this word we have to consider only the k +1 last letters for knowing the state reached by the automaton. Formally: Theorem 7. An automaton has an associated algorithm in VA[↑] if and only if it is trivial (any letter loops on any state) or if there exists an integer k such that the transition functions de?ned by the words of length k are constant. E ectively, let us consider a non-trivial automaton A having an algorithm in VA[↑]. We then have an algorithm computing the output vector r of the visited states from the input vector u and using only bit-wise logical operations and the right-shift. Let k be the number of right shift operations used. Therefore, it is easily seen that the nth position of r only depends on the positions n; n ? 1; : : : ; n ? k of u. Thus, if u is a word of length k + 1, then u leads to a state independent of the initial state, i.e, u de?nes a constant mapping in QQ , where Q is the set of states of A, what proves the ?rst implication. Conversely, let us consider an automaton having this property and let us construct an algorithm in VA[↑] for it. The case of the trivial automaton is not di cult and we will no longer deal with it. For any word v of length k , we compute the characteristic vector ev of v: ev =

k ?1 i=0

↑i0 (u = ak?1?i )

i where v = a0 · · · ak ?1 and note by ↑0 the operation ↑0 iterated i times. For any state q, we design by Lk q the set of words of length k sending any state on q. Therefore, the vector (r = q) = v∈Lk ev matches, except possibly on the k ?1 ?rst q terms, the characteristic vector (r = q). But it is easy to compute the k ? 1 ?rst terms of (r = q): it su ces to consider the words w of length less or equal than k ? 1 that lead to q from the initial state. Therefore, we just have to compute their characteristic

96

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

vectors ew and to take their disjunction. Thus we obtain the vector (r = q) that matches (r = q) on the k ? 1 ?rst terms. The vector (r = q) is ?nally given by (r = q) = [(r = q) ∧ x] ∨ [(r = q) ∧ ?x]

k ? where we let x = ↑k 0 1 = 0 1 . Therefore, we obtain an algorithm for A in VA[↑0 ]. We can give a corollary of this result in algebraic terms:

Corollary 1. A regular language belongs to L[↑0 ] if and only if its syntactic semigroup belongs to the variety D of semigroups de?ned by the equation yx! = x! . In fact the equation yx! = x! is associated with languages of the form A? X ∪ Y where X and Y are ?nite sets of non-empty words on an alphabet A [7]. It is therefore easy to verify, using Theorem 7, that the languages of L[↑0 ] are exactly those associated with the variety of semigroups D. E ectively, let us consider an automaton for which any word of a given length k de?nes a constant mapping in QQ . Let e be an idempotent of the transition semigroup. As e = ek ; e can be associated with a word of length greater or equal than k and therefore e is associated with a constant mapping and thus it is right absorbing, i.e., for any element v of the transition semigroup we have ve = e. Consequently, the transition semigroup veri?es the equation yx! = x! . Conversely, let us consider a language recognized by an automaton (that can be chosen deterministic and complete) such that its transition semigroup veri?es the equation yx! = x! . To any state q of the automaton, we can associate a language Lq composed of all words that lead from the initial state to q. The syntactic semigroup of this language divides the transition semigroup of the given automaton and thus veri?es the equation yx! = x! . Therefore, Lq = A? X ∪ Y where X and Y are two ?nite sets of words. The elements of X de?ne constant mappings that send any state on q. Making this reasoning for all states gives us for any state a set of characteristic words. Considering the longest word of these sets we ?nd an integer k such that any word of length k de?nes a constant transition function. Using a result on a fragment of temporal logic [14,15] and Lemma 1 we have the following characterizations: Theorem 8. Let L be a regular language over some alphabet A. Then the following assertions are equivalent: (1) L belongs to VL[↑0 ]. (2) L belongs to L[Y]. (3) The closure of the minimal automaton of L; Amin (L) does not match the following pattern:

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

97

(4) The syntactic semigroup of L belongs to the variety D de?ned by the equation yx! = x! . 6.2.5. Characterizing unambiguous languages In this section we give a characterization of unambiguous languages using a fragment of PTL-vectorial languages. Let us consider an alphabet A. A product of the form ? ? A? 0 a1 A1 a2 · · · ak Ak , where Ai is a subset of A and ai is a letter, is called unambiguous if for any word u on the alphabet A, if u belongs to the product then there is a unique decomposition u0 ; u1 ; : : : ; uk such that u = u0 a1 u1 a2 · · · ak uk with ui ∈ A? i . An unambiguous language is a ?nite, disjoint union of unambiguous products. Unambiguous languages are well studied. We will use there two results: the fact that unambiguous languages form a variety of languages and a characterization using a symmetric fragment of temporal logic. A symmetric fragment of temporal logic is de?ned as a classical fragment except that the use of future operators (and not only past operators) is allowed [14,15]. The symmetric fragment L[|XF|] associated with unambiguous languages is the one allowing the use of the strict operators past (YP) and future (XF). The operator XF has the following semantics: (w; n) |= XF’ if there exists n?m6|u| such that (w; m) |= ’. De?ning the operation strict left as a symmetric version of , using Lemma 1 and the equivalence between unambiguous languages and the symmetric fragment L[|XF|], we have the following result: Theorem 9. Let L be a regular language over some alphabet A. Then the following assertion are equivalent: (1) L is unambiguous. (2) L belongs to L[|XF|]. (3) L belongs to VL[ ; ]:

7. Reconstructing an automaton from a PTL-vectorial algorithm In the preceding sections we wanted to ?nd a vectorial algorithm from a given automaton. We now consider the converse problem, that is we want to check for a given PTL-vectorial algorithm whether there exists a deterministic complete automaton associated with it (and determine an automaton, if this is the case). This question becomes interesting for instance when we modify a given vectorial algorithm (associated with a deterministic automaton) and we want to check afterward that the new algorithm is equivalent to the old one. We will show that the complexity of this test is actually the same as testing the satis?ability of an LTL-formula (PSPACEcomplete). Vectorial algorithms are associated with deterministic complete automata and therefore depend on the initial state (and not only on the underlying labeled graph structure of the given automaton). We will thus suppose that the initial state is part of the input.

98

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

To begin with, let us consider a valid PTL-vectorial algorithm (i.e. an algorithm for which there exists a corresponding deterministic complete automaton) and let us explain how to construct such an associated automaton. Let A = {a1 ; : : : ; ak } be the alphabet of the automaton and let n be the number of states (we will identify them with the integers 1 : : : n). To compute an associated automaton A from a given PTL-vectorial algorithm we perform a depth-?rst search of A , that is we start from the initial state q0 and compute the states that can be reached by reading a letter from q0 and then we repeat this step with the new states found so far. We are done when we have explored all reachable states. With this method we explore all the transitions of the accessible part of the automaton. We just have to explain how to compute the reachable states from a given state. In our algorithm we maintain a vector, state direction, giving for any state encounter q a word u leading from the initial state to q. Therefore, when considering a state q, and a letter a to compute the transition from q reading a we have to apply to the word ua and consider the |u| + 1 component of the result, denoted |u|+1 (ua). We thus have the following algorithm: ? Variables and initialization: ? : (n×k )-vector. ? new states = [1] : LIFO structure. ? known states = {1} : Set structure. ? state direction = [”; ”; : : : ; ”]. ? Main loop: While new states = ? Do Let q = Delete element from new states. Let u = state direction:(q). Let h = |u|. For i = 1 to k Do Let q = h+1 (uai ). Let (q; i) = q . If q ∈ = known states Then Add q to new states and to known states. Set state direction:(q ) = ua. End If. End For. End While. ? Return . To test the validity of a given algorithm we will ?rst use the preceding algorithm to compute the automaton A associated with , if it is valid. If the algorithm does not work (that is if h+1 (uai ) is not de?ned for a given step of the algorithm) this implies that is not valid. Otherwise we need to use the validity test stated in the theorem below. For any state q, let L(q) denote the regular language de?ned by the logical formula obtained as in Section 4.2 from the algorithm computing (r = q).

n

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

99

Theorem 10. Let be a PTL-vectorial algorithm and let A be the deterministic complete automaton constructed by the algorithm above. Then is a valid algorithm associated with A if and only if: (1) For any non-reachable state q of A , we have L(q) = ?. (2) For any reachable state q, we have that L(q) = ?. In addition, the following assertions are equivalent: (i) L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq , where Eq = {”} if q is the initial state and Eq = ? otherwise. Moreover, aj is a letter and each qj is a reachable state. (ii) {(q1 ; a1 ); : : : ; (qi ; ai )} is exactly the set of the pairs (qj ; aj ) such that qj :aj = q in A . Proof. First let us assume that is valid. This implies that for any state q, the word u belongs to L(q) if and only if q0 · u = q, where q0 denotes the initial state of A . Therefore, we easily obtain that L(q) = ?, for any non-reachable state q of A . Let us now consider the case of a reachable state q and assume that (i) holds: L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq . For any pair (qj ; aj ), as qj is reachable, there exists v ∈ L(qj ) such that q0 · v = qj and vaj ∈ L(q). Consequently we have qj · aj = (q0 · v) · aj = q0 · u = q. Conversely, consider a pair (q ; a) such that q · a = q and let us prove is valid this implies that that L(q) ? L(q )a. Let us consider a word w ∈ L(q ). As q0 · w = q and therefore q0 · wa = q · a = q, what shows that L(q )a ? L(q). We have thus shown that (i) implies (ii). Let us now assume that (ii) holds. We will prove that L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq where {(q1 ; a1 ); : : : ; (qi ; ai )} is exactly the set of the pairs (qj ; aj ) such that qj · aj = q. So let us consider a word u ∈ L(q). As is valid, we have that q0 · u = q and therefore if |u|?2, we can write u as u = va with q0 · u = (q0 · v) · a. So there exists j such that (q0 · v; a) = (qj ; aj ) and v ∈ L(qj ) and thus u ∈ L(qj )aj . The cases |u| = 0 and |u| = 1 are immediate as ” belongs to L(q0 ). Conversely, if we consider a word u = vaj ∈ L(qj )aj we have that q0 · u = (q0 · v) · aj = qj · aj = q and thus u ∈ Lq . We have thus proved that (ii) implies (i). Suppose now that for any non-reachable state q, L(q) = ? and that for any reachable state q, the set L(q) is non-empty and that (i) and (ii) are equivalent. Let us prove that this implies the validity of . We work by contradiction assuming that is not valid. We have two cases: (1) There exists u ∈ L(q) and q0 · u = q. We can choose u of minimal length. With this property, as u ∈ L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq , we have u = vaj (the case |u| = ” is immediate) where 16j 6i and v ∈ L(qj ) (v can be empty). By minimality of u we must have q0 :v = qj and therefore, q0 · u = (q0 · v) · aj = qj · aj = q (by equivalence between (i) and (ii)) what leads to a contradiction. (2) There exists a word u such that q0 · u = q and u ∈ = L(q). We can choose again u of minimal length. The case u = ” is immediate and we can therefore decompose u as u = va (where v can be empty). The minimality of u implies that v ∈ L(q ) where we set q = q0 · v. But we also have that q · a = q and thus, by equivalence between

100

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

(i) and (ii) we have that u = va ∈ L(q )a ? L(q), what leads to a contradiction with u∈ = L(q). We have thus proved that is valid and so it is associated with A . We can now give a method to test the validity of a PTL-vectorial algorithm : (1) We apply the depth-?rst search algorithm described above to . If the algorithm does not yield a deterministic automaton A , then is not a valid algorithm and we can stop. Otherwise we go to the next step. (2) We determine the reachable states and the non-reachable states of the automaton A constructed in the preceding step. (3) For every non-reachable state q we translate the associated component in into a PTL-formula ’q and test whether or not it can be satis?ed (see Section 8 and [10]). If ’q is satis?able for a non-reachable-state q then is not valid and we stop. Otherwise we go to the next step. (4) For every reachable state q we determine the set {(q1 ; a1 ); : : : ; (qi ; ai )} of the pairs (qj ; aj ) such that qj · aj = q in A and we verify that L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq . To achieve this e ciently we can determine for every j a PTLformula associated with L(qj )aj . It su ces to consider the formula paj ∧ Y’qj where ’qj is the translation of the component of associated with qj . Then, we can construct a PTL-formula for the language L(q) [L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq ], where holds for the symmetric di erence, and verify that it cannot be satis?ed, what is equivalent to the equality L(q) = L(q1 )a1 ∪ · · · ∪ L(qi )ai ∪ Eq . If the test does not fail, then is valid and associated with A , otherwise is not valid. Let us now give the complexity of this algorithm. We will prove that determining whether or not a PTL-algorithm is valid is a PSPACE-complete problem. We ?rst show that this test can be achieved in polynomial space. The ?rst step, the depth-?rst search algorithm, calculates all the transitions of the reachable part of A . As A is a deterministic complete automaton, there are O(n|A|) transitions, where n denotes the number of states of A and A is the alphabet of A . The result of applied to a given word can be computed in logarithmic space. E ectively the PTL-operations are logarithmic space operations and logarithmic space operations are closed by composition. Therefore, as n = O(| |) and |A| = O(| |) (the size of the algorithm is the size of the PTL-formula plus the size of A), the ?rst step can be achieved in polynomial time. The second step, is performed also in polynomial time (and thus in polynomial space). In the third step, the construction and the size of ’q is polynomial in | |. Determining whether or not a PTLformula can be satis?ed, is known to be a PSPACE-complete problem (see Section 8.5 and [10]). As |’q | is polynomial in | |, this step can be achieved in polynomial space. For the same reasons the fourth step can also be achieved in polynomial space. We have thus proved: Proposition 2. Deciding whether or not a PTL-vectorial algorithm is valid can be done in polynomial space.

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

101

In fact, we can give a more precise result: Theorem 11. Deciding whether or not a PTL-vectorial algorithm is valid is a PSPACE-complete problem. Proof. We just have to prove the PSPACE-hardness. For this, we reduce the PSPACEcomplete problem of deciding whether or not a PTL-formula can be satis?ed. So let us consider a PTL-formula ’ over some alphabet A. We will consider an automaton with two states, 1 and 2. Let be the translation of ’ into a PTL-vectorial formula. Then, we de?ne a PTL-vectorial algorithm by: = (r = 1) = true; (r = 2) = ;

where the initial state is 1. We have that ’ can be satis?ed if and only if is not valid. The automaton constructed using the depth-?rst search algorithm is the solid part of the following automaton:

If ’ can be satis?ed, say by a word u, the algorithm does not give a correct result on u. Conversely, if is not correct, using Theorem 10, we have two cases: (1) L(2) is non-empty, that is ’ can be satis?ed. (2) L(1) is empty (what is wrong) or L(1) = L(1)a ∪ {”} (what is also wrong). Therefore, we have proved that ’ can be satis?ed if and only if is not valid. This proves that determining whether or not a PTL-vectorial algorithm is valid is a PSPACE-complete problem. We now consider the same problem but for fragments of PTL-vectorial languages. For instance we have the following result for algorithms in VA(↑0 ): Theorem 12. Deciding whether or not an algorithm in VA(↑0 ) is valid is an NPcomplete problem. As for the general problem we ?rst use the depth-?rst search algorithm to determine an automaton such that our algorithm is valid if and only if it is associated with this automaton. Using Theorem 8 it is easily seen that an algorithm in VA(↑0 ) is associated with a given automaton if and only if it is associated with it for words of length less or

102

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

equal than k + 1, where k designs the maximum number of nested shift operations. This implies the membership in NP (we have to determine k and then to guess a word of length less or equal than k + 1 and ?nally to test the correctness of the algorithm for it). In order to prove the NP-hardness we reduce the problem of deciding whether or not a formula in PTL(Y) can be satis?ed to our problem. For this we use the same reduction as in Theorem 11. We conclude the proof using the following lemma: Lemma 4. Deciding whether or not a formula in PTL(Y) is satis?able, is an NPcomplete problem. Proof. The membership in NP is not di cult: a formula in PTL(Y) can be satis?ed if and only if it can be satis?ed by a word of length less or equal than k + 1, where k designs the maximum number of nested Y operators (e ectively the truth of a formula in PTL(Y) applied to a word u only depends on the su x of length k + 1 of u). The NP-hardness is shown by a reduction from the NP-complete problem SAT. Let us consider a propositional formula F and let us construct a formula ’ in PTL(Y) such that F can be satis?ed if and only if ’ can be satis?ed. We denote by p1 ; : : : ; pn the propositional variables used in F . The alphabet of the temporal formula ’ is the boolean alphabet: { ; ⊥}, and ’ is constructed from F by replacing each propositional variable pi by Y : : : Y p (p is the predicate associated with the letter ). For example, for F = (p2 ∨ p1 ) ∧ ?[p1 ∨ (p3 ∧ p2 )] we de?ne ’ = (Yp ∨ YYp ) ∧ ?[YYp ∨ (p ∧ Yp )] For any formula F , we easily have that F is satis?ed by a valuation (b1 ; : : : ; bn ), where each bi is a boolean (bi = or ⊥), if and only if (b1 : : : bn ; n) |= ’. This shows that SAT can be polynomially reduced to our problem and therefore achieves the proof.

n?i

8. Reconstructing automata from GTL-vectorial algorithms In the preceding section we have shown how to decide whether there exists an associated counter-free automaton with a given PTL-vectorial algorithm . For this, we ?rst construct an automaton A associated with , if is valid. Then, using Theorem 10 we decide whether is valid. A natural investigation is to try to extend these results to MTL-vectorial and GTL-vectorial languages introduced in Sections 5.1 and 5.2. The main result of this section states that deciding the validity of a GTL-vectorial algorithm is PSPACE-complete. For obtaining this result, we review the construction of alternating automata from temporal logic formulas and show how to deal with modular and group operators and we also use that Theorem 10 does not actually depend on the

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

103

vectorial operations allowed in our algorithm and can be stated in a more general way, by assuming is a vectorial algorithm. For a PTL-vectorial algorithm , in order to compute the automaton A we simulate a depth-?rst search algorithm. This algorithm can be adapted to MTL-vectorial algorithms and to GTL-vectorial algorithms without change. Nevertheless, its complexity is not the same as the simulation of in the general case of modular and group operators is more costly. Actually, we have the following result: Lemma 5. Let be a GTL-vectorial algorithm and let u be a word. Then the computation of the result of applied to u can be achieved in O(|u|:| |) operations Proof. The result trivially holds in the special case of PTL-vectorial algorithms. We denote by C ( ; u) the cost of the computation of applied to u. If = Sl; k ( 1 ), to compute the result of applied to u, we ?rst compute the result of 1 applied to u and then read it from left to right to determine the ?nal result. We have that C ( ; u) = C ( 1 ; u)+ |u|. Therefore, modular operators cost linear time. If = P g;G ( 1 ; : : : ; q ), to compute the result of applied to u, we ?rst compute the results of 1 ; : : : ; q applied to u and then read them simultaneously from left to right to determine the ?nal result. We have that C ( ; u) = C ( 1 ; u) + · · · + C ( q ; u) + |u|. Thus group operators also cost linear time. Therefore, the computation of the result of applied to u can be achieved in O(|u|:| |) operations. Lemma 5 implies that the computation by the depth-?rst search algorithm of an can be made in polynomial time. There is another associated automaton A with question left in order to solve our problem, that is how to use Theorem 10 for MTLvectorial and GTL-vectorial algorithms. As for PTL-vectorial languages, the equality on languages to verity can be translated into a satis?ability problem, for GTL-formula in this case. In Section 8.5, we prove that the satis?ability problem for GTL-formula is PSPACE-complete and therefore, we have the following result: Theorem 13. Deciding whether or not a GTL-vectorial algorithm is valid is a PSPACE-complete problem. To prove the satis?ability result for GTL-formulas, we use alternating automata and reduce the satis?ability problem to a non-emptiness problem for alternating automata. 8.1. Alternating automata An alternating automaton is a tuple A = (Q; A; ; q0 ; F ), where Q is a ?nite set of states, A is a ?nite alphabet, q0 is the initial state, F is the set of ?nal states and : Q×A → B+ (Q) is the transition function, where B+ (Q) is the set of all negationfree boolean formulas over Q.

104

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

A run of an alternating automaton is a ?nite tree whose nodes are labeled with states of Q and edges with elements of A. The level of a node is the length of the word labeling the path from the root to this node. A run associated with a ?nite word u = a1 a2 · · · an is de?ned by induction: (1) The root is q0 . (2) The nodes of level n are leaves (i.e. they have no sons). (3) If q is a state of level i?n and (q; ai ) = C1 ∨ C2 ∨ · · · ∨ Cm with Cj = qj; 1 ∧ qj; 2 ∧ · · · ∧ qj; nj then q has nj sons for some j , 16j 6m, labeled by q1; k1 ; qj; 1 ; : : : ; qj; nj . That is, q must have as sons all the states appearing in one of the conjunctions Cj . Remark 3. In our de?nition of a run, (q; a) is in disjunctive normal form for any state q and any letter a. Of course, could be de?ned as a function taking its values in negation-free boolean formulas in disjunctive normal form, but the constructions given in Sections 8.3 and 8.4 would lead to consider alternating automata with an exponential number of transitions. In fact we will not be interested in computing such automata but in runs of them. Therefore, for any formula (q; a), a minimal model (whose size will always be linear in the number of states) will be computed whenever we need it. A model for a formula is a set R of states, such that assigning to the states in R the value tt and to those on Q\R the value f f makes the formula true. Nevertheless, for representing alternating automata we will work with formulas in disjunctive normal form. A word u is accepted by A if there exists a run r associated with u such that all the leaves of r are ?nal states. The language recognized by an alternating automaton A is noted L(A). Alternating automata will be drawn as classical automata except for the fact that the outgoing edges go ?rst into a square (that is not a state!) that redirects the transition into groups of states (represented by the same index written on their incoming edges). For example the transition (q0 ; a) = (q1 ∧ q0 ) ∨ (q1 ∧ q2 ) is represented by

In the special case where (q; a) is a disjunction (that is nj = 1 for all j = 1 : : : m) we represent the transition (q; a) as a classical existential (i.e. non-deterministic) transition. Example 2. Consider the {q1 ; q2 }), where we have: alternating automaton A = ({q0 ; q1 ; q2 }; {a; b}; ; {q0 };

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

105

? (q0 ; a) = (q0 ∧ q2 ) ∨ q1 , (q1 ; a) = q1 ∨ q2 and (q2 ; a) = q0 ∧ q1 . ? (q0 ; b) = q1 ∨ q0 , (q1 ; b) = q1 and (q2 ; b) = q2 . A is represented by the following picture:

Let us now give two runs for the word u = aaba in A: the ?rst one is accepting (therefore u is recognized by A), whereas the second one is not accepting.

106

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

8.2. Linear temporal logic Similar to the past temporal logic, the future temporal logic, called Linear Temporal Logic (LTL) is de?ned using the temporal operators Next (denoted X), and Until (denoted U). X and U are, respectively, the future equivalents of the operators Y and S. Therefore, their semantics is de?ned by (1) (w; n) |= X’1 if n?|w| and (w; n + 1) |= ’1 . (2) (w; n) |= ’1 U’2 if there exists m?n such that (w; m) |= ’2 and, for every k such that n6k?m, (w; k ) |= ’1 . An LTL-formula ’ is satis?ed by a word w if (w; 1) |= ’. An LTL-formula ’ is called satis?able if its associated language L’ = {w | (w; 1) |= ’} is not empty. With an LTL-formula ’ one can associate a PTL-formula ’ ? by replacing the operator X by the operator Y and the operator S by the operator U. It is easily seen that, for any word w, (w; 1) |= ’ if and only if (w; ? |w|) |= ’ ? , where w ? designs the mirror image of w. Thus, to decide whether a PTL-formula is satis?able, it su ces to know how to solve the problem for LTL-formulas. In the next section we recall the construction of an alternating automaton recognizing the language L’ , where ’ is an LTL-formula [13]. We need the construction in order to generalize it to the more expressive temporal logics. For convenience, we use a new operator called Release (denoted R). The release operator is de?ned by the formula ’1 R’2 = ?(?’1 U?’2 ), or equivalently by: (w; n) |= ’1 R’2 if and only if for all m, n6m6|w|, such that (w; m) 2 ’2 , there exists n6i?m such that (w; i) 2 ’1 . The release operator requires its second argument to be true, a condition that is released as soon as the ?rst argument becomes true. Introducing the release operator allows to construct, for any LTL-formula ’, an equivalent positive formula , i.e. a formula that does not use the negation. The formula is constructed by induction on ’ and is of size O(|’|): (1) If ’ = pa where a is a letter, = ’. (2) If ’ = ?pa where a is a letter, = b∈A\{a} pb . (3) If ’ = ’1 ∨ ’2 then = 1 ∨ 2 where 1 and 2 are, respectively, constructed from ’1 and ’2 . (4) If ’ = ?(’1 ∨ ’2 ) then = 1 ∧ 2 where 1 and 2 are, respectively, constructed from ?’1 and ?’2 . (5) If ’ = ’1 ∧ ’2 then = 1 ∧ 2 where 1 and 2 are, respectively, constructed from ’1 and ’2 . (6) If ’ = ?(’1 ∧ ’2 ) then = 1 ∨ 2 where 1 and 2 are, respectively, constructed from ?’1 and ?’2 . (7) If ’ = X’1 then = X 1 where 1 is constructed from ’1 . (8) If ’ = ?X’1 then = X 1 where 1 is constructed from ?’1 . (9) If ’ = ’1 U’2 then = 1 U 2 where 1 and 2 are, respectively, constructed from ’1 and ’2 . (10) If ’ = ?(’1 U’2 ) then = 1 R 2 where 1 and 2 are, respectively, constructed from ?’1 and ?’2 .

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

107

(11) If ’ = ’1 R’2 then = 1 R 2 where 1 and 2 are, respectively, constructed from ’1 and ’2 . (12) If ’ = ?(’1 R’2 ) then = 1 U 2 where 1 and 2 are, respectively, constructed from ?’1 and ?’2 . For example if ’ = ?[pa U(pb ∨ Xpa )] and A = {a; b; c}, the associated formula is = (pb ∨ pc )R[(pa ∨ pc ) ∧ X(pb ∨ pc )] 8.3. From LTL-formulas to equivalent alternating automata Given a positive LTL-formula ’, there exists an alternating automaton A’ = (Q; A; ; q0 ; F ), whose number of states is linear in the size of ’ recognizing the language L’ (see also [13]). (1) The alphabet A of A’ is the alphabet of the words on which ’ is evaluated. (2) The states of A’ are the sub-formulas appearing in ’ and their negations ’ (written without using the negation as described in Section 8.2) plus the constants tt (True) and f f (False). (3) q0 = ’. (4) F = {tt } ∪ {’ = ’1 R’2 | ’ ∈ Q}. (5) is inductively de?ned by the following rules: (i) (tt; a) = tt and (f f; a) = f f for any letter a. tt if a = b; (ii) (pa ; b) = f f otherwise: (iii) (’1 ∨ ’2 ; a) = (’1 ; a) ∨ (’2 ; a). (iv) (’1 ∧ ’2 ; a) = (’1 ; a) ∧ (’2 ; a). (v) (X’; a) = ’ for all a ∈ A. (vi) (’1 U’2 ; a) = (’2 ; a) ∨ [ (’1 ; a) ∧ (’1 U’2 )]. (vii) (’1 R’2 ; a) = (’2 ; a) ∧[ (’1 ; a) ∨ (’1 R’2 )] = [ (’2 ; a) ∧ (’1 ; a)] ∨ [ (’2 ; a) ∧ (’1 R’2 )]. We have the following result what is shown in [13]. The detailed proof can be found in Appendix A. Theorem 14. Let ’ be a positive LTL-formula and let A’ be the automaton associated with ’. Then L’ = L(A’ ). 8.4. From GTL-formulas to equivalent alternating automata As alternating automata allow to recognize all regular languages, a natural investigation consists in associating an alternating automaton to formulas using modular or group operators. These operators were introduced in Sections 5.1 and 5.2. The modular operators were de?ned as past temporal operators. As we want to decide whether or not a temporal formula can be satis?ed, we will work with the dual operators, as de?ned for LTL. Therefore, to decide whether a MTL-formula or a GTL-formula can be satis?ed it su ces to decide the same problem for the dual formula. We thus give the de?nitions of the modular and group temporal operators for LTL (we will not change the notation with past temporal logic as no confusion can be

108

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

made here): ? With any pair (l; k ) of integers such that 06l?k we associate a unary modular operator Mod l; k such that for any word u, we have (u; i) |= Mod l; k (’) if and only if, modulo k , there are l positions j ?i such that (u; j ) |= ’. ? With any pair (g; G ), where G is a group and g is an element of G , we associate a group operator g;G that always binds |G | ? 1 formulas. The elements of G must have been ordered, say as g1 ; g2 ; : : : ; gq = id (the last element must be the identity). Let u be an element of A+ and let ’1 ; ’2 ; : : : ; ’q?1 be logical formulas. With each j , 16j 6|u| we associate an element of G , denoted ’1 ; ’2 : : : ’q?1 u; j , de?ned by: ’1 ; ’2 ; : : : ; ’q?1 u; j = gk ; where k = min{l | (u; j ) |= ’l } with the convention that min ? = q. Finally we have (u; i) |= g;G ’1 ; ’2 ; : : : ; ’q?1 if and only if

|u | j =i

’1 ; ’2 ; : : : ; ’q?1 u; j = g:

LTL extended by the modular operators will be denoted as MLTL. The extension by the group operators will be denoted GLTL. We have the following extension of Theorem 14: Theorem 15. Let ’ be a GLTL-formula. Then there exists an alternating automaton A’ such that L’ = L(A’ ). In addition, the number of states of A’ is quadratic in the size of ’. Proof. The modular operator is a special case of group temporal operators using only cyclic groups (Z=k Z; +), as (u; i) |= Mod l; k (’) if and only if we have (u; i) |= l; (Z=k Z;+) ’; f f; f f; : : : ; f f . Therefore, it su ces to consider the general case of GLTL. To keep working only with negation-free formulas, we have to explain, as in Section 8.2, how to construct a positive formula from a formula ’ = ? g;G ’1 ; ’2 ; : : : ; ’q?1 . Here it su ces to take: =

g =g g ;G

’1 ; ’2 ; : : : ; ’q?1 :

The alternating automaton A’ = (Q; A; ; q0 ; F ) recognizing L’ is de?ned almost as in Section 8.3: (1) The alphabet A of A’ is the alphabet of the words on which ’ is evaluated. (2) The states of A’ are the sub-formulas appearing in ’ and their negations ’ (written without using the negation, as described in Section 8.2) plus the constants tt (True) and f f (False). In addition, for any sub-formula g;G ’1 ; ’2 ; : : : ; ’q?1 appearing in ’ we add, for any g = g, the state g ;G ’1 ; ’2 ; : : : ; ’q?1 and its “positive negation”. (3) q0 = ’. (4) F = {tt } ∪ {’ = ’1 R’2 | ’ ∈ Q} ∪ {’ = id;G ’1 ; ’2 ; : : : ; ’q?1 | ’ ∈ Q}.

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

109

is inductively de?ned by the following rules: (i) (tt; a) = tt and (f f; a) = f f for any letter a. tt if a = b; (ii) (pa ; b) = f f otherwise: (iii) (’1 ∨ ’2 ; a) = (’1 ; a) ∨ (’2 ; a). (iv) (’1 ∧ ’2 ; a) = (’1 ; a) ∧ (’2 ; a). (v) (X’; a) = ’ for all a ∈ A. (vi) (’1 U’2 ; a) = (’2 ; a) ∨ [ (’1 ; a) ∧ (’1 U’2 )]. (vii) (’1 R’2 ; a) = (’2 ; a) ∧ [ (’1 ; a) ∨ (’1 R’2 )] = [ (’2 ; a) ∧ (’1 ; a)] ∨ [ (’2 ; a) ∧ (’1 R’2 )]. (viii) (Mod k; l (’); a) = [ (’; a) ∧ Mod k ?1; l (’)] ∨ [ (’; a) ∧ Mod k; l (’)] for all a ∈ A. (xi) ( g;G ’1 ; ’2 ; : : : ; ’q?1 ; a) = gi gj =g [ (i; a) ∧ gj ;G ’1 ; ’2 ; : : : ; ’q?1 ], where (i; a) = (’1 ; a) ∧ (’2 ; a) ∧ · · · ∧ (’i?1 ; a) ∧ (’i ; a), where ’q = tt . where (viii) is in fact a special case of (ix). The number of states of A’ is e ectively linear in the size of ’ times the sum of the cardinalities of the groups used in modular operators appearing in ’ and as this sum is linear in the size of ’, it follows that the number of states of A is quadratic in the size of ’. The proof is the same as for Theorem 14. We reason by induction on the formula ’. The only new case to consider is the one of ’ = g;G ’1 ; ’2 ; : : : ; ’q?1 . Any run of A’ on a non-empty word u whose ?rst letter is a1 has the following form:

(5)

where T is a run of A j , j = gj ;G ’1 ; ’2 ; : : : ; ’q?1 and gi1 gj = g, and where any tree of the following form is a run of A k for k = 1 : : : i1 , where k = ?’k if k?i1 and i1 = ’i1 (recall that ’q = tt ):

By induction hypothesis, this run is accepting if and only if (u; 1) |= ?’1 ∧ ?’2 ∧ · · · ∧ ?’i1 ?1 ∧ ’i1 and (u; 2) |= gj ;G ’1 ; ’2 ; : : : ; ’q?1 that is if and only if ’1 ; ’2 ; : : : ; ’q?1 u; 1 = gi1 and (u; 2) |= gj ;G ’1 ; ’2 ; : : : ; ’q?1 . Iterating this construction shows that with an accepting run of A’ on a word u = a1 · · · an one can associate a sequence gi1 ; : : : gin ; gin+1 of elements of G such that g = gi1 gi2 : : : gin gin+1 , for any k = 1 : : : n, ’1 ; ’2 ; : : : ; ’q?1 u; k = gik and such that (u; n)

110

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

|= gin+1 ;G ’1 ; ’2 ; : : : ; ’q?1 . But, as the unique ?nal state of the form gj ;G ’1 ; ’2 ; : : : ; ’q?1 is id = gq ;G ’1 ; ’2 ; : : : ; ’q?1 it follows that gin+1 must be equal to the neutral element gq of G and therefore that g = gi1 gi2 : : : gin , that is (u; n) |= ’. Conversely, with a word satisfying ’ it is easily seen how to construct an accepting run in A, what shows that we have L(A’ ) = L’ and achieves the proof. Example 3. Consider the MTL-formula ’ = [Mod 1; 3 (Xpa ∨ pb )] ∧ [pa Upb ] and let us describe the transition function associated with A’ : q pa pb Xpa Xpa = Xpb pa Upb Xpa ∨ pb Xpa ∨ pb = Xpb ∧ pa ’1 = Mod 1; 3 (Xpa ∨ pb ) ’2 = Mod 2; 3 (Xpa ∨ pb ) ’0 = Mod 0; 3 (Xpa ∨ pb ) ’ (q; a) tt f f pa pb pa Upb pa pb (pa ∧ ’0 ) ∨ (pb ∧ ’1 ) (pa ∧ ’1 ) ∨ (pb ∧ ’2 ) (pa ∧ ’2 ) ∨ (pb ∧ ’0 ) [pa ∧ ’0 ∧ (pa Upb )] ∨ [pb ∧ ’1 ∧ (pa Upb )] (q; b) f f tt pa pb tt tt f f ’0 ’1 ’2 ’0

The alternating automaton A’ is represented in Fig. 1. In fact, we represent only the reachable part and represent in dash a copy of pa and a copy of pb to improve readability. 8.5. Emptiness problem for alternating automata and its consequences In Sections 8.3 and 8.4 we have shown how to associate with a GLTL-formula ’ an alternating automaton A’ recognizing exactly the models of ’. Therefore, to decide satis?ability for GLTL-formulas (or for GTL-formulas), it su ces to know how to decide emptiness for alternating automata. We have the following result: Theorem 16. Let A be an alternating automaton, then testing whether L(A) = ? can be realized in polynomial space. Proof. As non-deterministic polynomial space is equal to deterministic polynomial space, we give a non-deterministic algorithm. To prove the non-emptiness of the language recognized by A we only have to construct an accepting run of A’ . The algorithm starts with the initial state ’ and guesses a letter a1 and a minimal model

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

111

Fig. 1. A’ for ’ = [Mod 1; 3 (Xpa ∨ pb )] ∧ [pa Upb ].

for (’; a1 ) (seen as a boolean positive formula). Then, it guesses the next letter a2 and for any state appearing in the minimal model, it guesses a minimal model for its image by reading a2 and therefore computes a set of states modeling all the preceding formulas (the algorithm works with a set of states and therefore it only needs a linear space to recall it) and so on. Finally, it decides to stop and accepts if all the actual states are ?nal states. To guess a minimal model of a boolean positive formula it su ces to explore all the possible valuations what gives the size of a minimal model and then to guess one of the minimal models. This can be made in polynomial space and therefore the entire algorithm only needs polynomial space. In fact, the algorithm could just guess a model without verifying it is a minimal one, as by non-determinism there exists a run of the algorithm where all guessed models are minimal. We therefore have the following corollary: Corollary 2. Deciding whether an GLTL-formula (or a GTL-formula) is satis?able is a PSPACE-complete problem.

112

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

Proof. The PSPACE membership is a consequence of Theorems 15 and 16. The PSPACE-hardness is a consequence of the PSPACE-hardness for the same problem restricted to PTL-formulas [10]. 9. Conclusion Using vectorial algorithms we have given new characterizations of star-free languages (as the class of PTL-vectorial languages), of solvable languages (as the class of MTL-vectorial languages) and of regular languages (as the class of GTLvectorial languages). However, even in the easiest case, that is for star-free languages, there is no general e cient method to compute an algorithm associated with a given language. Nevertheless, since vectorial languages are closely related with temporal logic this is not that surprising at all, as the computation of an algorithm associated with an automaton is at least as di cult as ?nding a temporal logic formula associated with a given language, which is exponential with regard to the automaton. We have characterized subsets of vectorial operations by equivalent sets of temporal logic operators. It is interesting to note that vectorial algorithms provide a more detailed information about an automaton than logical formulas without any loss in computational complexity and in the complexity of the operators used in both models. Finally, we have shown that deciding the validity of a GTL-vectorial algorithm is PSPACE-complete. As a byproduct we have obtained that the extension of LTL with group operators does not change the complexity of the satis?ability problem, which is still PSPACE-complete, and we have given an e ective algorithm deciding this question. Appendix A. Proof of Theorem 14 The aim is to prove that if ’ is a positive LTL-formula, then we have that L’ = L(A’ ), where A’ is the automaton associated with ’. For this we reason by induction on the formula ’: (1) If ’ = pa then A’ is the following alternating automaton:

and therefore it easily seen that A’ recognizes the language: L(A’ ) = {aw | w ∈ A? } = L’ .

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

113

(2) If ’ = ’1 ∨ ’2 then any run of A’ has the following form:

where a1 is the ?rst letter of the word and where one of the following runs is a run of A’1 for the ?rst one and of A’2 for the second one:

Therefore, we have that L(A’ ) = L(A’1 ) ∪ L(A’2 ). By induction hypothesis we thus have that L’ = L(A’ ). (3) If ’ = ’1 ∧ ’2 then any run of A’ has the following form:

where a1 is the ?rst letter of the word and where the following runs are runs of A’1 for the ?rst one and of A’2 for the second one:

Therefore, we have that L(A’ ) = L(A’1 ) ∩ L(A’2 ). By induction hypothesis we thus have that L’ = L(A’ ). (4) If ’ = X’1 then A’ has the following form:

where A’1 is equal to A’1 except that ’1 is not an initial state. The outgoing transitions from ’ to A’1 go to the state ’1 .

114

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

Therefore, we have that L(A’ ) = a∈A aL(A’1 ), and the induction hypothesis concludes this case: L’ = L(A’ ). (5) If ’ = ’1 U’2 . A run for A’ on a non-empty word u whose ?rst letter is a1 can have two di erent forms:

where T3 is a run of A’ , and where the following runs are, respectively, a run of A’1 for the ?rst one and a run of A’2 for the second one:

By induction hypothesis, the ?rst run is an accepting run for u if and only if (u; 1) |= ’2 and the second one is accepting if and only if (u; 1) |= ’1 and T3 is an accepting run of A’ . As the root of T3 is ’ = ’1 U’2 and as ’ is not a ?nal state this implies that T3 cannot be reduced to its root. Therefore, by an easy induction on the length of u, it follows that u is recognized by A’ if and only if there exists i, 16i6|u| such that for all j , 16j?i we have (u; j ) |= ’1 and (u; i) |= ’2 (This means that we cannot have always the second kind of run). Therefore, u is recognized by A’ if and only if (u; 1) |= ’. This implies that L’ = L(A’ ). (6) If ’ = ’1 R’2 . A run for A’ on a non-empty word u whose ?rst letter is a1 can have two di erent forms:

where T3 is a run of A’ , and where the following runs are, respectively, a run of A’1 for the ?rst one and a run of A’2 for the second one:

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

115

By induction hypothesis, the ?rst run is an accepting run for u if and only if (u; 1) |= ’2 and (u; 1) |= ’1 . The second one is accepting if and only if (u; 1) |= ’2 and T3 is an accepting run of A’ . As the root of T3 is ’ and as ’ = ’1 R’2 is a ?nal state this implies that T3 can be reduced to its root. Therefore, by an easy induction on the length of u, it follows that u is recognized by A’ if and only if one of the following cases is true: (i) For all i, 16i6|u|, (u; i) |= ’2 . (ii) There exists i, 16i6|u| such that for all j , 16j 6i we have (u; j ) |= ’2 and (u; i) |= ’1 (The condition on ’2 to be satis?ed is released at position i as ’1 is satis?ed). This exactly means that u is recognized by A’ if and only if (u; 1) |= ’. This implies that L’ = L(A’ ). This induction proves that for any LTL-formula ’ we have that L’ = L(A’ ).

Acknowledgements I gratefully acknowledge the many helpful suggestions of Anca Muscholl during the preparation of the paper. I also wish to express my thanks to Jean-Eric Pin for suggesting many stimulating ideas.

References

[1] A. Baziramwabo, P. McKenzie, D. Therien, Modular temporal logic, in: 14th Symp. on Logic in Computer Science (LICS’99), Trento, Italy, IEEE, New York, 1999, pp. 344 –351. [2] A. Bergeron, S. Hamel, Cascade decomposition are bit-vector algorithms, in: Implementation and Application of Automata, 6th Internat. Conf., CIAA 2001, Pretoria, South Africa, July 23–25, 2001, Revised Papers, Lecture Notes in Computer Science, Vol. 2494, Springer, Berlin, 2002, pp. 13– 66. [3] A. Bergeron, S. Hamel, Vector algorithms for approximate string matching, Internat. J. Found. Comput. Sci. 13 (1) (2002) 53–66. [4] J. Cohen, D. Perrin, J.-E. Pin, On the expressive power of temporal logic for ?nite words, J. Comput. System Sci. 46 (1993) 271–294. [5] J.A. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968. [6] R. McNaughton, S. Papert, Counter-Free Automata, MIT Press, Cambridge, MA, 1971. [7] J.-E. Pin, Varieties of Formal Languages, North Oxford, London, Plenum, New York, 1986 (Translation of Vari? et? es de langages formels). [8] J.-E. Pin, Syntactic semigroups, in: G. Rozenberg, A. Salomaa (Eds.), Handbook of Formal Languages, Vol. 1, Springer, Berlin, 1997, pp. 679 – 476 (Chapter 10). [9] M.P. Schutzenberger, On ?nite monoids having only trivial subgroups, Inform. Control 8 (1965) 190–194. [10] A.P. Sistla, E.M. Clarke, The complexity of propositional linear temporal logics, J. Assoc. Comput. Mach. 32 (3) (1985) 733–749. [11] H. Straubing, Families or recognizable sets corresponding to certain varieties of ?nite monoids, J. Pure Appl. Algebra 15 (1979) 305–318. [12] H. Straubing, Finite Automata, Formal Logic, and Circuit Complexity, Birkhauser, Basel, 1994.

116

O. Serre / Theoretical Computer Science 310 (2004) 79 – 116

[13] M.Y. Vardi, An automata-theoretic approach to linear-temporal logic, in: F. Moller, G. Birtwistle (Eds.), Logics for Concurrency, Lecture Notes in Computer Science, Vol. 1043, Springer, Berlin, 1996, pp. 238–266. [14] Th. Wilke, Classifying discrete temporal properties, Habilitation Thesis, Kiel, Germany, 1998. [15] Th. Wilke, Classifying discrete temporal properties, in: STACS 99 Lecture Notes in Computer Science, Vol. 1563, Springer, Berlin, 1999, pp. 32– 46.

赞助商链接

- Simple on-the-fly automatic verification of linear temporal logic
- Dynamic Linear Time Temporal Logic
- Algorithmic verification of linear temporal logic specifications
- Distributed Versions of Linear Time Temporal Logic
- in linear temporal logic
- Simple on-the-fly automatic verification of linear temporal logic
- Dynamic Linear Time Temporal Logic
- Model checking linear temporal logic using tabled logic programming
- Temporal and Modal Logic Programming Languages
- Propositional linear temporal logic and language homomorphisms
- Tense, Temporal Reference, and Tense Logic
- Stutter-invariant Languages, !-Automata, and Temporal Logic
- A tableau system for linear temporal logic
- Algorithmic verification of linear temporal logic specifications
- Nesting Until and Since in linear temporal logic

更多相关文章：
更多相关标签：