The Complexity of One-Agent Refinement Modal Logic

1 Introduction

Modal logics with propositional quantifiers have been investigated since Fine's seminal paper [Fine, 1970]. Fine distinguishes three different propositional quantifications, which allow different kinds of model transformations: quantifying over propositionally definable subsets (over booleans), quantifying over subsets definable in the logical language (of basic modalities and quantifiers), and quantifying over all subsets. Only the first two are, in our modern terms, bisimulation preserving. Propositional quantification can easily lead to undecidable logics [Fine, 1970; French, 2006]. Undecidability relies on the ability of propositional quantification to dictate the structural properties of the underlying model [French, 2006]. This has motivated, more recently, the introduction of bisimulation quantified logics [Visser, 1996; Hollenberg, 1998; French, 2006; Pinchinat, 2007]. In this framework, the quantification is over the models which are bisimilar to the current model except for a propositional variable p. This operation is bisimulation preserving, and these logics are decidable.

In [Balbiani et al., 2008] the authors propose a novel way of quantifying, namely over modally definable submodels.

∗The paper on which this extended abstract is based was the recipient of the best paper award of the 2012 JELIA conference in Toulouse [Bozzelli et al., 2012b]. Hans van Ditmarsch is also affiliated to IMSc, Chennai, as research associate.

†Technical University of Madrid (UPM), laura.bozzelli@fi.upm.es

‡LORIA, CNRS / Univ. of Lorraine, hans.vanditmarsch@loria.fr

§ IRISA/INRIA, University of Rennes, Sophie.Pinchinat@irisa.fr Unlike the above proposals, this not merely involves changing the valuation of a proposition in a subdomain, but restricting the model to that subdomain. The setting for these logics is how to quantify over information change. In the logic APAL of [Balbiani et al., 2008], an expression that we might write as ∃ϕ for our purposes stands for 'there is a modal formula ψ such that in the submodel restriction to the states satisfying ψ it holds that ϕ'. This logic is undecidable [French and van Ditmarsch, 2008]. Refinement modal logic (RML) [van Ditmarsch and French, 2009; van Ditmarsch et al., 2010; Bozzelli et al., 2012a] is a generalization of this perspective to more complex model transformations than submodel restrictions. This is achieved by existential and universal quantifiers which range over the refinements of the current model. From the atoms/forth/back requirements of bisimulation, a refinement of a modal structure need only satisfy atoms and back. It is therefore the dual of a simulation that need only satisfy atoms and forth. Refinement is more general than model restriction, since it is equivalent to bisimulation followed by model restriction. From a syntactic point of view it is bisimulation quantification followed by a relativization [Bozzelli et al., 2012a]. Just as in bisimulation quantified logics we have explicit quantification over propositional variables, refinement quantification as it is realized in refinement modal logic is implicit quantification over propositional variables, i.e., quantification over variables not occurring in the formula bound by the quantifier. In RML, an expression ∃rϕ stands for 'there is a refinement wherein it holds that ϕ.'

As an example of a refinement consider the following four rooted (underlined) structures.

With respect to the first model, M, the second one, M ′ , is a model restriction. Model M ′′ is a refinement ofM. It is not a model restriction. However, it is a model restriction of M ′′′ , a bisimilar copy of M. Refinements have really different properties, e.g., a formula like ♦□⊥ ∧ ♦♦□⊥ is clearly false in any model restriction of M, but it true in its refinement M ′′ . In the root of the original model M is satisfied the formula

∃r(♦□⊥∧♦♦□⊥), where ∃r is the refinement quantifier.

As amply illustrated in [Bozzelli et al., 2012a], refinement quantification has applications in many settings: in logics for games [Alur et al., 2002; Pinchinat, 2007], it may correspond to a player discarding some moves; for program logics [Harel et al., 2000], it may correspond to operational refinement; and for logics for spatial reasoning, it may correspond to subspace projections [Parikh et al., 2007].

We now get to the content of this paper and its novel contributions. We focus on complexity issues for (one-agent) refinement modal logic [van Ditmarsch and French, 2009; van Ditmarsch et al., 2010; Bozzelli et al., 2012a], the extension of (one-agent) basic modal logic (ML) obtained by adding the existential and universal refinement quantifiers ∃r and ∀r. It is known [van Ditmarsch et al., 2010; Bozzelli et al., 2012a] that RML has the same expressivity as ML, but the translation of RML into ML is of non-elementary complexity and no elementary upper bound is known for its satisfiability problem [Bozzelli et al., 2012a]. In fact, an upper bound in 2EXPTIME has been claimed in [van Ditmarsch et al., 2010] by a tableaux-based procedure: the authors later concluded that the procedure is sound but not complete [Bozzelli et al., 2012a]. In this paper, we close that gap. We also investigate the complexity of satisfiability for some equi-expressive fragments of RML. We associate with each RML formula ϕ a parameter Υw(ϕ) corresponding to a slight variant of the classical quantifier alternation depth (measured w.r.t. ∃r and ∀r), and for each k ≥ 1 we consider the fragment RMLk consisting of the RML formulas ϕ such that Υw(ϕ) ≤ k. Moreover, we consider the existential (resp., universal) fragment RML∃ (resp. RML∀ ) obtained by disallowing the universal (resp. exist.) refinement quantifier.

In order to present our results, first, we recall some computational complexity classes. We assume familiarity with the standard notions of complexity theory [Johnson, 1990; Papadimitriou, 1994]. We will make use of the levels Σ EXP k (k ≥ 1) of the exponential-time hierarchy EH, which are defined similarly to the levels ΣPk of the polynomial-time hierarchy PH, but with NP replaced with NEXPTIME. In particular, Σ EXP k corresponds to the class of problems decided by single exponential-time bounded Alternating Turing Machines (ATM, for short) with at most k - 1 alternations and where the initial state is existential [Johnson, 1990]. Note that ΣEXP 1 = NEXPTIME. Recall that EH ⊆ EXPSPACE and EXPSPACE corresponds to the class of problems decided by single exponential-time bounded ATM (with no constraint on the number of alternations) [Chandra et al., 1981]. We are also interested in an intermediate class between EH and EXPSPACE, here denoted by AEXPpol, that captures the precise complexity of some relevant problems [Ferrante and Rackoff, 1975; Johnson, 1990; Rybina and Voronkov, 2003] such as the first-order theory of real addition with order [Ferrante and Rackoff, 1975; Johnson, 1990]. Formally, AEXPpol is the class of problems solvable by single exponential-time bounded ATM with a polynomial-bounded number of alternations.

Our complexity results are summarized in Figure 1 where we also recall the well-known complexity of MLsatisfiability. For the upper bounds, the (technically nontrivial) main step in the proposed approach exploits a "small" size model property: we establish that like basic modal logic ML, RML enjoys a single exponential size model property.

Our results are surprising for the following reason. While our results essentially indicate that satisfiability of RML is "only" singly exponentially harder than satisfiability of ML, it is known [Bozzelli et al., 2012a] that RML is doubly exponentially more succinct than ML.

2 Preliminaries

Fix a finite set P of atomic propositions.

A (one-agent Kripke) structure (over P) is a tuple M = 〈S, E, V 〉, where S is a set of states (or worlds), E ⊆ S × S is a transition (or accessibility) relation, and V : S ↦→ 2P is a P -valuation assigning to each state s the set of propositions in P which hold at s. For states s and t of M such that (s, t) ∈ E, we say that t is a successor of s. A pointed structure is a pair (M, s) consisting of a structure M and a designated initial state s of M.

A tree T is a prefix-closed subset of N∗ , where N is the set of natural numbers. The elements of T are called nodes and the empty word ε is the root of T . For x ∈ T , the set of children (or successors) of x is {x·i ∈ T | i ∈ N}. The size |T | of T is the number of T-nodes. A (rooted) tree structure (over P) is a pair 〈T, V 〉 such that T is a tree and V : T ↦→ 2P is a P-valuation over T. For x ∈ T, the tree substructure of 〈T, V 〉 rooted at x is the tree structure 〈Tx, Vx〉, also denoted by 〈T, V 〉x, where Tx = {y ∈ N∗ | x · y ∈ T} and Vx(y) = V (x · y) for all y ∈ Tx. Note that a tree structure 〈T, V 〉 corresponds to the pointed structure (〈T,E, V 〉, ε), where (x, y) ∈ E iff y is a child of x. Moreover, we can associate with any pointed structure (M, s) a tree structure, denoted by Unw(M, s), obtained by unwinding M from s.

For two structures M = 〈S, E, V 〉 and M ′ = 〈S′ , E′ , V ′ 〉, a refinement from M to M ′ is a relation R ⊆ S × S such that for all (s, s′ ) ∈ R: (i) V (s) = V ′ (s′ ), and (ii) if (s′ , t′ ) ∈ E′ for some t′ ∈ S′ , then there is some state t ∈ S such that (s, t) ∈ E and (t, t′ ) ∈ R. If, additionally, the inverse of R is a refinement from M ′ to M, then R is a bisimulation from M to M ′ . For states s ∈ S and s′ ∈ S′ , (M ′ , s′ ) is a refinement of (M, s) (resp., (M, s)

and (M ′ , s′ ) are bisimilar), written (M, s) ≽ (M ′ , s′ ) (resp., (M, s) ≈ (M ′ , s′ )), if there is a refinement (resp., bisimulation) R fromM to M ′ s.t. (s, s′ ) ∈ R. Note that ≽ is a preorder (i.e., reflexive and transitive) and ≈ is an equivalence relation over pointed structures. For each pointed structure (M, s), (M, s) ≈ Unw(M, s).

We recall the syntax and semantics of one-agent refinement modal logic (RML) [van Ditmarsch et al., 2010; Bozzelli et al., 2012a], an equally expressive extension of basic modal logic [Blackburn et al., 2001] obtained by adding the existential and universal refinement quantifiers. For technical convenience, the syntax of RML formulas ϕ over P is given in positive form as:

where p ∈ P, ♦ϕ reads as "possibly ϕ", □ϕ reads as "necessarily ϕ", and ∃r and ∀r are the existential and universal refinement quantifiers. The dual ˜ ϕ of a RML formula ϕ is inductively defined as: ˜ p = ¬p, ˜ ¬p = p,˜ ϕ∨ψ = ˜ ϕ ∧ ˜ ψ, ˜ ♦ϕ = □˜ ϕ, ˜ □ϕ = ♦˜ ϕ, ˜ ∃rϕ = ∀r ˜ ϕ, and ˜ ∀rϕ = ∃r ˜ ϕ. The size |ϕ| of a formula ϕ is the number of distinct subformulas of ϕ. RML is interpreted over pointed structures (M, s). The satisfaction relation (M, s) |= ϕ is inductively defined as usual, we only give the clause for the existential refinement quantifier (the one for the universal quantifier is its dual).

Note that (M, s) |= ϕ iff (M, s) ̸|= ˜ ϕ. If (M, s) |= ϕ, we say that (M, s) satisfies ϕ, or also that (M, s) is a model of ϕ. A RML formula ϕ is satisfiable if ϕ admits some model.

Let ML be the fragment of RML obtained by disallowing the refinement quantifiers, which corresponds to basic modal logic [Blackburn et al., 2001], and RML∀ and RML∃ be the fragments of RML obtained by disallowing the existential refinement quantifier and the universal refinement quantifier, respectively. Moreover, we introduce a family {RMLk }k≥1 of RML-fragments, where RMLk consists of the RML formulas whose weak refinement quantifier alternation depth (see below) is at most k.

Definition 1 (Weak Refinement Quant. Alternation Depth)

We first define the weak alternation length ℓ(χ) of finite sequences χ ∈ {∃r, ∀r}∗ of refinement quantifiers: ℓ(ε) = 0, ℓ(Q) = 1 for every Q ∈ {∃r, ∀r}, and ℓ(QQ′χ) is ℓ(Q′χ) if Q = Q′ , and ℓ(Q′χ) + 1 otherwise. For a RML formula ϕ, let T(ϕ) be the standard tree encoding of ϕ, where each node is labeled by either a modality, or a boolean connective, or an atomic proposition. The weak refinement quantifier alternation depth Υw(ϕ) of a RML formula ϕ is the maximum of the alternation lengths ℓ(χ) where χ is the sequence of refinement quantifiers along a path of T(∃rϕ) (note that we consider T(∃rϕ) and not T(ϕ)).

As an example, for ϕ = ∀r∃rp ∨ □∃r(p ∧ ∀rq), Υw(ϕ) = 3. Note that RML∃ = RML1 and RML∀ ⊆ RML2 . Moreover, for each RML formula ϕ, Υw(∀rϕ) = Υw(˜ ∀rϕ) + 1. The following illustrates the succinctness of RML∃ w.r.t. ML.

Example 1 For n ≥ 1, a n-block is a sequence b1, . . . , bn+1 of n + 1 bits. The following RML∃ formula ϕn is satisfied by a tree structure iff there are two paths from the root encoding two n-blocks of the form b1, . . . , bn, bn+1 and b1, . . . , bn, b′n+1 s.t. bn+1 ̸= b′n+1 : ϕn := ∃r (♦n+1 (0∧¬1)∧ ♦n+1 (1 ∧ ¬ 0) ∧ ∧ni=1 ∨b∈{0,1} □i (b ∧ ¬(1 - b))). One can easily show that any ML formula which is equivalent to ϕn has size singly exponential in n.

For each RML-fragment F, let SAT(F) be the set of satisfiable F formulas. We investigate the complexity of SAT(F) for any F ∈ {RML, RML∃ , RML∀ , RML2 , . . .}. Figure 1 depicts our complexity results.

Since RML is bisimulation invariant [van Ditmarsch et al., 2010; Bozzelli et al., 2012a], and because each pointed structure is bisimilar to its tree unwinding, w.l.o.g. we can assume that the semantics of RML is restricted to tree structures. Further, since RML and ML have the same expressivity [van Ditmarsch et al., 2010; Bozzelli et al., 2012a], we easily obtain:

Proposition 1 (Finite Model Property) Let ϕ be a RML formula and 〈T, V 〉 be a tree structure satisfying ϕ. Then, there is a finite refinement 〈Tr, Vr〉 of 〈T, V 〉 satisfying ϕ.

3 Upper Bounds

We first provide the upper bounds illustrated in Figure 1. Our approach consists of two steps. First we show that RML enjoys a singly exponential size model property. Using this result, we then show that SAT(RML) can be decided by a singly exponential-time bounded ATM whose number of alternations on an input ϕ is at most Υw(ϕ) - 1 and whose initial state is existential.

Theorem 2 (Exponential Size Model Property) For all satisfiable RML formulas ϕ and tree structures 〈T, V 〉 such that 〈T, V 〉 satisfies ϕ: there exists a finite refinement 〈T ′ , V ′ 〉 of 〈T, V 〉 such that 〈T ′ , V ′ 〉 satisfies ϕ and |T ′ | ≤ |ϕ|3|ϕ|2 .

The main steps in the proof of Theorem 2 are as follows. Fix a finite set P of atomic propositions and consider RML formulas and tree structures over P. Given a RML formula ϕ, we associate with ϕ tableaux-based finite objects called constraints systems for ϕ. Essentially, a constraint system S for ϕ is a tuple of hierarchically ordered finite tree structures which intuitively represents an extended model of ϕ: (1) each node x in a tree structure of S is additionally labeled by a set of subformulas of ϕ which hold at the tree substructure rooted at node x, and, in particular, the first tree structure, called main structure, represents a model of ϕ, and (2) the other tree structures of S are used to manage the ∃r-subformulas of ϕ. In fact, in order to be an extended model of ϕ, S has to satisfy additional structural requirements which capture the semantics of the boolean connectives and all the modalities except the universal refinement quantifier ∀r, the latter being only semantically captured. Let C(ϕ) be the set of these constraints systems for ϕ, which are said to be well-formed, saturated, and semantically ∀r-consistent. We individuate a subclass Cmin(ϕ) of C(ϕ) consisting of "minimal" constraints systems for ϕ whose sizes are singly exponential in the size of

ϕ, and which can be obtained from ϕ by applying structural completion rules. Furthermore, we introduce a notion of "refinement" between constraint systems for ϕ which preserves the semantic ∀r-consistency requirement. Then, given a finite tree structure 〈T, V 〉 satisfying ϕ, we show that: (1) there is a constraint system S ∈ C(ϕ) whose main structure is 〈T, V 〉, and (2) starting from S, it is possible to construct a minimal constraint system Smin ∈ Cmin(ϕ) which is a refinement of S. This entails that the main structure of Smin is a refinement of 〈T, V 〉 satisfying ϕ and having a single exponential size. Hence, by Proposition 1, Theorem 2 follows.

Using Theorem 2, we then show Theorem 3 that says that SAT(RML) can be decided by a singly exponential-time bounded ATM whose number of alternations on an input ϕ is at most Υw(ϕ) - 1 and whose initial state is existential.

Theorem 3 SAT(RML) ∈ AEXPpol and SAT(RMLk ) ∈ Σ EXP k for each k ≥ 1.

4 Lower Bounds

We now provide the lower bounds illustrated in Figure 1. The main contribution is AEXPpol-hardness of SAT(RML), which is proved by a polynomial-time reduction from a suitable AEXPpol-complete problem.

For k ≥ 1, a k-ary deterministic Turing Machine is a deterministic Turing machine M = 〈k, I, A, Q, {qacc, qrej}, q0, δ〉 operating on k ordered semi-infinite tapes and having just one read/write head, where: I (resp., A ⊃ I) is the input (resp., work) alphabet, A contains the blank symbol #, Q is the set of states, qacc (resp., qrej) is the terminal accepting (resp., rejecting) state, q0 is the initial state, and δ : (Q\{qacc, qrej})×A→ (Q×A×{-1,+1})∪{1, . . . , k} is the transition function. In each non-terminal step, if the read/write head scans a cell of the ℓth tape (1 ≤ ℓ ≤ k) and (q, a) ∈ (Q \ {qacc, qrej}) × A is the current pair state/ scanned cell content, the following occurs:

• δ(q, a) ∈ Q × A × {-1,+1} (ordinary moves): M overwrites the tape cell being scanned, there is a change of state, and the read/write head moves one position to the left (-1) or right (+1) in accordance with δ(q, a).
• δ(q, a) = h ∈ {1, . . . , k} (jump moves): the read/write head jumps to the left-most cell of the hth tape and the state remains unchanged.

M accepts a k-ary input (w1, . . . ,wk) ∈ (I ∗ )k , written M(w1, . . . , wk), if the computation ofMfrom (w1, . . . , wk) (initially, the ℓth tape contains the word wℓ, and the head points to the left-most cell of the first tape) is accepting.

An instance of the Alternation Problem is a triple (k, n,M), where k ≥ 1, n > 1, and a M is a polynomialtime bounded k-ary deterministic Turing Machine with input alphabet I. The instance (k, n,M) is positive iff the following holds, where Qℓ = ∃ if ℓ is odd, and Qℓ = ∀ otherwise (for all 1 ≤ ℓ ≤ k), Q1x1 ∈ I 2n .Q2x2 ∈ I 2n . . . .Qkxk ∈ I 2n .M(x1, . . . , xk). Note that the quantifications Qi are restricted to words over I of length 2n .

For k ≥ 1, the k-Alternation Problem is the Alternation Problem restricted to instances of the form (k, n,M) (i.e., the first input parameter is fixed to k), and the Linear Alternation Problem is the Alternation Problem restricted to instances of the form (n, n,M). The following Prop. is then standard.

Proposition 4 The Linear Alternation Problem is AEXPpolcomplete and for all k ≥ 1, the k-Alternation Problem is Σ EXP k -complete.

We then proceed as follows. Fix an instance (k, n,M) of the Alternation Problem with M = 〈k, I, A, Q, {qacc, qrej}, q0, δ〉. Since M is polynomial-time bounded, there is an integer constant c ≥ 1 such that when started on a k-ary input (w1, . . . , wk), M reaches a terminal configuration in at most (|w1| + . . . + |wk|)c steps. A (k, n)-input is a k-ary input (w1, . . . ,wk) such that wi ∈ I 2n for all 1 ≤ i ≤ k. Let c(k, n) := c · (n+⌈log k⌉), where ⌈log k⌉ denotes the smallest i ∈ N such that i ≥ log k. Note that a configuration of M reachable from a (k, n)-input, called (k, n)-configuration, can be described as a tuple -→C = (C1, . . . ,Ck) of k words C1, . . . ,Ck over A∪ (Q×A) of length exactly 2c(k,n) such that for some 1 ≤ ℓ ≤ k, Cℓ is of the form w · (q, a) · w′ ∈ A∗ × (Q × A) × A∗ , and for i ̸= ℓ, Ci ∈ A2c(k,n) . For a (k, n)-input (a · w1, . . . ,wk), the associated initial (k, n)-configuration is ((q0, a) · w1 · #2c(k,n)-2n , . . . ,wk · #2c(k,n)-2n ). Thus, the computations of M from (k, n)- inputs, called (k, n)-computations, can be described by sequences π of at most 2c(k,n) (k, n)-configurations. In fact, w.l.o.g., we can assume that π has length exactly 2c(k,n) . This makes it possible to prove Th. 5. In the omitted proof we need an encoding of (k, n)-computations by suitable tree structures, called (k, n)-computation tree code.

Theorem 5 One can construct a RMLk+1 formula ϕ in time polynomial in n, k, and the size of the TMMsuch that (i) ϕ is a RML∀ formula if k = 1, and (ii) ϕ is satisfiable iff the instance (k, n,M) of the Alternation Problem is positive.

From Proposition 4 and Theorem 5 we also obtain:

Corollary 6 SAT(RML) is AEXPpol-hard, SAT(RML∀ ) is NEXPTIME-hard, and for all k ≥ 1, SAT(RMLk+1 ) is Σ EXP k -hard.

5 Concluding Remarks

An intriguing question left open is the complexity of satisfiability for multi-agent RML [van Ditmarsch et al., 2010; Bozzelli et al., 2012a]. Our approach does not seem to scale to the multi-agent case. Another interesting direction is to investigate the exact complexity of the fragments RML∃ , RML∀ , and RMLk , and the succinctness gap between RMLk and RMLk+1 for each k ≥ 1. Furthermore, since the modal µ-calculus extended with refinement quantifiers (RMLµ , for short) is non-elementarily decidable [Bozzelli et al., 2012a], it would be interesting to individuate weak forms of interactions between fixed-points and refinement quantifiers, which may lead to elementarily decidable and interesting RMLµ - fragments.