Stéphane Demri
email: demri@lsv.ens-cachan.fr.

A polynomial space construction of tree-like models for logics with local chains of modal connectives

Keywords: computational complexity, modal logic, Ladner-like algorithm, local agreement

The LA-logics ("logics with Local Agreement") are polymodal logics defined semantically such that at any world of a model, the sets of successors for the different accessibility relations can be linearly ordered and the accessibility relations are equivalence relations. In a previous work, we have shown that every LA-logic defined with a finite set of modal indices has an NP-complete satisfiability problem. In this paper, we introduce a class of LA-logics with a countably infinite set of modal indices and we show that the satisfiability problem is PSPACE-complete for every logic of such a class. The upper bound is shown by exhibiting a tree structure of the models. This allows us to establish a surprising correspondence between the modal depth of formulae and the number of occurrences of distinct modal connectives. More importantly, as a consequence, we can show the PSPACE-completeness of Gargov's logic DALLA and Nakamura's logic LGM restricted to modal indices that are rational numbers, for which the computational complexity characterization has been open until now. These logics are known to belong to the class of information logics and fuzzy modal logics, respectively.

Introduction

Complexity of modal logics. The worst-case complexity of modal logics is a flourishing research activity not only because of the ever growing number of new modal logics (program logics, temporal logics, description logics, information logics, . . . ) but also because known techniques in theoretical computer science can be applied to problems for such logics. The best illustration of this phenomenon has been the design of automata-theoretical decision procedures for dynamic and temporal logics (see e.g. (VW86; VW94; EJS01; Var98)) to quote two types of logics. Such an automata-based approach has been fruitful for characterizing EXPTIME-complete logics but it does not adapt easily to PSPACE-complete logics as far as satisfiability problems are concerned. For model-checking problems the situation differs essentially (VW94), e.g. for PLTL model-checking. In order to establish a PSPACE upper bound for the satisfiability problem of modal logics, one of the best known methods is due to Ladner [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] in which trees with branches of polynomial length are explored. Such a method admits numerous technical variants either based on decision procedures from analytic proof systems (see e.g. (HM92; Vig00; Dem01)) or based on semantics-based algorithms (see e.g. (Lad77; Spa93b; Dem00; Bal01; BS01)). When the models admit a tree-like structure, in order to establish the PSPACE upper bound, the main difficulty is to show that the path depth into the tree is polynomially bounded (a polynomially bounded branching width is easier to obtain). Unlike the EXPTIME decision procedure based on automata machinery, no path of exponential length needs to be constructed. In the present paper, we consider a class of multimodal logics that are shown to be PSPACE-complete. The lower bound is established by a reduction from QBF whereas the upper bound is shown via a Ladner-like algorithm.

Chains of S5 modal connectives. A standard result for multimodal logics due to [START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF] states that the multimodal logic with n independent S5 connectives has a PSPACE-complete satisfiability problem as soon as n is greater than two. This upper bound is preserved if we consider a countably infinite set of S5 modal connectives instead of a finite one. Surprisingly, in the finite case, the problem becomes NP-complete if the equivalence relations are ordered locally [START_REF] Demri | A class of decidable information logics[END_REF], that is to say, in the models for every world w ∈ W , for all relation indices i, j ∈ {1, . . . , n}, either R i (w) ⊆ R j (w) or R j (w) ⊆ R i (w). In other words, for every world w ∈ W , there is a permutation σ on {1, . . . , n} such that R σ(1) (w) ⊆ . . . ⊆ R σ(n) (w).

The binary relations R i and R j are said to be in local agreement [START_REF] Gargov | Two completeness theorems in the logic for data analysis[END_REF]. The NP-completeness is preserved if we consider chains of relations of the form

R 1 ⊆ R 2 ⊆ . . . ⊆ R n ,
that is to say we enforce the permutation σ to be identity. However, it is open whether the problem remains in NP if a countably infinite set of connectives is considered.

Our contribution. We introduce a class of multimodal logics with a countably infinite set of modal connectives characterized by models in which the local agreement condition holds between any two equivalence relations of the models. The logics in the class, called nice unbounded LA-logics, differ by the admitted permutations σ that can locally occur. For instance, such a class contains the logic for which the relations of the models satisfy

R 0 ⊆ R 1 ⊆ . . . ⊆ R n ⊆ . . . .
We show that every logic in that class has a PSPACE-complete satisfiability problem. The lower bound is obtained by reducing QBF, a well-known PSPACE-complete problem [START_REF] Stockmeyer | The polynomial-time hierarchy[END_REF]. The PSPACE upper bound is shown with a sophisticated Ladner-like procedure. Hence, the NP upper bound of the finite case does not extend to the infinite case (unless PSPACE = NP). This is in sharp contrast with the situation for independent S5 modal connectives and is reminiscent of the complexity of the basic modal logic K restricted to formulae of fixed modal depth: K satisfiability is PSPACE-complete (Lad77) whereas for every fixed k ≥ 0, K satisfiability restricted to formulae of modal depth at most k is NP-complete (Hal95). So, in nice unbounded LA-logics the number of distinct modal connectives occurring in a formula can be viewed as a measure of the modal depth as far as complexity issues are concerned. Actually, such a statement can be made even more precise for certain nice unbounded LA-logics (see e.g. Corollary 2.3). As applications of our main result, the logic DALLA introduced in (Gar86) (see also [START_REF] Ph | A hierarchy of modal logics with relative accessibility relations[END_REF] for an equivalent logic defined with relative accessibility relations) is shown to be PSPACE-complete. The best known upper bound was NEXPTIME and the best known lower bound was NP. Moreover, Nakamura's logic LGM (Nak93) restricted to modal indices in the set of rational numbers is also shown to be PSPACE-complete.

The reason why DALLA is of interest to model reasoning in presence of incomplete information is the following. The Data Analysis Logic DAL (FdCO85) is the paradigm logic for reasoning about indiscernibility relations derived from information systems (Paw91). Unfortunately, very few results are known for DAL (its decidability status for example). That is why, variants of DAL have been proposed for which more results have been established while preserving some important features of DAL (see e.g. (Gar86; AT89; Bal96)). One of such logics is the logic DALLA introduced in (Gar86). An axiomatization is proposed in (Gar86) and the first decidability proof appeared in [START_REF] Demri | The validity problem for the logic DALLA is decidable[END_REF].

More about DAL and DALLA can be found in the forthcoming (DO) (see also Section 5).

It is possible to adapt our results to logics for which the relations in the mod-els are not necessarily equivalence relations but the PSPACE-completeness result is far less interesting since the standard modal logics K, T, B, and S4 are already known to be PSPACE-complete (Lad77; CL94).

Related work.

The paper uses the presentation of Ladner-like algorithms from (Spa93b) as it is also done in (Dem00). More generally, the PSPACE procedure designed in the paper is closely related in spirit to algorithms presented in (Lad77; HM92; Spa93b; BS01).

Plan of the paper. The rest of the paper is structured as follows. In Section 2, we introduce the class of LA-logics, remarkable elements in it and subclasses that are of particular interest in our computational complexity investigations. In Section 3, we show that every nice unbounded LA-logic has a PSPACE-hard satisfiability problem by taking advantage of the tree-like structure of the models. A Ladner-like algorithm for nice unbounded LA-logics is studied in Section 4, which allows us to conclude that every nice unbounded LA-logic has a satisfiability problem in PSPACE. In Section 5, we show how the PSPACE-completeness for the auxiliary logics DALLA and LGM can be lifted to Gargov's logic DALLA and Nakamura's logic LGM, respectively. Section 6 contains concluding remarks.

Some of the proofs are relegated to the appendix in order to facilitate the reading.

Logics with local agreement

In this section, we introduce the class of nice unbounded LA-logics which are modal logics defined semantically with a countable number of modal connectives. Some of the logics in this class are of special interest since they can be related to the logics DALLA (Gar86; DO98) and LGM [START_REF] Nakamura | On a logic based on graded modalities[END_REF]. Studying a class of modal logics in which some members are distinguished is a natural approach in modal logic theory, see e.g. (Sah75; Spa93a; Kra96) to quote only a few examples.

Language

Given the set PRP = {p i , r i , d i : i ≥ 0} of propositional variables, the set FOR of modal formulae φ is inductively defined as follows:

φ ::= p i | r i | d i | ¬φ | φ ∧ φ | φ ⇒ φ | φ ⇔ φ | φ ∨ φ | [i]φ,
where i ∈ N. For every i ≥ 0, we write FOR i to denote the fragment of FOR restricted to modal connectives in {[0], . . . , [i]}. All the natural numbers occurring in formulae are encoded in binary writing as a bit-string. For the sake of simplicity, we always write n in decimal representation. Standard abbreviations include i , , ⊥. The set sub(φ) of subformulae of the formula φ is defined in the standard way. We write N(φ) to denote the finite subset of N of modal indices occurring in φ. For instance, for every i ≥ 0, for every φ ∈ FOR i , N(φ) ⊆ {0, . . . , i}. The modal depth of an occurrence of a formula ψ in φ is the number of occurrences of elements of the form [i] in φ such that ψ is in their scope. We write md(φ) to denote the modal depth of the formula φ, that is the maximum of the modal depths of the subformulae of φ.

Semantics

A frame is a structure F = W, (R i ) i∈N such that W is a non-empty set and for every i ∈ N, R i is a binary relation on W . Similarly, an i-frame is a structure of the form

W, R 0 , R 1 , . . . , R i . A model [resp. i-model] is a structure M = W, (R i ) i∈N , V [resp. M = W, R 0 , . . . , R i , V ] such that F = W, (R i ) i∈N [resp. F = W, R 0 , . . . , R i ] is a frame [resp. an i-frame] and V is a valuation V : PRP → 2 W .
The satisfiability relation |= is defined inductively in the usual way:

• M, x |= p def ⇔ x ∈ V (p) for every p ∈ PRP; • M, x |= φ 1 ∧ φ 2 def ⇔ M, x |= φ 1 and M, x |= φ 2 ; • M, x |= ¬φ def ⇔ not M, x |= φ; • M, x |= [i]φ def ⇔ for every x ∈ R i (x), we have M, x |= φ, where R i (x) def = {x ∈ W : x, x ∈ R i }.
We omit the standard clauses for the other connectives. A modal formula φ is said to be true in the model M (written M |= φ) def ⇔ for every x ∈ W , M, x |= φ. A modal formula φ is said to be true in the frame F (written F |= φ) def ⇔ φ is true in every model based on F.

LA-logics

The definitions in Section 2.1 and 2.2 are quite standard. In the sequel, we introduce the class of unbounded LA-logics (as a subclass of logics introduced in (Dem98)) in which each logic is characterized by a set of linear orders over N.

An unbounded LA-logic [resp. bounded LA-logic] L is a pair FOR, S [resp. FOR i , S for some i ≥ 0] where S is a non-empty class of frames [resp. i-frames] such that there exists a non-empty class lo(L) of linear orders3 on N [resp. on {0, . . . , i}] such that for every frame F = W, (R i ) i∈N [resp. i-frame F = W, R 0 , . . . , R i ], F ∈ S def ⇔ (EQUIV) for every j ∈ N [resp. j ∈ {0, . . . , i}], R j is an equivalence relation; (LA) for every w ∈ W , there is ∈ lo(L) such that for all j, j ∈ N [resp. j, j ∈ {0, . . . , i}], j j implies R j (w) ⊆ R j (w).

Condition (LA) is the local agreement condition and more generally we say that the relations R and R on W are in local agreement

def ⇔ for every w ∈ W , either R(w) ⊆ R (w) or R (w) ⊆ R(w).
A modal formula is said to be L-satisfiable def ⇔ there exist a model M based on some frame from S and x ∈ W such that M, x |= φ. A formula φ is said to be L-valid def ⇔ for every frame F ∈ S, we have F |= φ.

Example 2.1. The standard modal logic S5 is a bounded LA-logic as well as the bimodal logic with two S5 modal connectives [1] and [2] such that [2]p ⇒ [1]p is valid (semantically equivalent to R 1 ⊆ R 2 in the models). Similarly, the logics with a countably infinite set of modal connectives characterized by the frames W, (R i ) i∈N such that for every i ∈ N, R i is an equivalence relation and

R 0 ⊆ R 1 ⊆ R 2 ⊆ R 3 ⊆ . . . is an unbounded LA-logic.
The LA-logics satisfy the finite model property as stated below.

Theorem 2.1. (Dem98, Proposition 4.5) Let L be an LA-logic either bounded or unbounded.

(I) A formula φ is L-satisfiable iff φ is satisfied in an L-model of cardinality less than 1 + n × |φ| n where n is the cardinality of N(φ). (II) Every bounded LA-logic has an NP-complete satisfiability problem. Theorem 2.1(I) is proved by using an extension of the construction done for S5 in [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. In (Dem98), it is not shown whether the exponential size of the models is unavoidable in the worst case. Remember that n depends on |φ| and n < |φ|. The rest of the paper is dedicated to show that this exponential size of the models is inescapable and that nevertheless many unbounded LA-logics admit a PSPACE satisfiability problem.

Nice unbounded LA-logics

The class of linear orders on N is uncountable and therefore one can expect that there exist undecidable unbounded LA-logics. In this section, we introduce a class of unbounded LA-logics that shall be shown to be decidable in polynomial space. An unbounded LA-logic is said to be nice def ⇔ (NICE1) there is a map f : N → N * in logarithmic space such that for every

n ≥ 1, f (n) is a string of n + 1 elements, say f (n) = i 1 • . . . • i n+1 , for which there is ∈ lo(L) verifying i 1 i 2 . . . i n+1 . (NICE2) for every non-empty string i 1 • . . . • i n of natural numbers (encoded
in binary writing), deciding whether there is some ∈ lo(L) such that i 1 . . . i n can be done in polynomial space in the size of Σ n j=1 log(i j ). If such a linear order exists for i

1 •. . .•i n , then we say that i 1 •. . .•i n is L-extendable. (NICE3) for every non-empty string i 1 • . . . • i n , n ≥ 1, for all equivalence relations R i 1 , . . . ,
, . . . , i n } such that R σ(1) (w) ⊆ . . . ⊆ R σ(n) (w) and σ(1) • . . . • σ(n) is L-extendable, there is an L-frame W, (R k ) k∈N such that for every j ∈ {1, . . . , n}, R i j = R i j .
Condition (NICE1) almost states that there is a simple distinguished element in lo(L) except that in (NICE1) the linear ordering depends on n. Simplicity is reflected by the requirement that f is in logarithmic space. For instance, if the usual ordering ≤ on natural numbers is in lo(L), then f (n) can take the value 0

• 1 • . . . • (n -1) • n.
In the sequel, without any loss of generality, we can assume that ≤∈ lo(L) so that f (n

) = 0 • 1 • . . . • (n -1) • n. Condition (NICE1)
is mainly used to show that every nice unbounded LA-logic has a PSPACEhard satisfiability problem (see the proof of Lemma 3.1). Condition (NICE2) states that from a finite string one can decide in polynomial space whereas this chain can be extended as an infinite one viewed as a linear ordering from lo(L) (see the proof of Theorem 4.6). This condition has to do with the fact that we want to define a class of logics in PSPACE. Condition (NICE3) guarantees that every finite structure satisfying certain local conditions can be extended as an L-model (see the proof of Lemma 4.7).

Below we give examples of nice unbounded LA-logics.

DALLA is the nice unbounded LA-logic such that lo(DALLA ) is the set of all the linear orders on N (Dem98) (see Section 5 for understanding the relationship between DALLA and Gargov's logic DALLA (Gar86)).

LGM is the nice unbounded LA-logic such that lo(LGM ) is the singleton set {≥} (Dem98) (see also [START_REF] Nakamura | On a logic based on graded modalities[END_REF]). The map f can be defined as

f (n) = n • (n -1) • . . . • 1 • 0. LGM k : for every k ≥ 0, let LGM k [resp. LGM k ] be the nice unbounded LA-logic such that lo(LGM k ) is the class of linear orders such that restricted to {k + 1, k + 2, . . .} is ≥ [resp. ≤] restricted to {k + 1, k + 2, . . .} and for every i ∈ {0, . . . , k}, k + 1 i [resp. i k + 1]. Obviously, LGM is
LGM 0 and card(lo(LGM k )) = (k + 1)! for every k ≥ 0.

A few properties

For the modal logic S5 it is known that every modal formula φ is equivalent to a formula φ of modal depth at most one. φ can be effectively built from φ (see e.g. ( HC68)). Lemma 2.2 below generalizes this result to LGM , providing an analogy between the modal depth and the number of distinct modal connectives.

Lemma 2.2. Every LGM -formula φ has an LGM -equivalent formula ψ such that if

[i]ϕ 1 occurs in the scope of [i ]ϕ 2 in ψ, then i > i .
The proof in the appendix is based on results for the modal logic S5 (HC68) and on results for modal logics augmented with a universal modal connective (GP92). This allows us to view the number of distinct modal connectives in local agreement as a modal depth.

Corollary 2.3. Every LGM -formula φ has an LGM -equivalent formula, say ψ, such that the modal depth of ψ is equal the number of different modal indices occurring in φ.

Each class of linear orders over N determines a unique unbounded LA-logic. Since the class of linear orders on N is uncountable, there exist unbounded LA-logics that are undecidable. However, the conditions (NICE1)-(NICE3) guarantee decidability.

Theorem 2.4. For every nice unbounded LA-logic L, the L-satisfiability problem is decidable.

Proof: Let φ be a formula for which we want to know whether φ is Lsatisfiable. By Theorem 2.1, φ is L-satisfiable iff φ is satisfied in an L-model of cardinality less than 1 + n × |φ| n where n is the cardinality of N(φ). In order to check whether φ is L-satisfiable, enumerate all the structures M = W, (R i ) i∈N(φ) , V (modulo the isomorphic copies) such that card(W ) ≤ 1 + n × |φ| n , the R i s are binary relations on W and V is a valuation restricted to the propositional variables occurring in φ. Check the following properties:

(i) Is M, w |= φ for some w ∈ W ? This model-checking instance can be done in time O(card(W ) 2 × |φ|). (ii) Is it the case that for all i ∈ N(φ), the R i 's are equivalence relations and they are in local agreement? This can be checked in polynomial time in card(W ) + |φ|.

(iii) Is it the case that for every w ∈ W , there is ∈ lo(L) such that for all i, j ∈ N(φ), i j implies R i (w) ⊆ R j (w)? By satisfaction of the condition (NICE2), this is a decidable question.

By satisfaction of the condition (NICE3), one can easily show that φ is Lsatisfiable iff there is some structure W, (R i ) i∈N(φ) , V satisfying the above conditions (i)-(iii). Q.E.D.

The rest of the paper is mainly dedicated to show that one can refine this decidability result to obtain PSPACE-completeness of the satisfiability problem of any nice unbounded LA-logic.

3 Tree-like models and the PSPACE lower bound

In the rest of this section, L is a nice unbounded LA-logic such that ≤∈ lo(L). Lemma 3.1 below states that there exist L-satisfiable formulae with exponential size models. Such an exponential bound can be obtained for the standard modal logics K, T and S4 (see e.g. ( HM92)) but not for the bounded LA-logics (Dem98).

Lemma 3.1. There is a family (ψ n ) n≥1 of formulae such that for every n ≥ 1,

|ψ n | is in O(n),
ψ n is L-satisfiable and every L-model for ψ n has cardinality at least 2 n .

Proof: We define recursively the formulae renam j and tree j for every j ≥ 1.

• renam

1 def = ; • tree 1 def = 1 [0]p 1 ∧ 1 [0]¬p 1 ; • renam j+1 def = [j + 1]renam j ∧ [j + 1](tree j ⇔ r j ); • tree j+1 def = j + 1 (([j]p j+1 ) ∧ r j ) ∧ j + 1 (([j]¬p j+1 ) ∧ r j ).
The propositional variable r j is a renaming variable for the formula tree j . We define ψ n as the conjunction renam n ∧ tree n . By induction on n, one can

show that if M, w 0 |= ψ n for some L-model M, then card(R n (w 0 )) ≥ 2 n and {R j (w 0 ) : 1 ≤ j ≤ n -1} ⊆ R n (w 0 ). So, an alternative definition for ψ n , n ≥ 2, is ψ n def = n-1 j=1 [n](tree j ⇔ r j ) ∧ tree n .
This is due to the fact that {R j (w 0 ) :

1 ≤ j ≤ n -1} ⊆ R n (w 0 ) implies M, w 0 |= [n][n 1 ] . . . [n k ]ψ ⇔ [n]ψ for every formula ψ and for every finite sequence n 1 • . . . • n k ∈ {1, . . . n} * .
The formula ψ n can be defined in a way that makes clear its logarithmic space construction in n. Indeed, the formula tree j is not defined inductively. For every n ≥ 2, let ψ n be defined as follows:

ψ n def = n-1 j=1 [n]( tree j ( j ([j -1]p j ∧ r j-1 ) ∧ j ([j -1]¬p j ∧ r j-1 )) ⇔ r j )∧ treen n ([n -1]p n ∧ r n-1 ) ∧ n ([n -1]¬p n ∧ r n-1 )
In Figure 1, we present a skeleton of an L-model for ψ 2 . The family (R i ) i∈N defined in Figure 1 is the smallest family of equivalence relations containing the pairs of worlds from the skeleton such that R 0 ⊂ R 1 ⊂ R 2 and for every j > 2, R j = R 2 . Obviously R 0 is the identity relation.

tree 2 ∧ renam 2 [1]p 2 , p 2 , r 1 , tree 1 [1]¬p 2 , ¬p 2 , r 1 , tree 1 [0]p 1 , p 1 , p 2 [0]¬p 1 , ¬p 1 , p 2 [0]p 1 , p 1 , ¬p 2 [0]¬p 1 , ¬p 1 , ¬p 2 2 2 1 1 1 1 Fig. 1. L-model skeleton for ψ 2 Q.E.D.
As shown in the proof of Lemma 3.1, the L-models for the formula ψ n have a tree-like structure and this shall be exploited for reducing QBF into Lsatisfiability. If the usual ordering ≤ is not in lo(L), then in the proof of Lemma 3.1, for every j ∈ {0, . . . , n}, we replace [j] by [j ] where j is the j + 1th element of f (n) and f is the map from the condition (NICE1). We invite the reader to check that ψ n can be built in logarithmic space in n because the composition of logarithmic space reductions is still a logarithmic space reduction (see e.g. (Pap94, Proposition 8.3)). Hence, Lemma 3.1 entails that the exponential size of models in Theorem 2.1(I) is unavoidable.

Given a Quantified Boolean formula φ = Q n p n Q n-1 p n-1 . . . Q 1 p 1 φ
where φ is a propositional formula built over {p 1 , . . . , p n } (without modal connectives), and {Q 1 , . . . , Q n } ⊆ {∃, ∀}, deciding whether φ is true is PSPACEcomplete (Sto77).

Lemma 3.2. There is a logarithmic space many-one reduction from QBF into L-satisfiability.

Proof: Let φ = Q n p n Q n-1 p n-1 . . . Q 1 p 1 φ
be a quantified Boolean formula in prenex form. Let us define an L-formula ψ such that φ is true iff ψ is Lsatisfiable by taking advantage of the construction of Lemma 3.1. For every j ≥ 1, we use the following abbreviation: l j def = ¬d 1 ∧ . . . ∧ ¬d j-1 ∧ d j ("level j"). The propositional variable d j stands for "depth j". For instance l 1 = d 1 . We define recursively the formulae renam j , tree j , quanti j for every j ≥ 1.

• renam 1 def = ; • tree 1 def = 1 ([0]p 1 ∧ l 1 ) ∧ 1 ([0]¬p 1 ∧ l 1 ) ∧ [1](l 1 ⇒ ([0]p 1 ∨ [0]¬p 1 )); • quanti 1 def = [1](l 1 ⇒ φ ) if Q 1 = ∀, otherwise quanti 1 def = 1 (l 1 ∧ φ ); • renam j+1 def = [j + 1]renam j ∧ [j + 1](tree j ⇔ r j ); • tree j+1 def = j +1 (([j]p j+1 ∧l j+1 )) ∧ j +1 (([j]¬p j+1 ∧l j+1 )) ∧[j +1](l j+1 ⇒ (([j]p j+1 ∨ [j]¬p j+1 ) ∧ r j )); • quanti j+1 def = [j + 1](l j+1 ⇒ quanti j ) if Q j+1 = ∀, otherwise quanti j+1 def = j + 1 (l j+1 ∧ quanti j ).
Finally, ψ def = quanti n ∧ renam n ∧ tree n . One can check that this many-one reduction is in logarithmic space. This is simpler to observe than in the proof of Lemma 3.1: to define formulae at stage j + 1, one needs at most one copy of each formula of the stage j. The main differences with the formulae introduced in the proof of Lemma 3.1 are the following.

(1) Propositional variables for depths are introduced. As usual, they allow to distinguish the different quantification depths in the tree-like structure.

(2) In the definition of the formulae (tree j ) 1≤j≤n , one cannot express that internal nodes have exactly two children. Instead, as usual, we can enforce that at most two children of internal nodes behave differently as far as the modal language is concerned. (3) Once the tree structure is encoded by the satisfaction of the formula renam n ∧ tree n , the formulae (quanti j ) 1≤j≤n allow to quantify over the leaves of the tree, mimicking the quantifications in the QBF formula φ.

Let us show that φ is true iff ψ is L-satisfiable.

Assume that φ is true. Then, ψ is satisfied in the L-model M = W, (R i ) i∈N , V defined as follows:

• W def = {u ∈ {0, 1} * : |u| ≤ n};
• for every j ∈ {0, . . . , n}, we define the auxiliary relation R j as follows:

u, v ∈ R j def ⇔ v = u • i for some i ∈ {0, 1} and |u| + j = n; • for every j ∈ {0, . . . , n}, R j def = ( 0≤k≤j (R k ∪ R -1 k )) * ; • for every j > n, R j def = R n ; • for every 1 ≤ j ≤ n, • V (d j ) def = {u ∈ W : |u| = n + 1 -j}; • V (p j ) def = {u ∈ W : |u| ≥ n + 1 -j, (n + 1 -j)th bit of u is 1}; • V (r j ) def = {u ∈ W : |u| = n -j} if j ≤ n -1. M is an L-model since R 0 ⊆ R 1 ⊆ R 2 ⊆ R 3 ⊆ . . .

and ≤∈ lo(L).

For every j ∈ {0, . . . , n}, for every u ∈ W such that |u| = j, we can show that M, u |= tree n-j ∧ renam n-j . Hence, M, |= tree n ∧ renam n , where is the empty string.

A valuation over the propositional variables {p 1 , . . . , p n } can be represented by a string u of length n in {0, 1} * such that p i is true iff the ith bit of u is 1. Here the ordering of bits is from the right to the left. It is a standard characterization of QBF that the QBF formula φ is true iff there is a nonempty set X of valuations over {p 1 , . . . , p n } such that:

(QBF1) for every string u ∈ X, u satisfies φ in the propositional sense; (QBF2) for every string u ∈ X, for every r such that Q r = ∀, there is u ∈ X such that the rth bit of u is different from the rth bit of u and for all r < r ≤ n, the r th bit of u is equal to the r th bit of u.

One can show that {u ∈ W : |u| = n, M, u |= φ } is such a set and therefore M, |= quanti n . Consequently, M, |= ψ.

Conversely, one can show that if M, w |= ψ n for some L-model M, then one can easily extract from M a set X of valuations over {p 1 , . . . , p n } satisfying the above conditions (QBF1) and (QBF2). Q.E.D.

If the usual ordering ≤ is not in lo(L), one can easily adapt the proof in Lemma 3.2 to get a logarithmic space many-one reduction as done for the proof of Lemma 3.1.

Other translations from QBF into modal and temporal logics can be found in the papers (Lad77; SSS91; HM92; DS01). As usual, our reduction in the proof of Lemma 3.2 builds a tree-like models in which the leaves encode propositional valuations and the quantification in QBF are encoded by modal connectives in L. The peculiarity of our reduction is in the fact that each quantifier in the QBF formula corresponds to a modal operator with different index, depending on the depth of this quantifier. This allows us to enforce the local linear orders.

PSPACE complexity upper bound

In this section, we show that every nice unbounded LA-logic has a satisfiability problem in PSPACE using a sophisticated Ladner-like algorithm (Lad77).

• In Section 4.1 we present preliminary definitions and results. Since the al-gorithm explores the branches of the tree-like potential L-models, we need to fix what are the nodes of the trees (sets of formulae) and how they are related to each other. • In Section 4.2, we present the definition of the main algorithm.

• In Section 4.3, we show that the main algorithm terminates by emphasizing what is the measure that strictly decreases depending on the history of the recursive calls. • In Section 4.4, we finally show that the algorithm solves the L-satisfiability problem.

Preliminary results

In Definition 4.1 below, we introduce a closure operator for sets of modal formulae as it is done for Propositional Dynamic Logic in (FL79).

Definition 4.1. Let X be a set of formulae. cl(X) is the smallest set of formulae such that:

• X ⊆ cl(X); • cl(X) is closed under subformulae; • if [i]φ, [j]φ ∈ cl(X), then [i]φ ∈ cl(X).

∇

A set X of formulae is said to be closed def ⇔ cl(X) = X. Observe that for every finite set X of formulae, md(cl(X)) = md(X) and card(cl({φ})) ≤ card(N(φ)) × card(sub(φ)) < |φ| 2 . Indeed, one can consider that each subformula of φ generates at most N(φ) formulae in cl({φ}). This is a crucial property since in order to establish the PSPACE upper bound, card(cl({φ})) is bounded by a polynomial in |φ|.

The forthcoming algorithm defined in Section 4.2 explores branches of a tree and for each node one can abstract its path from the root by a finite word in N * . For each path, we define the admitted formulae that have to be taken into account for the nodes reachable from the root with such a path. Definition 4.2 states how such sets of formulae are defined. Definition 4.2. Let φ be a formula. For every u ∈ N * , cl(u, φ) is the smallest set such that:

(1) cl( , φ) = cl({φ});

(2) for every v, cl(v, φ) is closed;

(3) for every v, for every

i ∈ N, if [i]ψ ∈ cl(v, φ), then [i]ψ ∈ cl(v • i, φ).
function LA-WORLD(Σ, u, σ, index, Z, φ) (Consistency) if last(Σ) is not u, σ -consistent, then return false;

(last(Σ) denotes the last element of the sequence Σ) (Witnesses) for every [i]ψ ∈ cl(u, φ) \ last(Σ) with i ∈ Z do if one of the two conditions below holds,

(NewIndex) index = σ -1 (i); (NoExistingWitness) there is no X ∈ Σ such that (i) Σ = Σ 1 XΣ 2 and u = u • i |Σ 2 | for some sequences Σ 1 , Σ 2 such that Σ 2 is non-empty; (ii) ψ ∈ X; (iii) last(Σ) ≈ σ(j) X for every j ∈ {index, . . . , card(N(φ))}; then (SearchWitness) for every X ψ ⊆ cl(u•i, φ)\{ψ}, for every bijection σ : {1, . . . , card(N(φ))} → N(φ) such that (iv) σ (j) = σ(j) for every j ∈ {σ -1 (i), . . . , card(N(φ))}; (v) last(Σ) ≈ σ (j) X ψ for every j ∈ {σ -1 (i), . . . , card(N(φ))}; (vi) σ (1), . . . , σ (card(N(φ))) is L-extendable; call LA-WORLD(Σ • X ψ , u • i, σ , σ -1 (i), Z i σ , φ) with Z i σ def = {σ (j) : j ∈ {1, . . . , σ -1 (i)}}.
(NoWitnessFound) If all these calls return false, then return false; (AllWitnessesFound) Return true. For every L-model M = W, (R i ) i∈N , V , for every u ∈ N * , for every formula φ such that N(φ) = ∅, for all w, w ∈ W , for every bijection σ : {1, . . . , card(N(φ))} → N(φ) such that R σ(j-1) (w) ⊆ R σ(j) (w) for every j ∈ {2, . . . , card(N(φ))}, for every k ∈ N(φ), the following conditions are satisfied:

(I) X w,u def = {ψ ∈ cl(u, φ) : M, w |= ψ} is u, σ -consistent; (II) if w, w ∈ R k , then X w,u ≈ σ(j) X w ,u•k for every j ∈ {σ -1 (k), . . . , n}.
The proof of the above lemma is by an easy verification using that cl(u, φ) is closed. Lemma 4.2(II) is a counterpart of (Dem98, Proposition 4.2(2)).

The algorithm

In Figure 2, the function LA-WORLD(Σ, u, σ, index, Z, φ) returning a Boolean value is defined.

The arguments of LA-WORLD are of the following form:

• Σ is a finite non-empty sequence of subsets of cl({φ});

• u ∈ N(φ) * ; • σ is a 1-1 mapping {1, . . . , card(N(φ))} → N(φ); • index ∈ {1, . . . , card(N(φ))}; • Z ⊆ N(φ).
LA-WORLD is defined on the model of the function K-WORLD in (Lad77) (see also (Spa93b; DLNN97; Dem00; Mas00)). Σ and u are historical information about the parent calls to LA-WORLD. For this reason, we shall have |Σ| = |u| + 1. We shall establish that if LA-WORLD(Σ, u, σ, index, Z, φ) returns true, then there is an L-model M = W, (R i ) i∈N , V and w ∈ W such that (Prop1) for every ψ ∈ last(Σ), we have M, w |= ψ;

(Prop2) R σ(1) (w) ⊆ . . . ⊆ R σ(n) (w).
The inputs Σ, index and Z guarantee termination of the algorithm. For instance, no recursive call is performed when the argument Z is empty. Similarly, every sequence of more than |φ| 2 +1 successive recursive calls strictly decreases the cardinality of the argument Z (see Section 4.3 for details).

In Figure 2, the condition (Consistency) is just a consistency check whereas the condition (Witnesses) is the part searching for witnesses for negations of formulae of the form [i]ψ. If a new witness is really needed (by satisfaction of either the condition (NewIndex) or the condition (NoExistingWitness)), then one tests potential new witnesses by checking local conditions ((iv), (v), and (v)) and global one via the recursive call. The arguments need to be appropriately updated in such a call in order to guarantee termination. As other tableaux-like procedures, LA-WORLD(Σ, u, σ, index, Z, φ) tries to build a quasi L-model for last(Σ) having a tree-like structure. Then, proving the correctness of our algorithm partly consists in showing that from this quasi L-model, it is possible to complete it providing a standard L-model satisfying the conditions (Prop1) and (Prop2). More technical details are provided in the sequel.

We say that LA-WORLD(Σ, u, σ, index, Z, φ) directly calls LA-WORLD(Σ , u , σ , index , Z , φ) def ⇔ LA-WORLD(Σ , u , σ , index , Z, φ) is called at depth one in the computation tree of LA-WORLD calls from the execution of LA-WORLD(Σ, u, σ, index, Z, φ). If the call is at some depth (not necessarily one) in the computation tree of LA-WORLD calls from the execution of LA-WORLD(Σ, u, σ, index, Z, φ), we simply say that LA-WORLD(Σ , u , σ , index , Z , φ) is called in LA-WORLD(Σ, u, σ, index, Z, φ).

Given an L-formula φ such that N(φ) is empty, it is easy to show that φ is L-satisfiable iff there is Y ⊆ cl({φ}) such that LA-WORLD(Y, , σ, 0, ∅, φ) returns true. In the sequel, we treat the case N(φ) = ∅.

Polynomially bounded recursion depth and space

In this section, we shall show that termination of LA-WORLD is guaranteed for calls of the form LA-WORLD(Y, , σ, n, N(φ), φ) where (1) φ is an L-formula, Y ⊆ cl({φ}) and n = card(N(φ));

(2) σ : {1, . . . , card(N(φ))} → N(φ) is a bijection.

For every call LA-WORLD(Σ, u, σ, index, Z, φ) in LA-WORLD(Y, , σ, n, N(φ), φ) the following invariant conditions can be easily checked:

(INV1) last(Σ) ⊆ cl(u, φ); (INV2) Z index σ = Z (see the definition of Z index σ from the point (vi) of Fig- ure 2); (INV3) last(u) = σ(index); (INV4) σ -1 (i) > index for every i ∈ N(φ) \ Z.
Clearly, the number of arguments in LA-WORLD can be reduced but minimality is not our main purpose here.

Lemma 4.3. If LA-WORLD(Σ, u, σ, index, Z, φ) is called in LA-WORLD(Y, , σ, n, N(φ), φ), then there is no substring of the form i |φ| 2 +1 for some i ∈ N(φ) occurring in u.
The proof of Lemma 4.3 can be found in the appendix. It can be viewed as a refined variant of the proof showing that the modal logic S5 has the linear size model property [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. A corollary of Lemma 4.3 is that there is no sequence of successive calls of length greater than |φ| 2 such that the value of the argument index does not change. Lemma 4.4 below states that when the value of the argument index changes, the number of elements of the argument Z strictly decreases. This is particularly interesting since whenever the argument Z is empty no recursive call LA-WORLD is possible.

Lemma 4.4. Let LA-WORLD(Σ, u, σ, index, Z, φ) and LA-WORLD(Σ , u , σ , index , Z , φ) be calls in LA-WORLD(Y, , σ, n, N(φ), φ) such that LA-WORLD(Σ, u, σ, index, Z, φ) directly calls LA-WORLD(Σ , u , σ , index , Z , φ). If index = index , then Z ⊂ Z (proper inclusion).
Proof: The proof is by an easy verification using the condition (INV2), the condition (iv) in Figure 2 and the fact that only bijections of the form {1, . . . , n} → N(φ) with n = card(N(φ)) are involved in the algorithm defined in Figure 2. Q.E.D.

Consequently, we obtain the following result. Lemma 4.5. Let LA-WORLD(Σ, u, σ, index, Z, φ) be a call in LA-WORLD(Y, , σ, n, N(φ), φ). Then, |u| = |Σ| -1 ≤ |φ| 3 . Since the logic L satisfies the condition (NICE2), the condition (vi) in Figure 2 can be checked in polynomial space in |φ|. For DALLA , this can be done in constant space and for LGM in linear space. Consequently, since the depth of the recursion is polynomial in |φ| from LA-WORLD(Y, , σ, n, N(φ), φ) and since at each level of the recursion, we need only polynomial space in |φ|, we can deduce the following result.

Theorem 4.6. For every L-formula φ, for every Y ⊆ cl({φ}), for every bijection σ : {1, . . . , card(N(φ))} → N(φ), LA-WORLD(Y, , σ, card(N(φ)), N(φ), φ) terminates and requires polynomial space in φ.

The subsets of cl({φ}) can be implemented as bit-strings of polynomial length in |φ| and the sequences Σ and u can be implemented as global stacks. Refinements are possible but they are omitted here since they do not essentially decrease the space bounds. For instance, it is easy to design a variant of LA-WORLD from Figure 2 for which |Σ| ≤ |φ| 2 in the conditions of Lemma 4.5. Indeed, we need to recall the history of the recursive calls (we assume that past is linear and finite) only when the argument index does not change.

Correctness

Lemmas 4.7 and 4.8 below state that not only LA-WORLD terminates but also it solves the L-satisfiability problem.

Lemma 4.7. Let φ be an L-formula such that card(N(φ)) = n ≥ 1, Y ⊆ cl({φ}), and σ be a bijection {1, . . . , n} → N(φ) such that φ ∈ Y . If LA-WORLD(Y, , σ, n, N(φ), φ) returns true, then φ is L-satisfiable.

Proof: Assume that LA-WORLD(Y, , σ, n, N(φ), φ) returns true. Let us build an L-model M = W, (R i ) i∈N , V such that for some w ∈ W for every ψ ∈ cl({φ}), we have M, w |= ψ iff ψ ∈ Y .

We define W as the set of quintuples Σ, u, σ, index, Z such that there is a finite sequence

Σ 1 , u 1 , σ 1 , index 1 , Z 1 , . . . , Σ k , u k , σ k , index k , Z k , k ≥ 1, such that (1) Σ 1 , u 1 , σ 1 , index 1 , Z 1 = Y, , σ, n, N(φ) ; (2) Σ k , u k , σ k , index k , Z k = Σ, u, σ, index, Z ;
(3) for every i ∈ {1, . . . , k}, LA-WORLD(Σ i , u i , σ i , index i , Z i ) returns true; (4) for every i ∈ {1, . . . , k -1}, LA-WORLD(Σ i , u i , σ i , index i , Z i , φ) directly calls LA-WORLD(Σ i+1 , u i+1 , σ i+1 , index i+1 , Z i+1 , φ).

By assumption, Y, , σ, n, N(φ) ∈ W and Σ, u, σ, index, Z ∈ W implies that last(Σ) is u, σ -consistent. In order to define (R i ) i∈N , we introduce the auxiliary families of relations (S i ) i∈N and (T i ) i∈N . Whereas each relation S i can be viewed as a "single step relation", T i is its extension by considering the local inclusions with the permutations. For every i ∈ N(φ), let us define S i on W as follows: Σ, u, σ, index, Z S i Σ , u , σ , index , Z def ⇔ (1) LA-WORLD(Σ, u, σ, index, Z, φ) calls directly LA-WORLD(Σ , u , σ , index , Z , φ) and (2) u = u • i. For every i ∈ N(φ), we define the auxiliary relation T i as follows:

T i def = { w, w ∈ W 2 : w, w ∈ S j , j ∈ N(φ) such that σ -1 (j) ≤ σ -1 (i)}.
In the definition of T i , the map σ -1 is from w = . . . , σ, . . . . The definition of M can be now completed.

• For every i ∈ N(φ), R i def = (T i ∪ T -1
i ) * (reflexive, symmetric, and transitive closure of T i ).

• By construction of the family (R i ) i∈N(φ) , one can show that for every w = Σ, u, σ, index, Z ∈ W , R σ(1) (w) ⊆ . . . ⊆ R σ(n) (w). Moreover every relation in (R i ) i∈N(φ) is an equivalence relation. Hence, by the condition (NICE3), it is possible to define the relations R i with i ranging over N \ N(φ), such that the resulting structure W, (R i ) i∈N is an L-frame. • For every p ∈ PRP, V (p)

def = { Σ, u, σ, index, Z ∈ W : p ∈ last(Σ)}.
Hence, M is an L-model. One can show that for every i ∈ N(φ),

• S i ⊆ T i and S * i ⊆ T * i ⊆ R i ; • Σ, u, σ, index, Z , Σ , u , σ , index , Z ∈ R i implies last(Σ) ≈ i last(Σ )
(≈ i is an equivalence relation on Refl).

By induction on the structure on ψ, we shall show that for every quintuple w = Σ, u, σ, index, Z in W , for every ψ ∈ cl(u, φ), ψ ∈ last(Σ) iff M, w |= ψ.

The case when ψ is a propositional variable, say p, holds by the definition of V (p). Induction hypothesis: for every ψ ∈ cl({φ}) such that |ψ| ≤ n, for every

w = Σ, u, σ, index, Z ∈ W , if ψ ∈ cl(u, φ), then ψ ∈ last(Σ) iff M, w |= ψ.
Let ψ be a formula in cl({φ}) such that |ψ| ≤ n + 1. The cases when the outermost connective of ψ is Boolean are consequences of the u, σ -consistency of last(Σ) and the induction hypothesis. Let us treat the other case. Let ψ = [i]ψ ∈ cl({φ}) and w = Σ, u, σ, index, Z be an element of W such that ψ ∈ cl(u, φ).

Assume that [i]ψ ∈ last(Σ). Since, for every w = Σ , u , σ , index , Z ∈ R i (w), we have last(Σ) ≈ i last(Σ ), we can conclude that ψ ∈ last(Σ ). By the induction hypothesis, for every w ∈ R i (w), M, w |= ψ . Consequently, M, w |= [i]ψ .

Now assume that [i]ψ ∈ last(Σ).

Case 1: ψ = [i]ψ for some i ∈ Z. Case 1.1: σ -1 (i) = index and there is X in Σ satisfying the conditions (i)-(iii) in Figure 2. We use notations from Figure 2 and this case corresponds to the situation when the conditions (NewIndex) and (NoExistingWitness) from Figure 2 do not hold. By definition of the set W , LA-WORLD(Σ 1 • X, u , σ , index , Z , φ) returns true for some u , σ , index and Z . By definition of the binary relation S i , w , w ∈ S * i and w, w ∈ R i with w taking the value Σ 1 • X, u , σ , index , Z . By the induction hypothesis, M, w |= ψ and therefore M, w |= [i]ψ . Case 1.2: the condition for the Case 1.1 does not hold. Since w ∈ W , LA-WORLD(Σ, u, σ, index, Z, φ) returns true and therefore there exist X ψ ⊆ cl(u • i, φ) \ {ψ } and a bijection σ : {1, . . . , card(N(φ))} → N(φ) such that the conditions (iv)-(vi) from Figure 2 hold true and LA-WORLD(Σ

• X ψ , u • i, σ , σ -1 (i), Z i σ , φ) returns true. By definition of S i , w, Σ • X ψ , u • i, σ , σ -1 (i), Z i σ ∈ S i ⊆ R i . By the induction hypothesis, M, Σ • X ψ , u • i, σ , σ -1 (i), Z i σ |= ψ and therefore M, w |= [i]ψ . Case 2: ψ = [i]ψ and i ∈ Z.
One can show that there is a finite sequence

Σ 1 , u 1 , σ 1 , index 1 , Z 1 , . . . , Σ j , u j , σ j , index j , Z j , j ≥ 2, in W such that (1) Σ j , u j , σ j , index j , Z j = Σ, u, σ, index, Z ; (2) for every k ∈ {1, . . . , j -1}, LA-WORLD(Σ k , u k , σ k , index k , Z k , φ) directly calls LA-WORLD(Σ k+1 , u k+1 , σ k+1 , index k+1 , Z k+1 , φ); (3) [i]ψ ∈ cl(s, φ) \ last(Σ 1 ), i ∈ Z 1 and i ∈ Z 2 ∪ . . . ∪ Z j ; (4) there is w = Σ , u , σ , index , Z ∈ W such that Σ 1 , u 1 , σ 1 , index 1 , Z 1 , Σ , u , σ , index , Z ∈ S * i and ψ ∈ last(Σ ).
Since the condition (INV4) is satisfied, one can show that for every k ∈ {1, . . . , j-1}, Σ k , u k , σ k , index k , Z k T i Σ k+1 , u k+1 , σ k+1 , index k+1 , Z k+1 . For every k ∈ {1, . . . , j -1}, we have

Σ k , u k , σ k , index k , Z k (S i ∪ T i ) * Σ k+1 , u k+1 , σ k+1 , index k+1 , Z k+1 .
Therefore, w, w ∈ R i . By the induction hypothesis, we get M, w |= ψ . Hence, M, w |= ψ. This part of the proof can be viewed as an algorithmic explanation for the most interesting case in the proof of (Dem98, Proposition 4.4). Q.E.D.

The model M built in the proof of Lemma 4.7 is finite and it has a tree structure obtained from the tree of successful recursive calls to LA-WORLD.

Combined with Lemma 4.8 below this provides a tree model property for L.

This is a property known to be essential for decidability of modal logics (see e.g. ( Grä99)).

Lemma 4.8. For every L-satisfiable formula φ such that card(N(φ)) = n ≥ 1, there exist Y ⊆ cl({φ}) and a bijection σ : {1, . . . , n} → N(φ) such that φ ∈ Y and LA-WORLD(Y, , σ, n, N(φ), φ) returns true.

The proof of Lemma 4.8 can be found in the appendix. From Lemmas 3.2, 4.7, 4.8 and Theorem 4.6, we can conclude the main result of the paper.

Theorem 4.9. Every nice unbounded LA-logic has a PSPACE-complete satisfiability problem.

Corollary 4.10. DALLA -satisfiability and LGM -satisfiability are PSPACE-complete.

Applications to information and fuzzy modal logics

In this section, we just explain how the PSPACE-completeness for DALLA and LGM can be lifted to DALLA (Gar86) and LGM (Nak93), respectively.

DALLA

The logic DALLA defined in (Gar86) is a polymodal logic with a countably infinite set of modal connectives of the form Obviously, every propositional variable p i new behaves as a renaming variable similarly to every propositional variable r j in the proof of Lemma 3.1. Observe also that for every formula ψ built on the modal constants {c 1 , . . . c l }, the formula [c 1 ]ψ ∧ . . . ∧ [c l ]ψ behaves as the formula ψ prefixed by a universal modal connective. f (φ) can be computed in polynomial-time in |φ| and φ is DALLAsatisfiable iff f (φ) is DALLA-satisfiable. Hence φ is DALLA-satisfiable iff f |φ| (φ) is DALLA-satisfiable. f |φ| (φ) can be computed in polynomial-time in |φ| and it is a DALLA -formula by identifying [c i ] and [i]. Q.E.D.

Hence, an important consequence of Theorem 4.9 is the following result.

Theorem 5.2. DALLA-satisfiability is PSPACE-complete.

As a corollary, the logic S5 S L3 introduced in (BO99) has a PSPACE-complete satisfiability problem, since DALLA and S5 S L3 can be viewed as syntactic variants.

LGM

The logic of graded modalities LGM introduced in (Nak93) is based on the graded equivalence relations, i.e., the graded similarity in Zadeh's meaning. Here, by LGM we mean the restriction of LGM defined in [START_REF] Nakamura | On a logic based on graded modalities[END_REF] where only rational numbers4 can occur in modal connectives. Following (Dem98, Section 5.2), one can show that LGM-satisfiability and LGM -satisfiability are of the same computational complexity. Consequently, Theorem 5.3. LGM-satisfiability is PSPACE-complete.

Concluding remarks

In the paper we have introduced a class of nice unbounded LA-logics and we have shown that every nice unbounded LA-logic has a PSPACE-complete satisfiability problem whereas for bounded LA-logics, the problem is "only" NP-complete. The large class of nice unbounded LA-logics includes DALLA and LGM and consequently we were able to show that the logics LGM and DALLA are PSPACE-complete (see Section 5). The best known complexity bounds for DALLA were NP-hardness and NEXPTIME-easiness. A byproduct of our technical developments is the observation that for LA-logics, bounding the number of distinct modal connectives is similar to the effect of bounding the modal depth for the standard modal logic K (see e.g. ( Hal95)). We conjecture that Corollary 2.3 can be extended to other unbounded LAlogics.

An interesting open problem is the decidability (and computational complexity if meaningful) of the satisfiability problem for the Data Analysis Logic DAL defined in [START_REF] Del Cerro | DAL -A logic for data analysis[END_REF]. DAL has the same language as DALLA and the DAL models are the structures satisfying the conditions (equiv) and (∩+∪ * ). What is known so far is that DAL satisfiability is EXPTIME-hard by (Hem96, Theorem 5.1) and therefore it is highly probable that DAL behaves differently from DALLA as far as complexity issues are concerned. The largest fragment of DAL we are aware of for which the satisfiability problem is in EXPTIME is studied in (HM97; HM99). Science Institute, Krakow University, in February 1996 !! I wish to express my thanks to Pawel Idziak for his observations on the tree-like structure of the DALLA-models. I am indebted to Ewa Orłowska for bringing to my attention information logics and their computational issues. I wish also to thank the referees for their comments and suggestions and Kumar Neeraj Verma for helpful language corrections.

Fig. 2 .

 2 Fig. 2. Algorithm LA-WORLD

  [e] where Π D e ::= c i | e ∪ * e | e ∩ e . Each c i , i ≥ 0, is a modal constant. DALLA is a variant of the Data Analysis Logic DAL introduced in (FdCO85) (see also another variant in (AT89)) and designed to model reasoning on Pawlak's information systems (see e.g. (Paw91)). The first decidability proof for DALLA can be found in (Dem96) (see a generalization in (Dem98)) but its complexity characterization has been open until now. The DALLA-models are the Kripke style structures of the form W, (R e ) e∈Π D , V where (equiv) every relation R e is an equivalence relation; (∩ + ∪ * ) ∩ and ∪ * are interpreted as intersection and transitive and reflexive closure of the union, respectively; (la) R e and R e are in local agreement for all e, e ∈ Π D . It is not difficult to see that DALLA can be viewed as a fragment of DALLA by identifying [i] and [c i ]. Indeed, one can replace in the definition of DALLAmodels the condition (la) by the condition (la ) defined below and still get the same class of models (see e.g. (DO98, Proposition 10.7)): (la ) R c and R c are in local agreement for all the modal constants c and c .As a consequence, DALLA-satisfiability is PSPACE-hard. The PSPACE upper bound for DALLA satisfiability problem can be proved by using the renaming techniques (see e.g. (Min88)) and results for DALLA as shown in the proof of Lemma 5.1 below.Lemma 5.1. There is polynomial time many-one reduction from DALLA into DALLA .Proof: Let f be the map from the set of DALLA-formulae into the set of DALLA -formulae such that f (φ)def = φ if neither ∩ nor ∪ * occurs in φ, otherwise f (φ) α ](p i new ⇔ ψ i ) such that • {φ 1 , . . . , φ β }, β ≥ 1,are subformulae of φ such that for every i ∈ {1, . . . , β}, φ i is of the form [e ⊕ e ]ψ i for some ⊕ ∈ {∩, ∪ * } and neither ∩ nor ∪ * occurs in ψ i ; • the modal constants in φ are {c 1 , . . . c l }, l ≥ 1; • p 1 new , . . . , p β new are distinct propositional variables that do not occur in φ; • φ is obtained from φ by substituting every occurrence of [e ⊕ e ]ψ i by [e]p i new ∧ [e ]p i new if ⊕ = ∪ * and by [e]p i new ∨ [e ]p i new if ⊕ = ∩.

A linear order is a binary relation that is reflexive, transitive, totally connected and antisymmetric.

[START_REF] Demri | A class of decidable information logics[END_REF] the argument for the decidability of LGM only applies when the set of modal connectives is countable, as it is the case for instance when we consider the set of rational numbers.

Acknowledgements: The proof of the PSPACE lower bound shown in this paper has been inspired from a discussion with Pawel Idziak at the Computer

∇

For instance,

Lemma 4.1 contains some basic properties about the sets cl(u, φ).

Lemma 4.1. Let φ be a formula and u, u ∈ N * be such that u is a prefix of u . Then, (I) cl(u , φ) ⊆ cl(u, φ); (II) if md(cl(u, φ)) = 0, then cl(u • i, φ) = ∅ for every i ∈ N(φ).

In Definition 4.3 below, we define relations between sets of formulae that will be the basis to build binary relations in the L-models obtained from the algorithm defined in Section 4.2 (see the proof of Lemma 4.7).

Definition 4.3. Let X, Y be sets of formulae. The binary relation ≈ i is defined as follows:

The relation ≈ i is an equivalence relation on Refl. As maximally consistent sets for building canonical models from Hilbert-style proof systems for modal logics (see e.g. ( BRV01)), we define below a notion of consistency adapted to the forthcoming tableaux-like method defined in Section 4.2.

Definition 4.4. Let φ be a formula such that N(φ) ≥ 1. Let X be a subset of cl(u, φ) for some u ∈ N * and σ be a bijection σ : {1, . . . , card(N(φ))} → N(φ).

The set X is said to be u, σ -consistent def ⇔ for every ψ ∈ cl(u, φ):

∇

Roughly speaking, the u, σ -consistency entails the maximal propositional consistency with respect to the set cl(u, φ) of formulae. Furthermore, the conditions (3)-(4) in Definition 4.4 are added in order to take into account the reflexivity of R i and the series of inclusions R σ(1) ⊆ . . . ⊆ R σ(n) we wish to enforce, where n = card(N(φ)). Lemma 4.2 below states the natural relationships between the relation ≈ i and the relation R i .

A Proof of Lemma 2.2

The proof is based on results from (HC68; GP92) and is done by induction on card(N(φ)).

For every X ⊆ N, an LGM (X)-formula ψ is an LGM -formula such that N(ψ) ⊆ X.

Base case: card(N(φ)) ≤ 1.

Immediate from the results for the modal logic S5 (HC68, Chapter 3). Induction step: assume that for every LGM -formula

. By adapting definitions from (GP92), an elementary X-disjunction is an LGM (X)-formula of the form

where φ -1 , φ 0 , . . . , φ N are LGM (X \ {i 1 })-formulae. For every LGM (X)-formula φ, if φ ⇔ ψ is LGM -valid and ψ is a conjunction of elementary Xdisjunctions, then ψ is said to be a X-conjunctive form of φ. We show that for every LGM (X)-formula φ, there exists an X-conjunctive form that can be effectively computed. Let i ∈ X and ϕ, ϕ be LGM (X)-formulae such that ϕ is a Boolean combination of formulae prefixed by [i 1 ] or i 1 . The LGM (X)formulae below are LGM -valid:

By the induction on the structure of φ one can show that φ is equivalent to a conjunction of elementary X-disjunctions. The base case (φ is a propositional variable) and the cases in the induction step when the outermost connective of φ is Boolean are standard and they are omitted here. Let φ = [i]φ 1 with i ∈ X \ {i 1 }. By the induction hypothesis, there is a finite set {κ 1 , . . . , κ M } of elementary X-disjunctions such that κ

LGM -valid. The condition (i) above guarantees that for every j ∈ {1, . . . , M }, [i]κ j , has a X-conjunctive form. So φ has a X-conjunctive form. When φ = [i 1 ]φ 1 , the proof is similar to the previous case except that the condition (ii) above is used instead of (i).

Consequently, for every LGM (X)-formula φ, there is a finite set {κ 1 , . .

LGM (X \ {i 1 })-formulae. By the induction hypothesis, each φ i j has an LGMformula ψ i j equivalent to φ i j such that [i]ϕ 1 occurs in the scope of [i ]ϕ 2 in ψ, then i > i . The replacement of LGM equivalent formulae preserves validity, i which allows us to complete the proof easily.

B Proof of Lemma 4.3

Let LA-WORLD(Σ, u, σ, index, Z, φ) be a call in LA-WORLD(Y, , σ, n, N(φ), φ). Suppose that Σ is of the form

such that for every j ∈ {1, . . . , |φ| 2 + 1}, the (i 0 + j)th element of u is i. By definition of LA-WORLD (condition (v)), for every j ∈ {0, . . . , |φ| 2 }, we have

and that there is no X ∈ Σ verifying the conditions (i)-(iii) from Figure 2. By the definition of ≈ i , for all j, j ∈ {0, . . . ,

, there are formulae ψ 1 , . . . , ψ |φ| 2 +1 in cl({φ}) such that for every α ∈ {1, . . . , |φ| 2 +1}. ψ α ∈ X i 0 +α and for every α ∈ {0, . . . , α-1}, ψ α ∈ X i 0 +α . Hence ψ 1 , . . . , ψ |φ| 2 +1 are |φ| 2 + 1 distinct formulae in cl({φ}), which is in contradiction with card(cl({φ})) ≤ |φ| 2 .

C Proof of Lemma 4.8

For every u ∈ N * , for every j ∈ {1, . . . , |u|}, we write u(j) [resp. u[j]] to denote the jth element of u [resp. to denote the prefix of u of length j]. By convention u[0] = . Assume that φ is L-satisfiable with card(N(φ)) = n. There is an Lmodel M = W 0 , (R 0 i ) i∈N , V and w 0 ∈ W 0 such that M 0 , w 0 |= φ. We show that (i) for every u ∈ N * , for every sequence σ 0 , . . . , σ |u| of bijections of the form {1, . . . , n} → N(φ), for every sequence Σ = X 0 , . . . , X |u| such that for every j ∈ {0, . . . , |u|},

ii if there is an L-model M and w ∈ W such that (5) for every

, φ) returns true.

The conditions (1)-(4) state conditions between arguments of successive calls to LA-WORLD whereas the conditions (5)-( 6) are similar to the conditions (Prop1) and (Prop2) from Section 4.2.

By convention, if u = , then σ -1 |u| (last(u)) = n and Z last(u) σ |u| = N(φ). Consequently, by taking Y = {ψ ∈ cl( , φ) : M 0 , w 0 |= ψ}, σ = σ 0 for some bijection σ 0 such that R σ 0 (1) (w 0 ) ⊆ . . . ⊆ R σ 0 (n) (w 0 ), we obtain that LA-WORLD(Y, , σ, n, N(φ), φ) returns true. The proof of (i) is by the induction on the length of u. Base case: |u| > |φ| 3 . By a reasoning similar to the proof of Lemma 4.5, one can that no sequence Σ = X 0 , . . . , X |u| satisfies the conditions above. Induction step: for every u ∈ N * of length |u| ≥ m, (i) holds true. Now assume that u ∈ N * is of length m -1. Let σ 0 , . . . , σ m-1 and Σ = X 0 , . . . , X m-1 satisfy the conditions (1)-(4). Let M = W, (R i ) i∈N , V be an Lmodel and w ∈ W satisfying the conditions ( 5

σ m-1 such that for every X ψ ⊆ cl(u • i, φ), for every bijection σ : {1, . . . , n} → N(φ) such that the conditions (iv)-(vi) from Figure 2 m-1 (i), . . . , n}, X m-1 ≈ σ m-1 (j) Y . If either σ -1 m-1 (last(u)) = σ -1 m-1 (i) or there is no l ∈ {1, . . . , m -1} such that ψ ∈ X l , u = u • i l-1 and for every j ∈ {σ -1 m-1 (last(u)), . . . , n}, X m-1 ≈ σ m-1 (j) X l , by the induction hypothesis, LA-WORLD(Σ • Y, u • i, σ m , σ -1 m (i), Z i σm , φ) returns true, a contradiction.

iii