# First-order logic with two variables and unary temporal logic

发布时间:2021-11-29 06:24:02

Basic Research in Computer Science BRICS RS-97-5 Etessami et al.: First-Order Logic with Two Variables and Unary Temporal Logic

BRICS

First-Order Logic with Two Variables and Unary Temporal Logic

Kousha Etessami Moshe Y. Vardi Thomas Wilke

BRICS Report Series ISSN 0909-0878

RS-97-5 March 1997

Copyright c 1997,

BRICS, Department of Computer Science University of Aarhus. All rights reserved. Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting: BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs: http://www.brics.dk ftp://ftp.brics.dk This document in subdirectory RS/97/5/

First-Order Logic with Two Variables and Unary Temporal Logic

Kousha Etessamiy Moshe Y. Vardiz Thomas Wilkex

Abstract

! -words and ?nite words, a logic denoted by FO2 . We prove that FO2 can

express precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quanti?er depth of the ?rst-order formula. We show that this translation is optimal. While satis?ability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satis?ability for FO2 is NEXP-complete, in sharp contrast to the fact that satis?ability for FO3 has non-elementary computational complexity. Our NEXP time upper bound for FO2 satis?ability has the advantage of being in terms of the quanti?er depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satis?able FO2 formula has a model whose “size” is at most exponential in the quanti?er depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary- TL is based on an analysis of unary-TL types.

Part of the research reported here was conducted while the authors were visiting DIMACS as part of the Special Year on Logic and Algorithms. y Basic Research in Computer Science (BRICS), Centre of the Danish National Research Foundation. This research supported by the ESPRIT Long Term Research Programme of the EU under project number 20244 (ALCOM-IT). email: kousha@brics.dk. z Department of Computer Science, Rice University. email: vardi@cs.rice.edu. During the preparation of this paper this author was partially supported by an NSF Grant. x Institut f¨ r Informatik und Prakt. Math., Christian-Albrechts-Universit¨ t zu Kiel, Germany. u a email: tw@informatik.uni-kiel.de

We investigate the power of ?rst-order logic with only two variables over

1 Introduction

Over the past three decades a considerable amount of knowledge has accumulated regarding the relationship between ?rst-order and temporal logic over both ?nite words and ! -words: the ?rst-order expressible properties are exactly those expressible in temporal logic [Kam68, GPSS80, GHR94]; three variables suf?ce for expressing all the ?rst-order expressible properties [Kam68, IK89]; while satis?ability for ?rst-order logic with three variables has non-elementary computational complexity [Sto74], the satis?ability problem for temporal logic is PSPACE-complete [SC85]; moreover, there are classes of ?rst-order formulas with three variables whose smallest equivalent temporal formulas require nonelementarily larger size (a consequence derivable from [Sto74]). In computer science the importance of this work stems from the practical relevance of temporal logic, which is used extensively today to specify and verify properties of reactive systems (see, e.g., [Pnu77] and [MP92]). In this paper we provide a scaled down study of the relationship between ?rstorder and temporal logic. Looking at ?rst-order logic with only two variables, we show that the tight correspondence to temporal logic persists. We prove that ?rstorder logic with two variables, denoted by FO2 , has precisely the same expressive power as temporal logic with the usual future and past unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, but without the binary operators “until” and “since”, a logic we denote by unary- TL. In other words, FO2 coincides with the lowest level of the combined until/since hierarchy (which is known to be in?nite [EW96]). By contrast to the quite dif?cult proofs available for the correspondence between full ?rst-order logic and temporal logic (cf., e.g., [Kam68, GPSS80, GHR94]), our proof that FO2 = unary-TL is an easily understood inductive translation. In fact, our proof yields the following much stronger assertions: (1) FO2 formulas can be translated to equivalent unary-TL formulas that are at most exponentially larger and whose operator depth is at most twice the quanti?er depth of the ?rstorder formula, and (2) the translation can be carried out in time polynomial in the size of the output formula. We show that our translation is essentially optimal by exhibiting a sequence of 2 formulas that require exponentially larger unary- TL formulas. Thus, while FO with just three variables there is already a non-elementary gap between the succinctness of ?rst-order logic and full temporal logic, FO2 remains more succinct than unary-TL but not nearly as much: an exponential blowup is exactly what is necessary in the worst-case. 2

The same result that shows that satis?ability for temporal logic is PSPACEcomplete ([SC85]) also shows that satis?ability remains PSPACE-complete for unary-TL. We prove on the other hand that satis?ability for FO2 is NEXPcomplete. This again contrasts sharply with the non-elementary complexity of satis?ability for FO3 . Moreover, this is surprising given that FO2 is exponentially more succinct than unary-TL, and that satis?ability for unary-TL is PSPACEcomplete, leading one to expect that FO2 satis?ability will be EXPSPACE-complete. Indeed, as a consequence of our NEXP bound it follows that FO2 formulas that require “large” (exponentially bigger) unary- TL expressions necessarily have models that are “very small” (subexponential) with respect to the size of their unary-TL expression. Such “very small” models do not exist in general for unary- TL, as we can easily express with an nO(1) size unary-TL formula a “counter” whose smallest model has size 2n . An interesting and related aspect of our NEXP upper bound is that the time bound is only in terms of the quanti?er depth of the FO2 formula. This is because we prove our upper bound using an unusually strong small model property for FO2, one which states that every satis?able FO2 formula has a model whose “size” is at most exponential in the quanti?er depth of the given formula, rather than the size of the entire formula. For large but shallow formulas the gap between these quantities can make a signi?cant difference. It should be noted here that in a recent result Gr¨ del, Kolaitis, and Vardi a [GKV97] have shown that satis?ability for two-variable ?rst-order formulas over arbitrary relational structures is computable in NEXP time. Their results also rely on a small model property. They prove that every satis?able two-variable formula over arbitrary structures has a ?nite model of size at most exponential in the size of the formula, improving on a previous doubly-exponential bound obtained by Mortimer [Mor74]. Despite the similarity between the statement of their result and ours, the two are essentially incompatible and neither result implies the other. The reasons for this are two-fold. First, our results hold over words, i.e., over a unary vocabulary with built-in ordering. In particular, unlike arbitrary structures, over words we do not have a genuine ?nite model property: with two variables one can say that for every position in the word there is a greater position. Secondly, our “small” model property (Theorem 4) shows that every satis?able formula has a model whose “size” is bounded exponentially by the quanti?er depth of the formula, whereas the small model property of [GKV97] depends on the size of the entire formula. Moreover, the proof techniques used in the two results are completely different. Our proof of the “small” model property for FO2 is facilitated by our transla3

tion. It is enough to prove the same small model property for unary- TL (in terms of operator depth instead of quanti?er depth) because our translation from FO2 to unary-TL at most doubles the quanti?er/operator depth. The existence of small models for unary-TL is established by an analysis of unary-TL types; these types behave quite differently than types for temporal logic in general. FO2 provides built-in binary predicates for a total order and a successor relation (besides free unary predicates). As further evidence of the robust correspondence between ?rst-order and temporal logic we show that even when FO2 is further restricted by removing the successor predicate, the relationship to temporal logic still persists: the resulting logic has exactly the same power as temporal logic with temporal operators “sometime in the future” and “sometime in the past” only. Moreover, we determine the complexity of satis?ability for this further restricted ?rst-order logic, and the corresponding temporal logic, as well as their difference in succinctness. All our results hold both for ?nite words and ! -words with only minor technical changes. In this conference paper we only deal with the more interesting case of ! -words. The paper is organized as follows. Section 2 introduces our notation and terminology. Section 3 presents the translation from FO2 to unary-TL and shows it is optimal. Section 4 establishes NEXP-completeness of satis?ability for FO2. In Section 5, we establish the small model property. Section 6 is concerned with FO2 without “successor” and unary-TL without “next” and “previously”. We conclude in Section 7.

2 Terminology and Notation

We work with ?rst-order logic over ! -words, where our vocabulary contains unary predicates from m = P0 ; P1 ; P2 ; : : :; Pm?1 for some m, and in addition contains the built-in predicates “suc” for “successor” and “<” for “less than”. We use FO2 to denote the class of properties de?nable by ?rst-order formulas '(x), where at most x occurs free, and where at most 2 variables occur in all of '. We will also informally use FO2 to refer to the set of such formulas. An FO2 formula '(x) naturally de?nes a property of !-words over the alphabet whose symbols are subsets of m = p0 ; : : : ; pm?1 , namely the property (2 m )! = ' 0] . Here = Pj (i) iff pj i for i 0, j < m. We use unary-TL to denote the class of properties of ! -words de?nable by linear temporal logic formulas built from atomic propositions from m , using

f

g

j

f

2

g

f 2

j j

g

4

the boolean connectives and the unary temporal operators h (“next”), h (“previously”), (“eventually” or “sometime in the future”), and (“sometime in the past”). We also use unary-TL to denote the set of such formulas. By convention, ( ; i) = ' if there exists a position j strictly greater than i such that ( ; j ) = '. The same applies to . Formulas ' and from FO2 over m or unary-TL over m are said to be equivalent if ( ; i) = ' iff ( ; i) = for all (2 m )! and i 0. A formula ' from FO2 over m or unary-TL over m is said to be satis?able if the property over 2 m it de?nes is non-empty. Let the atomic order formulas be x = y, suc(x; y), suc(y; x), x < y, and y < x. The length of a formula ' is denoted by ' , its quanti?er (operator) depth by qdp(') (respectively odp(')).

j

j

j

j

2

jj

3 Unary-TL = FO2

We prove that the logics unary-TL and FO2 are equally expressive. The nontrivial direction of this fact follows from the following much stronger statement: Theorem 1 Every FO2 formula '(x) can be converted to an equivalent unary-TL formula '0 with '0 2O(j'j (qdp(')+1)) and odp('0) 2 qdp('). Moreover, the translation is computable in time polynomially in '0 .

j j2

j j

The reverse translation is trivial, and linear in both size and operator/quanti?er depth. Note the contrast between the theorem and what follows from the work in [Sto74]: there is a non-elementary lower bound in terms of blow-up in size for any translation of ?rst-order formulas with three variables into temporal formulas. Proof of Theorem 1. Given an FO2 formula '(x) the translation procedure works a follows. When '(x) is atomic, i. e., of the form Pi x, it outputs pi . When '(x) is of the form 1 2 or —we say that '(x) is composite—it recursively 0 0 0 0 0. The two cases that remain computes 1 and 2, or 0 and outputs 1 2 or are when '(x) is of the form x' (x) or y' (x; y ). In both cases, we say that '(x) is existential. In the ?rst case, '(x) is equivalent to y' (y) and, viewing x as a dummy free variable in ' (y ), this reduces to the second case. In the second case, we can rewrite ' (x; y ) in the form

_

:

9

_ 9

:

9

' (x; y) =

( 0(x; y); ::; r?1(x; y); 0 (x); ::; s?1(x); 0 (y ); ::;

5

t?1(y ))

where is a propositional formula, each formula i is an atomic order formula, each formula i is an atomic or existential FO2 formula with qdp( i ) < qdp('), and each formula i is an atomic or existential FO2 formula with qdp( i ) < qdp('). In order to be able to recurse on subformulas of ' we have to separate the i ’s from the i ’s. We ?rst introduce a case distinction on which of the subformulas i hold or not. Let T and F denote true and false. We obtain the following equivalent formulation for ':

W

2fT, Fgs

( ( i $ i) ^

i<s

^

9y ( 0; ::;

r?1; 0 ; ::; s?1 ; 0 ; ::; t?1))

We proceed by a case distinction on which order relation holds between x and y . We consider ?ve mutually exclusive cases, determined by the following formulas, which we call order types: x = y , suc(x; y ), suc(y; x), x < y suc(x; y), y < x suc(y; x). When we assume that one of these order types is true, each atomic order formula evaluates to either T or F, in particular, each of the i ’s evaluates to either T or F; we will denote this truth value by i . We can ?nally rewrite ' as follows, where stands for the set of all order types:

^:

^:

W

2fT, Fgs

( ( i $ i) ^

i<s

_

^

2

9y( ^ ( 0; ::;

r?1;

; )))

Notice now the following. If is an order type, (x) an FO2 formula, and 0 an equivalent unary-TL formula, there is an obvious way to obtain a unary-TL formula ] equivalent to (y), see the following table:

^

x=y h0 suc(x; y) h0 suc(y; x) x < y ^ :suc(x; y) h 0 y < x ^ :suc(y; x) h 0

Our procedure will therefore recursively compute i0 for i < s and i0 for i < t 6

0

]

and output

W

2fT, Fgs

( ( i0 $ i ) ^

i<s

_

^

(1)

proof is inductive on the quanti?er depth of '. The basic observation is that there are 2s 2j'j possibilities for in the disjuction of line 1 above, and by the inductive hypothesis each disjunct has length at most c ' 2O(j'j (qdp('))), for a constant c. The stated bound for '0 follows by induction. That odp('0 ) 2 qdp(') follows from the conversions in the table above. It is straightforward to verify that our translation to '0 can be computed in time polynomial in '0 .

2 0 j and odp('0 ) are bounded as stated in the theorem. The Now we verify that j'

( 0; ::;

r?1;

; ))

(2)

j j

jj

j j

An exponential blow-up, as incurred in the translation of Theorem 1, is necessary: Theorem 2 There is a sequence ('n )n 1 of FO2 sentences over 1 of size (n2 ) such that the shortest temporal logic formulas equivalent to 'n have size 2 (n) .

O

Proof. We give only a proof for an unbounded vocabulary; in this case the formulas 'n can be chosen to be of size (n). The formula 'n is a formula over n+1 that de?nes the following property, denoted Ln : “any two positions that agree on p0 , . . . , pn?1 also agree on pn ”. This is easily de?ned in FO2 within size linear in n:

O

i<n As every property (language) de?ned by any temporal logic formula ' (even with “until” or “since”) is recognized by a non-deterministic B¨ chi automaton u O(j'j) states, see [VW94], it is enough to show that every B¨ chi automaton with 2 u n for Ln requires at least 22 states. Suppose A recognizes Ln . Let a0 , . . . , a2n ?1 be any sequence of the 2n symbols of the alphabet 2 n . For every subset K of f0; : : : ; 2n ? 1g let wK be the word b0 . . . b2n ?1 with bi = ai if i 2 K and else bi = ai fpn g. Notice that there n ! ! are 22 such words. Also, wK j= ' and wK wK 6j= 'n for K 6= K 0 . Therefore, 0 and qK and qK are the states assumed by A in accepting runs for w! if K 6= K K ! and wK after 2n steps, then qK and qK have to be distinct, i. e., A needs at least 22n states.

0 0 0 0

'n = 8x8y( (Pix $ Piy) ! (Pn x $ Pn y)):

^

7

4 The Complexity of Satis?ability for FO2

We now show that the satis?ability problem for FO2 over ! -words is NEXPcomplete. This is in sharp contrast to the non-elementary lower bound for satis?ability of ?rst-order logic with three variables over words which follows from [Sto74]. Satis?ability for unary-TL remains, as with full TL, PSPACE-complete [SC85]. Theorem 3 Satis?ability for an FO2 formula ' over m is decidable in non2 deterministic time 2O(qdp(') m) , and thus satis?ability for FO2 is in NEXP. As a main tool for our NEXP upper bound we prove a strong small model property for FO2 which is of interest in its own right: Theorem 4 Every satis?able FO2 formula ' over m has a model of the form uv!, where both u and v have length bounded by 2O(qdp(')2m). We will prove Theorem 4 in Section 5. The other ingredient in our NEXP upper bound is the following lemma, which allows us to ?nd out, given strings u and v , whether uv ! satis?es an FO2 formula ' by just checking ' on the string uv2d+1, where d is the quanti?er depth of '. Lemma 1 Let '(x) be an FO2 formula, and let and let d = qdp('). 1. For r 0 and 0 s < v ,

u and v be words with jvj > 2,

2.

jj uv! j= ' juj + 2djvj + s] iff uv! j= ' juj + (2d + r)jvj + s] (3) In particular, if '(x) = 9y' (x; y ) and uv ! j= ' i] with i < juv 2d+1j, then there exists j juv 2d+3j such that uv ! j= ' i; j ].

Proof. Part 2 follows from the proof of part 1. The proof for part 1 is by induction on the quanti?er depth d. Base case: When '(x) is quanti?er free, the only thing we can say about the only variable x is which predicates hold at x, and clearly the predicates that hold at a position j = uv + q v + r are exactly those that hold at u + r (simply because we are at the same position in the word v ).

j j

jj

jj

8

where denotes a boolean combination of the given formulas and each i (x; y ) is an atomic order relation (i.e., one of x < y , suc(y; x), etc.). We will argue that part 1 holds for formulas of the form '0 and it will follow that it holds for ' as well because the “iff” in part 1 is preserved under boolean combination. ( ) Suppose ' j ] holds for j = u + (2(d + 1) + r) v + s, where r 0 and 0 s v . Then there is a witness for y, namely a position k at which ( 1 j; k]; : : :; l j; k]; 1 j ]; : : :; m j ]; 1 k]; : : :; c k]) holds. We consider sev0 eral cases based on the location of k in uv ! . Let jd+1 = u + 2(d + 1) v + s. We 0 want to show that ' jd+1 ] also holds.

Inductive case: Assume true for d, we prove the assertion for d + 1. Our formula '(x) of depth d + 1 is a boolean combination of formulas '0(x) of the form: y ( 1; : : :; l; 1(x); : : :; m(x); 1(y); : : :; c(y))

9

(

jj

jj

jj

jj

jj

1.

j

0 k: In this case we know by the inductive hypothesis that jd+1 satis?es 0 the same i ’s as j , and that jd+1 + (k ? j ) satis?es the same i ’s as k , and 0 just as k is for j , because their juxtaposition is thus is a witness for jd+1

exactly the same.

2. 3.

juj + (2d + 1)jvj k < j : In this case the exact same argument as in case

1 works, with the roles of k and j reversed.

k < juj + (2d + 1)jvj: In this case, we can ?x k as a witness for both j and 0 0 jd+1 because, given that jvj > 2, the order type of (k; jd+1) and (k; j ) is the

same.

( ) Suppose that ' j ] holds for j where uv 2d+2 j < uv2d+3 . Then the claim is that ' j 0] holds for j 0 = j + r v and for all r. This is again split into cases based on the location of the witness k .

)

jj

j

j

j

j

1. 2. 3.

j k: But then j + rjvj has a witness at k + rjvj. juj + (2d + 1)jvj k < j : In this case again j + rjvj has k + rjvj as a

witness.

k < juj + (2d + 1)jvj: Now again as in the second case above k is a witness for both j and j + rjv j because, given that jv j > 2, the order types of (k; j ) and (k; j + rjv j) are the same.

9

Proof of Theorem 3. The non-deterministic algorithm determines the satis?ability of an FO2 formula '(x) over m as follows. It ?rst guesses u and v of 2 length bounded by 2O(qdp(') m) . It then builds up a table that contains for every i < uv 2d+1 and for every subformula (z ) of '(x) a bit saying whether uv! = i]. This is done inductively. The entry for an atomic or composite (see proof of Theorem 1) is easily determined. From Lemma 1, part 2, it follows that in order to determine whether or not an existential formula (see proof of Theorem 1) of the form y ( (x; y ); (x); (y )) holds at a position i < uv 2d+1 it suf?ces to consider only positions < uv 2d+3 for y . Whether or not a formula (y) holds at such a position can be determined by a lookup in the table according to (3). The algorithm outputs the entry for position 0 and '(x). Now to conclude that FO2 satis?ability is NEXP-complete, we observe that

j

j

j

9

j

j

j

j

it is NEXP-hard. This follows from the work of [Le80, F¨ 84]. We sketch the u reduction for completeness: Theorem 5 ([Le80, Fu84]) FO2 satis?ability is NEXP-hard. In fact, even satis?¨ 2 over , as well as satis?ability for FO2 formulas that do not use ability for FO 1 “suc” and “<” are NEXP-hard. Proof. We only sketch the proof for showing that satis?ability for FO2 without either “suc” or “<” is NEXP-hard. We give a reduction from the problem of determining whether for a given tiling system T 0; 1; : : : ; c 1 4 with c colors and a given initial row x T + of length n there exists a tiling of a 2n 2n square consistent with T and with x occurring in the lower left corner. (Recall that an T is considered a square tile with left edge colored by element c1 ; c2 ; c3 ; c4 c1, right edge colored by c2, etc. A tiling is consistent if adjacent edges carry the same color.) This problem is known to be NEXP-complete, see, e. g., [F¨ 84]. We u can, with a short FO2 formula, name the adjacent positions in a tiling (and check their consistency) by exploiting the fact that addition has poly-sized propositional formulae. The predicates are used to specify the address coordinates, as well as tile content, of positions in the tiling.

2

f

?g

h

i2

5 A small model property for FO2

Theorem 1 tells us that every FO2 formula of depth k can be translated into an equivalent unary-TL formula of depth 2k . Thus in order to prove Theorem 4 it suf?ces to prove the same small model property for unary- TL, namely: 10

Theorem 6 Every satis?able unary-TL formula ' over m has a model 2 where the sizes of u and v are bounded by 2O(odp(') m) .

uv!

We mention without proof that such a small model property does not hold for temporal logic in general. In fact, one can prove a non-elementary lower bound on the size of small models of temporal logic formulas in terms of operator depth. We also mention that there is a family of satis?able unary-TL formulas 'n over m of depth (n) where the smallest models have size (2mn ). We ?rst sketch a proof of Theorem 6 and then go into details. Let k; k 0 0. We say that a unary-TL formula ' is of depth (at most) (k; k 0) if it is of depth (at most) k in and depth (at most) k 0 in h Given an ! -word w and a position i 0, . w the (k; k 0) type of i in w, denoted k;k (i), is the set of all unary-TL formulas of w depth at most (k; k 0 ) that hold in w at i. This means that w = ' iff ' k;k (0) 0 ). It is thus enough to show that for for every formula ' of operator depth (k; k 2 every ! -word w there exist u and v of size bounded by 2O((k+k +1) m) such that w w 0 ! k;k (0) = k;k (0) for w = uv . In order to establish this, we ?rst show that for every ! -word w one can ?nd u and v such that w and uv ! agree on the types of position 0 and such that u and v are bounded polynomially in the number of types that occur in w. We then show that the number of types occurring in a given !-word is bounded by 2O((k+k +1)2m). (Notice that the number of (0; 0) types occurring in any ! -word over m is already in (2m ).) The following lemma establishes that the (k + 1; k 0 ) type of a position i in a given word w is determined uniquely by (1) i’s local neighborhood, (2) the (k; k 0 ) types that occur to its right, and (3) the (k; k 0) types that occur to its left.

O

0

j

2

0

0

0

0

0

0

Lemma 2 Let w and w0 be ! -words and i, i0 0. 0 0 w 0 w 1. 0;k (i) = 0;k (i0) iff wi?k : : : wi : : : wi+k = wi ?k : : : wi : : : wi +k where, 0 by convention, wj = $ and wj = $ for j < 0 ($ being a special symbol). w w w w w 2. k+1;k (i) = k+1;k (i0) if and only if 0;k (i) = 0;k (i0), k;k (j ) j < i = 0 w w 0 w k;k (j ) j < i , and k;k (j ) j > i = k;k (j ) j > i .

0 0 0 0 0 0 0 0 0 0 0 0

f

0

0

0

j

g

0

f

0

j

g f

0

0

0

0

j

f

0

g

j

g

Proof. Part 1 is clear: A depth k 0 formula that uses no operator can describe completely the content of the k 0 -neighborhood of the current position, and nothing more. To prove part 2 we proceed by induction on k . The base case, k = 0, is immediate. Assume true for k , we prove the claim for k + 1. w w ( ) If k+1;k (i) = k+1;k (i0) then in particular (w; i) and (w0; i0 ) agree on all w w depth (0; k ) formulas, and thus 0;k (i) = 0;k (i0).

)

0

0

0

0

0

0

11

0 w w 0 w To show k;k (j ) j > i k;k (j ) j > i , let k;k (j ) j > i . There are only a bounded number of inequivalent formulas of depth (k; k 0) (this can be proved by a straightforward induction). Let k;k denote the set of such formulas. There is thus a formula

0 0 0 0 0

f

j

g f

=

^

j

g

2f

j

g

'2

'^

0

^

2 k;k n

0

:

0

which holds in a word precisely at those positions having (k; k 0 )-type 0. But then is a depth (k + 1; k 0 ) formula that holds at (w0 ; i0) precisely when 0 0 w w w k;k (j ) k;k (j ) j > i . A symmetric proof shows that k;k (j ) j > i w w j > i0 , and thus k;k (j ) j > i = k;k (j ) j > i0 . A similar proof shows w w that k;k (j ) j < i = k;k (j ) j < i0 . w w ( ) Assume that 0w;k (i) = 0w;k (i0), k;k (j ) j < i = k;k (j ) j < i0 , w w and k;k (j ) j > i = k;k (j ) j > i0 . First observe that every unary- TL formula of depth (k; k 0 ) is equivalent to a formula 0 also of depth (k; k 0 ), where 0 is in a normal form where all h have been “moved in”, i.e., appear without any operators in their scope. In other words, every unary- TL formula of depth (k; k 0 ) is equivalent to a boolean combination of formulas of depth (k; k 0) starting with , and formulas of depth (0; k0). Thus we can restrict our attention to normal form formulas. Now, let be a depth (k + 1; k 0 ) formula in normal form. If the outermost connective of is h then it is a depth (0; k 0 ) formula. Thus, , 0 w w (i) = w (i0), w since by assumption 0;k 0;k k+1;k (i ). k+1;k (i) If the outermost connective of is then = . Now (w; i) = iff there w (j ). Hence, since by assumption w (j ) j > exists a j > i such that k;k k;k w w (i) w (i0). The case when i = k;k (j ) j > i0 , we have k+1;k k+1;k = is symmetric. To conclude the proof, note that the “ ” in the previous two paragraphs is preserved under boolean combination.

f

0

0

f ( f

g

j

0

j

g f

g f

0

0

j

0

0

0

j

g f

0

0

g f j g f j g

0 0

0

0

j

f

0

g

j

g f

0

0

0

2 j

0

j

g f

0

j

g

0

0

0

2

0

, 2

0

0

0

g f

0

0

j

g

2

0

2

0

, 2

f

j

0

j

0

,

Using Lemma 2, we can now establish the following lemma which shows how to collapse ! -words in order to get “smaller” ! -words without changing the type structure of the ! -word in an essential way. In the following lemma k 0 will be w ?xed, and we adopt the shorthand notation k for (w ) . k;k

0

Lemma 3 Let w = u0u1 u2 : : : be an ! -word.

12

w w 1. Assume i and j are positions such that i < j and k (i) = k (j ). Let 0 = u1 : : : uiuj +1 uj +2 : : : w w w w w Then k (l) = k (l) for l i and k (l) = k (l + (j i)) for l > i. 2. Assume i and j are positions such that (a) i < j , w w (b) k (i) = k (j ), w w (c) k (l) l 0 = k (l) l < i , and w w w w (d) k (l) i l < j = k (l) ! l0( k (l) = k (l0 )) . Let w0 = u0 : : : ui (ui+1 : : :uj )! . w w Then k (l) = k (l) for l i and kw (i + r(j i) + s) = kw (i + s) for r 0 and 0 s < j i.

0 0

?

f f

j j

g f j g g f j9 ?

g

0

0

?

Proof. We prove part 1 by induction on k . Base case, k = 0. When we cut out a piece of a word, we don’t change any of the characters we didn’t cut out, and moreover the characters in the k 0 -neighborhoods of a point remain the same, thus we don’t change (0; k 0 )-types of any point. w w Assume true for k . Suppose k+1 (i) = k+1 (j ). By part 2 of Lemma 2 it follows that

f kw (i + 1); : : : ; kw (j ? 1)g f kw (m) j m < ig f kw (i + 1); : : : ; kw (j ? 1)g f kw (m) j m > j g

Let

(4) (5)

(l) be the mapping de?ned by: (l) =

l l + (j ? i)

if l i otherwise

0

w w By the inductive hypothesis we know that for all l, k (l) = k ( (l)). w (m) m > l = w ( (m)) m > l = w (m) m > (l) , But then k k k the last equality following from containment 5. Similarly, using containment 4, w we have k (m) m l = kw ( (m)) m l = kw (m) m (l) . w w But then by part 2 of Lemma 2 we have k+1 (l) = k+1 ( (l)), which is what we wanted to prove. The proof of part 2 is again by induction on k . Base case, k = 0. For l i, given that i and j have the same k 0 -neighborhood, the k 0 -neighborhood of position l in w0 is the same as the k0 neighborhood of l in w. Also, for l = i + r(j i) + s,

f

0

0

j

g f

j

g f

j

g

f

j

g f

0

j

g f

j

g

?

13

by the same fact, l has the same k 0-neighborhood as i + s. The base case then follows from part 1 of Lemma 2. Suppose true for k , we prove the claim for k + 1. First note that (k + 1; k 0 )types constitute a re?nement of (k; k 0 )-types, meaning that two positions with the same (k + 1; k 0)-type have the same (k; k 0 )-type. Thus, given that (a) through (d) w w hold for k + 1, by the inductive hypothesis we know that k (l) = k (l) for l i w w and k (i + r(j i) + s) = k (i + s) for r 0 and 0 s < j i. Thus, in particular, we claim that for l i, kw (m) m > l = w (m) m > l . This is so because by (d) the in?nitely recurring (k + 1; k0)-types (and thus also in?nitely recurring (k; k 0 )-types) are precisely those that already occur w at i, i + 1, : : : ; i + (j i 1) = j 1. In a similar way it follows that k (m) m l = w (m) m l . Thus, by part 2 of Lemma 2, it follows that w w k+1 (l) = k+1 (l). w w A similar proof shows that k+1 (i + r(j i) + s) = k+1 (i + s), for r 0 and 0 s < (j i).

0 0

?

g

f

0

j

?

g f f

j

g

f

0

? ? j

g

?

0

j

0

?

?

From this lemma, we conclude: Lemma 4 Let w be an ! -word over 2 m and t the number of (k; k 0) types occurring in w. There exists w0 of the form uv ! such that the length of u and v is less w w than (t + 1)2 and such that k;k (0) = k;k (0).

0 0 0

Proof. Part 2 of Lemma 3 immediately implies we can assume w = uv ! for some u and v. We can also assume that u and v are chosen such that the assumptions of part 2 of Lemma 3 are given with i = u and j = uv . Now, let u and v be such that for every other such pair u0 and v 0 we have uv u0v0 . For contradiction, 2 . For every (k; k 0) type of a position s with i s < j assume ?rst v (t + 1) w pick a position i such that i i < j and k;k (i ) = . Since v (t + 1)2, we can ?nd two positions l and l0 carrying the same type such that i l < l0 < j and either i < l or l0 < i for each of the i ’s. Thus, by part 2 of Lemma 3, u0 = u and v0 = v0v1 : : : vl?jujvl ?juj+1 : : :vjvj?juj?1 would be a smaller pair. If u (t + 1)2 we obtain a contradiction in a similar way using part 1 of Lemma 3.

jj

jj

j j j j j j

0

jj

0

jj

We now upper bound the number of types that can occur in a given ! -word: Lemma 5 The number of (k; k 0 ) types occurring in any ! -word over m is at w most 23((2k +1)(m+1)+1), i. e., 0 23((2k +1)(m+1)+1) for every k;k (i) i m )! . w (2

0

2

jf

0

j

gj

0

14

Proof. The proof is by induction on k . Let w be any ! -word over m . Let t(k;k ) be the number of (k; k0) types occurring in w. For the base case, from Lemma 2, part 1, it is easy to see that t(0;k ) 2(2k +1)(m+1) . Now observe that the w sequence ( k;k (i) j < i )i 0 is an increasing sequence containing at most t(k;k ) w distinct elements. Similarly, the sequence ( k;k (j ) j > i )i 0 is a decreasing sequence containing at most t(k;k ) + 1 distinct elements. Therefore, there are only w w 2t(k;k ) + 1 many distinct pairs of the form ( k;k (j ) j < i ; k;k (j ) j > i ), (2t(k;k ) + 1)2(2k +1)(m+1), where, and thus, using Lemma 2, part 1, t(k+1;k ) (2k +1)(m+1) accounts for the number of distinct (0; k 0 ) types. The lemma again, 2 follows by induction.

0 0

f

0

j

g

0

0

0

f f

0

0

j j

0

g gf

0

0

0

j

g

0

0

Theorem 6 now follows from Lemma 4 together with Lemma 5; this also proves Theorem 4. We also prove a different small model property in terms of formula size (proof omitted): Theorem 7 1. Every satis?able FO2 formula ' has a model of size 2O(j'j) .

2. Satis?ability for an FO2 formula ' can also be decided in non-deterministic time 2O(j'j).

6 Further Restricting FO2 and Unary-TL

It is only natural to further restrict FO2 by allowing < as the only built-in predicate; we denote the resulting logic by FO2 <]. Correspondingly, one can consider the logical language that is obtained from unary-TL by disallowing the use of h and h we denote this language by TL ]. ; Obviously, TL ] can easily be translated into FO2 <]. A slight modi?cation of the translation from FO2 to unary-TL described in the proof of Theorem 1 yields the reverse translation, i. e., TL ] = FO2 <]. Corresponding to Theorem 1, we have: Theorem 8 Every FO2 formula '(x) can be converted to an equivalent formula '0 with '0 2O(j'j qdp(')) and odp('0) qdp(').

j j2

TL ]

As FO2 <] is a sublogic of FO2 , the upper bounds for the complexity of the satis?ability for FO2 carry over to FO 2 <]. Moreover, as we have seen in Theorem 5, even the hardness result carries over: 15

Theorem 9 Satis?ability for FO2 <] is NEXP-complete. In fact, satis?ability for an FO2 <] formula ' over m is decidable in non-deterministic time 2O(qdp(')m) and also in non-deterministic time 2O(j'j). 2 Note the difference between 2O(qdp(') m) in Theorem 3 and 2O(qdp(')m) in the above theorem. That satis?ability for FO2 <] is no less dif?cult than satis?ability for FO2 (both are NEXP-complete) contrasts with what happens to satis?ability when passing from unary-TL to TL ]. In [SC85], it was shown that satis?ability for the temporal logic where the only temporal operator is “at present or sometime in the future” is in NP. We show that satis?ability for TL ] (which now includes the past operator) remains in NP, and thus is NP-complete. This is obtained by proving a linear-size model property: for every satis?able TL ] formula ' there exist u and v with u ; v ' such that uv! = ' (proof omitted).

jjjj j j

j

7 Conclusion

We have shown that the close correspondence between ?rst-order and temporal logic over words persists when looking at ?rst-order formulas with only two variables, and we have presented an easily understood translation of these formulas into temporal formulas. Our translation is optimal: the formulas incur at most an exponential blow-up in size and we have proved that this is necessary in the worst case. The satis?ability problem for unary-TL is known to remain, as with full TL, PSPACE-complete, but we have shown that FO2 satis?ability is drastically simpler than FO3 satis?ability: the former is NEXP-complete, while the latter is known to require non-elementary complexity. Moreover, our NEXP upper bound for FO2 satis?ability, and the corresponding small model properties for FO2 and unary-TL, have the advantage of being only in terms of quanti?er/operator depth and the number of propositions in the vocabulary, rather than the size of the entire formula, a fact that may be of potential use when dealing with large but shallow formulas. Some remaining questions: (1) Given a regular language L (say, as a B¨ chi or u ?nite automaton), can we decide whether L is FO2 (and thus unary-TL) de?nable? [EW96, TW96b] obtained closely related results, but neither yields this particular fact. (2) Is the FO2 quanti?er alternation hierarchy strict? This question can also be phrased in terms of operator alternation in unary- TL. (3) Does satis?ability remain NEXP-hard for FO2 <] formulas (without successor) over a bounded 16

number of predicates? (4) Can the upper bound of the small model property for FO2 be improved to 2O(qdp(')+m)? This would make (the proof of) Theorem 7 obsolete.

References

[EW96] K. Etessami and Th. Wilke. An Until hierarchy for temporal logic. In 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, pages 108–117, 1996. [F¨ 84] u M. F¨ rer. The computational complexity of the unconstrained domino u problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, pages 312–319. Volume 171 in Lect. Notes in Comput. Sci., Springer, 1984.

[GHR94] D. M. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic, volume 1. Clarendon Press, Oxford, 1994. [GPSS80] D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Conference Record of the 7th Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nev., pages 163–173, 1980. [GKV97] E. Gr¨ del, Ph. G. Kolaitis, and M. Y. Vardi. On the Decision Problem a for Two-Variable First-Order Logic. To appear in Bulletin of the Assoc. for Symbolic Logic. [IK89] N. Immerman and D. Kozen. De?nability with bounded number of bound variables. Information and Computation, 83(2):121–139, 1989.

[Kam68] J. A. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. [Le80] H. R. Lewis. Complexity Results for Classes of Quanti?cational Formulas. J. Comput. System Sci., 21: 317–353, 1980.

[MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, Berlin/New York, 1992.

17

[Mor74] M. Mortimer. On languages with two variables. Z. Math. Logik Grundlag. Math., 21:135-140, 1975. [Pnu77] A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, pages 46–57, 1977. [SC85] [Sto74] A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. Assoc. Comput. Mach., 32(3):733–749, 1985. L. J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, Department of Electrical Engineering, MIT, 1974.

[TW96b] D. Th? rien and Th. Wilke. Temporal logic and semidirect products: An e effective characterization of the until hierarchy. In Proceedings of the 37th Annual Symposium on Foundations of Computer Science, Burlington, Vermont, pages 256–263, 1996. [VW94] M. Y. Vardi and P. Wolper. Reasoning about in?nite computations. Information and Computation 115: 1–37, 1994.

18

Recent BRICS Report Series Publications

RS-97-5 Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. FirstOrder Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings. RS-97-4 Richard Blute, Jos? e Desharnais, Abbas Edalat, and Prakash e Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings. RS-97-3 Carsten Butz and Ieke Moerdijk. A De?nability Theorem for First Order Logic. March 1997. 10 pp. RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp. RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation. RS-96-62 P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. i+13 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings. RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59–80. RS-96-60 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. U PPAAL in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431–434. RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995.