We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae , ′, decide whether there is a modal formula that separates them, that is, that satisfies |= |= ¬ ′. This problem has applications for finding simple reasons for inconsistency. Our main contributions are tight complexity bounds for deciding modal separability and optimal ways to compute a separator if it exists. More precisely, it is ExpTime-complete in general and PSpace-complete over words. Separators can be computed in doubly exponential time in general and in exponential time over words, and this is optimal as well. The results for general structures transfer to arbitrary, finitely branching, and finite trees. The word case results hold for finite, infinite, and arbitrary words.
Generalizing the example, in this paper we investigate ML-separability of formulae in the modal
-calculus ML [
Our results generalize the ML-definability problem for ML which was shown decidable by Otto [6,
Main Theorem]. The adaptation of the argument to the more general separability is relatively easy.
However, Otto’s paper is focussed on deciding the existence of modal definitions. The problem of
computing a definition when it exists is not discussed, and it seems that the formula which can be read
of from the proof is at least tower-exponential big. This issue was addressed in [
We consider both general models and “word models” which are Kripke structures in which each point has at most one successor. The latter are relevant from a verification perspective and for temporal reasoning. In order to obtain our results we first prove model-theoretic characterizations in terms of bisimulations. We then exploit the close connection of ML to nondeterministic parity tree automata to give (1) optimal procedures for the separability problem and (2) upper bounds on the modal depth of a separator, if it exists. In (1) we show ExpTime-completeness of modal separability in general and PSpace-completeness over words. The lower bounds are essentially inherited from satisfiability. The upper bounds derived in (2) are then used together with the automata to compute so-called -uniform consequences, that is, modal formulae that have exactly the same modal consequences as a given MLformula, up to modal depth . These -uniform consequences are then used as separators. Also here, our procedures are optimal: they compute separators of at most double exponential size, and we show that there are ML-formulae that are expressible in ML but any equivalent ML-formulae must have doubly exponential size. This means that there is a double exponential succinctness gap between ML and ML. In the word case, our procedures compute exponentially sized separators and there is only an exponential succinctness gap. All lower bounds (both computational and succinctness) already hold for PDL (ℒreg) in place of ML, and for definability in place of separability.
It is interesting to note that our results hold over classes of models definable by ML-formulae. This observation allows us to cover the more general notion of separation in presence of an ontology (i.e. a background theory imposing some conditions on models). As long as the ontology is expressible in ML, separability and computation of separators reduce to the ontology-free setting. Without much efort the same observation lets us transfer our results to finite words, infinite words, and finite trees.
All the missing proofs and constructions can be found in the full version [
Related Work. Separability has been intensively studied in formal language theory. A seminal
result in this area is that separability of regular word languages by a first-order language is decidable
in ExpTime [
In logic, a recent work investigates the complexity of separating between formulae supporting
counting quantifiers by formulae that do not support them [
Another related problem is the question of interpolant existence. An interpolant of two ℒ-formulae
and ′ is an ℒ-formula with |= |= ′ and such that the signature of is contained in the
signatures of both and ′. Thus, the problem resembles separability but the restriction on is in
terms of the signature instead of in terms of the logic. Sometimes this question reduces to entailment, as
many logics enjoy the Craig interpolation property: an interpolant of and ′ exists whenever |= ′.
Interpolant existence for logics that lack Craig interpolation has recently been studied in [
Finally, a related problem is separability of data examples. There, the task is to separate sets of pointed
structures instead of formulae (see [
Assuming familiarity of the reader with modal logic and the modal -calculus, we recall here only
the main notions and refer to [
Syntax. We consider modal logic ML and its fixpoint extension ML over a modal signature consisting of two finite sets: actions Act and propositions Prop. The syntax of ML is given as: ::= ⊤ | ⊥ | | ¬ | ∨ | ∧ | ⟨a⟩ | [a] with ∈ Prop and a ∈ Act. If Act = {a} is a singleton, we use ◇ and 2 in place of ⟨a⟩ and [a] . The syntax of ML is obtained by extending the above with additional clauses: ::= | . | . where belongs to a fixed set Var of variables. The restriction to a fixed finite signature is only for the sake of readability. All results in the paper remain true with arbitrary signature.
Semantics. The models we consider are pointed Kripke structures. That is, a model ℳ consists of a set (called its universe) with a distinguished point ∈ called the root, an interpretation →a ⊆ × for every a ∈ Act and a valuation val : → (Prop). We call the set (Prop) colors and denote it by Σ . Both ML and ML are interpreted in points of models in a standard way. Since models are by definition pointed we write ℳ |= meaning that the root of ℳ satisfies . The same symbol denotes entailment: |= means that every model of is a model of . In the case only models from some fixed class are considered we talk about satisfiability and entailment over and in the latter case write |
= .
A particularly relevant class of models are trees. A model ℳ is a tree if the underlying directed graph (, ⋃︀{ →a | a ∈ Act}) is a tree with as its root. The branching or outdegree of a point is the number of its children in this underlying graph. The class of all trees is denoted by Trees. We identify words (both finite and infinite) over alphabet Σ with trees over a single action of outdegree at most one. Points of such models are interpreted as positions in the word, the unique accessibility relation represents the successor relation, and the valuation determines the letter at each position. A prefix of a tree is a subset of its universe closed under taking ancestors. When no confusion arises we identify a prefix ⊆ with the induced subtree of ℳ that has as its universe. The depth of a point is the distance from the root. The prefix of depth (or just -prefix ) is the set of all points at depth at most and is denoted by | (and the corresponding subtree by ℳ| ).
We define bisimulations and bisimilarity in a standard way except that in the case of trees for convenience we assume that bisimulations only link points at the same depth. An -step bisimulation (or just -bisimulation) between trees ℳ and is a bisimulation between their -prefixes. We denote -bisimilarity by
-.
Size of formulae. The size of a formula , denoted | |, is the number of nodes in its syntax tree. Similarly, its depth is the maximal length of paths in the syntax tree. The depth of a formula should not be confused with its modal depth which is the maximal nesting of modal operators; all formulae of modal depth at most are denoted ML.
When we specify formulae in the paper, we use syntactic sugar ⋁︀ Φ , ⋀︀ Φ , and nabla ∇Φ , for finite sets of formulae Φ . The first two are self-explanatory and allow for higher branching in the syntax tree. The last one, ∇Φ , intuitively means that “every formula in Φ is true in some child and every child satisfies some formula from Φ ” and is an abbreviation for ∇Φ = ⋀︀ ∈Φ ◇ ∧ 2 ⋁︀ ∈Φ . (1) It is well-known that ⋁︀ Φ and ⋀︀ Φ can be rewritten into basic syntax under polynomial cost. We also include the colors Σ directly in the syntax: ∈ Σ is a shorthand for the formula ⋀︀{, ¬ ′ | ∈ , ′ ∈/ }. Rewriting colors increases the size only by a factor linear in |Prop|.
Automata. Throughout the paper we use automata over tree models of both bounded and arbitrary outdegree. A nondeterministic parity tree automaton (NPTA) is a tuple = (, Σ , , , rank) where is a finite set of states, ∈ is the initial state, Σ is the alphabet fixed above, and rank assigns each state a priority. The transition function is of type: : × Σ
→ (()).
Intuitively, (, ) = {1, ..., } means that in the state upon reading color the automaton (i) chooses a transition and (ii) labels all the children of the current point with states from so that every ∈ is assigned to some child. A run of on a tree ℳ is an assignment : → consistent with in such sense and sending the root of the tree to . The run is accepting if for every infinite path 0, 1 . . . in ℳ the sequence rank( (0)), rank( (1)), . . . satisfies the parity condition. We write ℳ |= in case has an accepting run on ℳ. An automaton that is identical to except that the original initial state is replaced with is denoted [ ← [ ]. We refer with NPWA to an NPTA working over words.
In NPTAs over trees of bounded outdegree it might be more common to use a transition function
of type : × Σ → (), but the diference is not essential: our NPTAs can be represented in this
way and conversely, all relevant constructions for such NPTAs can be adapted to our setting. Most
importantly, we rely on the following classical result (see for example the discussion in [
We start with recalling the notion of separability and discuss some of its basic properties.
is a modal separator over a class if | = = and | ¬ ′.
′ is ∈ ML with |= and |= ¬ ′. It
The notion induces the problem of modal separability: given two ML-formulae , ′, decide whether a modal separator exists. Clearly, ML-definability of or ′ is a suficient condition for the existence of a modal separator between , ′. However, Example 1 shows that it is not a necessary one: neither nor ′ are ML-definable, yet a separator exists. We make some foundational observations.
Inspired by the notion of Craig interpolation, one could also consider the notion of a Craig modal separator, which is a modal separator of , ′ which only uses symbols occurring in both and ′. However, based on the fact that ML enjoys Craig interpolation, we show in Theorem 2 (proof in the full version) that Craig modal separability and modal separability coincide. Since ML enjoys Craig interpolation over many classes of models [18, Theorem 1], Theorem 2 remains true over all classes of models considered below. We thus focus on modal separability.
Theorem 2. , ′ ∈ ML admit a modal separator if they admit a Craig modal separator.
Inspired by the notion of uniform interpolation [
Since ML has both the finite model property and the (finitely branching) tree model property, the notions of a modal separator over finite models, arbitrary tree models, and finitely branching tree models all coincide with modal separator (over arbitrary models). Unsurprisingly, this does not apply to the class of all finite trees.
Example 2. Consider a ML-formula ∞ = . ◇ expressing that there exists an infinite path originating in the root. It is satisfiable, but unsatisfiable over finite trees. Thus ⊥ is an ML-definition of ∞ over ifnite trees, but ∞ is not ML-definable (over arbitrary models).
We deal with separability over finite trees as follows. Call a class of models ML-definable in if there is a ML-formula such that ℳ ∈ if ℳ |= , for all models ℳ ∈ .
Lemma 1. Let be ML-definable in by and let ∈ ML. Then is a modal separator of , ′ ∈ ML over if is a modal separator of ∧ and ∧ ′ over .
Intuitively, Lemma 1 provides us with a reduction of modal separability over to modal separability over (the larger) . It has a number of interesting consequences. First, observe that the formula ¬ ∞ from Example 2 defines the class of finite trees in the class of all finitely branching trees. Hence ¬ ∞ provides a reduction of modal separability over finite trees to modal separability over finitely branching trees, and thus to modal separability. Similarly, and again using ∞, Lemma 1 reduces modal separability over finite words and over infinite words to modal separability over (arbitrary) words. Finally, the lemma can be used to reduce modal separability relative to background knowledge to modal separability. Call a modal separator of , ′ ∈ ML relative to 0 ∈ ML if it is a modal separator of , ′ over the class of models satisfying 0 in every point. This setting is most relevant for the DL community since 0 plays the role of an ontology. In particular, the question whether two ℒreg-concepts , ′ are separable by an ℒ-concept relative to an ℒreg-ontology is an instance of that problem (recall that every ℒreg-concept can be expressed as a ML-formula). Let be the ML-formula expressing that 0 is satisfied in every point reachable via the accessibility relations. Using Lemma 1 and bisimulation invariance of ML, it is routine to verify that is a modal separator of , ′ relative to 0 if is a modal separator of ∧ and ∧ ′.
In view of what was said so far, we will from now on concentrate on deciding modal separability over general and word models and computing separators if they exist. A main ingredient for both tasks is to show that if there is a modal separator for ML-formula , ′, then there is one of modal depth at most exponential in the size of and ′. As a necessary tool for showing this exponential bound on , and for eficiently deciding if a given sufices, we establish the following model-theoretic characterization. Fix , ′ ∈ ML for the rest of the paper and denote their size by = | | + | ′|. Proposition 1. Let ∈ N. The following are equivalent: (i) There is ∈ ML of modal depth separating and ′; (ii) For all models ℳ and ℳ′ bisimilar up to depth : ℳ |= implies ℳ′ ̸|= ′; (iii) For all trees ℳ and ℳ′ identical up to depth : ℳ |= implies ℳ′ ̸|= ′; (iv) For all trees ℳ and ℳ′ identical up to depth and whose branching is bounded by : ℳ |= implies ℳ′ ̸|= ′.
The proof can be found in the full version. Based on Proposition 1, we show that ML-separability of ML-formulae is ExpTime-complete and thus not harder than ML-definability.
Theorem 3. Modal separability of ML-formulae is ExpTime-complete over arbitrary models.
ExpTime-hardness already holds for ML-definability and is proved by an immediate reduction
from ML-satisfiability, which is ExpTime-complete already for its fragment PDL [3, Section 4]. It
is not hard to modify the original hardness proof for PDL-satisfiability to work over finite trees, so
Theorem 3 remains valid over finite trees as well. For the upper bound, we mostly follow the technical
development in [
Over words, we essentially follow the same approach. Since the tree automata used in the proof of Theorem 3 can be replaced by word automata, the complexity drops to PSpace. A matching lower bound can be derived as above by a reduction from satisfiability in LTL over words [21, Theorem 4.1] (which, in fact, can be rephrased in terms of PDL).
Theorem 4. Modal separability of ML-formulae is PSpace-complete over words.
The proofs for both cases, the case of arbitrary models and the case of words, can be found in the full version. As announced, an important step in the proofs of the upper bounds is the following proposition which we will also use later.
Proposition 2. If , ′ ∈ ML are separable then they are separable by a formula of modal depth exponential in their size . The same is true over words.
In the remainder of the paper we will deal with computing separators based on Proposition 2. Before
we proceed, let us note that our approach difers from the treatment of modal definability from [
Given ∈ ML and ∈ N, a formula ∈ ML is an -uniform consequence of if, for Definition 2. all ∈ ML: |= ⇐⇒ |= An analogous notion relative to a fixed class of models is obtained by replacing |= with |=.
In words: is an -uniform consequence of if it has modal depth , is a consequence of , and entails every other consequence of of modal depth . In particular, if and ′ are separable by some modal formula of modal depth and is an -uniform consequence of , then this separates from ′ as well. Observe that -uniform consequences exist for every ∈ ML and ∈ N. Indeed, given and we can obtain an -uniform consequence of by taking the disjunction of all ML-types consistent with . Here, by an ML-type we mean a maximal consistent subset of ML. Since up to equivalence there are only finitely many formulae in ML, each ML-type can be represented as a single ML-formula and the mentioned disjunction is well-defined.
In view of Proposition 2, it thus sufices to compute -uniform consequences of . Unfortunately, the naive construction given above is nonelementary in the size of the separated formulae and ′. In the next sections we give better constructions.
We construct doubly exponentially sized separators and provide matching lower bounds. 4.1. Construction Theorem 5. If and ′ are modally separable then a separator of size doubly exponential in = | | + | ′| exists and can be computed in doubly exponential time.
Lemma 2. For every ∈ ML and ∈ N, one can construct an -uniform consequence ∈ ML of with branching doubly exponential in | | and depth linear in .
We show how Theorem 5 follows from Lemma 2. Proposition 2 guarantees that if a modal separator for and ′ exists then there is one with modal depth exponential in . Since entails this separator it follows that is a separator itself.
The branching of is at most doubly exponential in | | and thus also in : ≤ 22 for some constant . The depth of is linear in and therefore ≤ 2 for some . Altogether this means that the size of :
| | ≤ ≤ (22 )2 is at most doubly exponential in . It remains to prove Lemma 2.
Proof. Let = (, Σ , , , rank) be the NPTA equivalent to with exponentially many states, which exists due to Theorem 1. For each ∈ N and ∈ we construct , ∈ ML of branching 22|| such that: ℳ |= , ⇐⇒
there exists |= [ ← [ ] with ℳ - (2) for every structure ℳ. Then, , is our desired -uniform consequence of .
We proceed by induction on ∈ N. For the base case we put:
0, = ⋁︁{ ∈ Σ | there is |= [ ← [ ] with |= } which clearly satisfies the induction goal (2). For the induction step define: +1, = ⋁︁ ⋁︁ ∈Σ ∈ (,) ∧ ∇{ , | ∈ }.
The proof that the above construction preserves (2) is not hard and can be found in the full version.
Let us remark that Lemma 2 can be easily adapted to deal with vocabulary restrictions. That is, given ⊆ Prop we could construct similar to but only using atomic propositions from and only entailing ML-consequences of whose vocabulary is contained in . To that end, it sufices to project-out atomic propositions not in from the automaton and only then proceed with our construction. Such (, )-uniform consequence of can then be taken as a Craig modal separator, in the same way as serves as a modal separator. 4.2. Lower bounds
For the lower bounds, we show that over arbitrary structures (in fact, already binary trees) ML is doubly exponentially more succinct than ML. The example is essentially taken from [22, Section 3.1]. There the authors use game-theoretic tools which are later applied to more complicated cases. Since we are only interested in this example, we provide a straightforward self-contained argument. Proposition 3. There is a sequence ( )∈N of ML-formulae of size polynomial in such that each is equivalent to a ML-formula but every ∈ ML equivalent to has size at least 22 . Proof. We only give a sketch, the details are found in the full version. We assume two diferent actions a and b. For each ∈ N consider the property:
: “No path (over all actions) longer than 2 starts in the root.” eficient, in ML.
This can be enforced by encoding an -bit binary counter into the structure of the model, and requiring that on every path the counter values are strictly increasing. Let be this (technically stronger) property expressing the behavior of the encoded counter. Assuming that the encoding is reasonably can be easily expressed by a ML-formula of size polynomial in (in fact, a weak fragment of PDL is already suficient). Since the lengths of paths are bounded, can be also expressed
of actions a and b of length 2, the syntax tree of must contain a descending sequence of subformulae of length 2 such that the -th subformula begins with a modal operator corresponding to the -th ∈ ML equivalent to has size at least 22 . The reason is that for every sequence action. This allows to embed a binary tree of height 2 into the syntax tree of .
Note that the presence of two diferent actions a and b is essential for the argument. We conjecture that ML is doubly exponentially more succinct than ML already in the monomodal setting. Consider the following Property , parameterized by ∈ N:
: “ and there exists a maximal path on which the number of points satisfying is even.” where is the same as in Proposition 3. It is not dificult to come up with small, that is, of size polynomial in , ML-formulae ′ expressing . Unfortunately, proving that no small ML formula can be equivalent to ′ seems dificult. For instance, consider models where every non-leaf point has a child satisfying and a child satisfying ¬ . Then a trick similar to the famous example of Potthof (showing, roughly, that the language of all binary trees of even depth is first-order definable) [ 23, Example 1] can be exploited to get a modal formula equivalent to ′ (over such models), but of size only single exponential in . Moreover, the results in the next Section 5 show that looking at words only is not suficient either.
In this section we show that optimal modal separators (over words) can be computed exponentially faster and are exponentially smaller compared to the case with arbitrary models. exists and can be computed in exponential time.
Theorem 6. If and ′ are modally separable over words, then a separator of size exponential in | | + | ′|
As with arbitrary models, Proposition 2 gives an upper bound on the modal depth of a separator and so it sufices to construct
-uniform consequences of of small size.
We illustrate the idea first. Consider the classes
of length in which proposition is satisfied in an even and odd, respectively, number of points. Constructing modal formulae and ′ defining EVEN and ODD in the following, naive way leads to exponential formulae since +1 contains both and and ′: 0 = ¬ ∧ 2⊥ ′0 = ∧ 2⊥ +1 = ◇⊤ ∧ ︀( ( ∧ ′) ∨ (¬ ∧ )︀) ′+1 = ◇⊤ ∧ ︀( ( ∧ ) ∨ (¬ ∧ ′))︀ This exponential blow-up can be avoided, however, using “divide-and-conquer” as follows: 2 = (︀ ∧ ◇ ︀) ∨ ︀( ′ ∧ ◇ ′)︀
′2 = (︀ ∧ ◇ ′)︀ ∨ ︀( ′ ∧ ◇
︀) Although several copies of formulae of smaller index are used as well, but since the index is halved, we end up with formulae of roughly quadradic size. The proof of the following analogue of Lemma 2 relies on this idea.
Lemma 3. For every ∈ N and every NPWA with states , one can construct a formula ∈ ML which is ’s -uniform consequence over words and has size polynomial in and ||. The construction requires polynomial time.
To see that Lemma 3 implies Theorem 6, let and ′ admit a modal separator over words. Let be an NPWA that is equivalent to . By Theorem 1, has exponentially many states and can be computed in exponential time. Proposition 2 implies that there is a modal separator of modal depth at most exponential in = | | + | ′|. As with arbitrary models, ’s -uniform consequence from Lemma 3 is the sought separator. We now prove the lemma.
Proof. Let = (, Σ , , , rank) be an NPWA. The main idea is to construct, for every , ∈ and ∈ N, a formula , such that for every input word ℳ: ℳ |= , ⇐⇒ there is a run from to over the -prefix of ℳ, The key step is the recursive splitting similar to the definitions of EVEN and ODD above. Intuitively, 2, is the disjunction over all ∈ of the conditions “there is a run from in the initial position to in position , and a run from in position to in position 2.” The latter conditions are recursively expressed using , and ,. The constructed formulas ,, ≤ are then used to describe all possible -prefixes of models of . The details of the construction are described in the full version.
We conclude the section with the comment that Theorem 6 is optimal in the sense that there are modally separable formulae which require a large separator. We actually show the following stronger statement implying that, over words, ML is exponentially more succinct than ML. Proposition 4. There is a sequence of ML-formulae ( )∈N of size polynomial in such that each is equivalent to a ML-formula but every ∈ ML equivalent to has size at least 2.
The proof is entirely standard. The main idea is that, already in PDL one can stipulate (with a small formula) a finite word of exponential length. Clearly, any ML-formula expressing this requires exponential size. The only dificulty is doing it with a fixed signature: instead of encoding -bit counters using propositions, we use just two propositions and encode numbers in consecutive points.
We have studied the problem of deciding separability of ML-formulae by fixpoint free formulae from ML, and computing separators if they exist. Our results cover several interesting classes of models such as trees, finite trees, and words. Due to the great expressivity of ML the results remain valid in the presence of ontologies.
A notably missing case is the class of trees of fixed outdegree independent from formulae. This is surprisingly diferent from the classes we studied. The key dificulty here lies in the fact that the implication (iii) ⇒ (ii) from Proposition 1 is not true over such trees.
An intriguing challenge left for future study is to look at extensions of ML and/or ML. Natural
extensions are inverse modalities, the universal modality, graded modalities, and constants
(corresponding to inverse roles, the universal role, counting quantifiers, and nominals in DL speech). We expect
the adaptation to inverse modalities to be only minor. Also graded modalities look innocent if they
are allowed both in the larger logic and in the separator logic. If we only extend ML with graded
modalities and ask for separators in ML (without graded modailites), we would have to combine our
techniques with the ones from [
Acknowledgements