Facundo Carreiro

Stéphane Demri

Beyond Regularity for Presburger Modal Logics

Keywords: Presburger constraint, context-free constraint, decidability, POL

Satisfiability problem for modal logic K with quantifier-free Presburger and regularity constraints (EML) is known to be pspace-complete. In this paper, we consider its extension with nonregular constraints, and more specifically those expressed by visibly pushdown languages (VPL). This class of languages behaves nicely, in particular when combined with Propositional Dynamic Logic (PDL). By extending EML, we show that decidability is preserved if we allow at most one positive VPL-constraint at each modal depth. However, the presence of two VPL-contraints or the presence of a negative occurrence of a single VPL-constraint leads to undecidability. These results contrast with the decidability of PDL augmented with VPL-constraints.

Introduction

Presburger modal logics. Graded modal logics are extensions of modal logic K in which the modality 3 (see e.g. [START_REF] Blackburn | Modal Logic[END_REF]) is replaced by 3 n ; the formula 3 n p states that there are at least n successor worlds satisfying the proposition p, early works about such counting operators can be found in [START_REF] Fine | In so many possible worlds[END_REF][START_REF] Barnaba | Graded modalities[END_REF][START_REF] Cerrato | General canonical models for graded normal logics[END_REF]. In [START_REF] Tobies | PSPACE reasoning for graded modal logics[END_REF], the minimal graded modal logic, counterpart of the modal logic K, is shown decidable in pspace. Recent complexity results can be found in [START_REF] Kazakov | A note on the complexity of the satisfiability problem for graded modal logic[END_REF], see also enriched logics with graded modalities in [START_REF] Kupferman | The complexity of the graded µ-calculus[END_REF][START_REF] Bonatti | The complexity of enriched mu-calculi[END_REF]. Nevertheless, richer arithmetical constraints about successor worlds are conceivable. For instance, in the majority logic [START_REF] Pacuit | Majority logic[END_REF], one can express that more than half of the successors satisfy a given formula. All of the above constraints, and many more, are expressible in Presburger arithmetic (PrA), the decidable first-order theory of natural numbers with addition. In the sequel, Presburger modal logics refer to logics admitting arithmetical constraints from PrA. Not only arithmetical constraints from graded modal logics have been considered in several classes of non-classical logics, including epistemic logics [START_REF] Van Der Hoek | Graded modalities in epistemic logic[END_REF] and description logics [START_REF] Hollunder | Qualifying number restrictions in concept languages[END_REF][START_REF] Calvanese | Expressive description logics[END_REF][START_REF] Areces | Modal Logics with Counting[END_REF] but also pspace-complete logics with richer arithmetical constraints have been designed [START_REF] Schröder | PSPACE bounds for rank-1 modal logics[END_REF][START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF][START_REF] Cîrstea | Modal logics are coalgebraic[END_REF]. If the pspace upper bound is given up, modal-like logics with more expressive Presburger constraints on the number of children can be found in [START_REF] Kupferman | The complexity of the graded µ-calculus[END_REF][START_REF] Zilio | XML schema, tree logic and sheaves automata[END_REF][START_REF] Seidl | Counting in trees[END_REF].

Assuming that the children of a node are ordered, it is possible to enrich Presburger modal logics with regularity constraints related to the ordering of siblings. This is particularly meaningful to design logical formalisms to query XML documents viewed as finite ordered unranked labeled trees; such logical and automata-based formalisms can be found, e.g., in [START_REF] Zilio | XML schema, tree logic and sheaves automata[END_REF][START_REF] Seidl | Counting in trees[END_REF]. For instance, a logic with fixpoint operators, arithmetical and regularity constraints is introduced in [START_REF] Seidl | Counting in trees[END_REF] and shown decidable with an exponential-time complexity, which improves results for description logics with qualified number restrictions [START_REF] Calvanese | Expressive description logics[END_REF]. Similarly, the main goal of [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF] was to introduce a Presburger modal logic EML with regularity constraints as in the logical formalisms from [START_REF] Wolper | Temporal logic can be more expressive[END_REF][START_REF] Zilio | XML schema, tree logic and sheaves automata[END_REF][START_REF] Seidl | Counting in trees[END_REF] with a satisfiability problem that could still be solved in polynomial space.

Our motivations: beyond regularity. The pspace upper bound established in [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF] for the satisfiability problem for EML is based on a Ladner-like algorithm [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. Moreover it takes advantage of the properties that the commutative images of context-free languages (CFLs) are effectively semilinear [START_REF] Parikh | On context-free languages[END_REF] and satisfiability for existential Presburger formulae can be solved in np thanks to the existence of small solutions [START_REF] Borosh | Bounds on positive integral solutions of linear diophantine equations[END_REF]. In this paper, our goal is to revisit decidability and complexity results for Presburger modal logics when context-free constraints are considered instead of regular ones. Usefulness of such contraints is best witnessed by their use to define Document Type Definitions (DTDs) for XML documents or to express nonregular programs as done in [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF], but the paper focuses on decidability issues. However, it is not reasonable to expect that adding all context-free languages (CFLs) would preserve decidability. We are aware of several situations in which such an extension does not preserve decidability. For instance, PDL with regular programs augmented with the context-free program {a i ba i : i 0} is known to be undecidable [START_REF] Harel | Propositional dynamic logic of nonregular programs[END_REF]. On the other hand, PDL augmented with context-free programs definable by semisimple minded pushdown automata is decidable [START_REF] Harel | Strengthened Results on Nonregular PDL[END_REF]. In such pushdown automata, the input symbol determines the stack operation to be performed, the next control state and the symbol to be pushed in case of a push operation. The ultimate decidability result has been obtained for PDL augmented by programs definable by visibly pushdown automata (VPA) [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF]. These automata are introduced in [START_REF] Alur | Visibly pushdown languages[END_REF] (see also the equivalent class of input-driven pushdown automata in [START_REF] Mehlhorn | Pebbling mountain ranges and its application to DCFL-recognization[END_REF]) and are motivated by verification problems for recursive state machines. They generalize the semi-simple-minded pushdown automata since we only require that the input symbol determines the stack operation.

The initial motivation for this work is to understand the decidability status of EML augmented with context-free constraints from VPAs (VPL-constraints). Also, the decidability proof for EML takes advantage of the Boolean closure of regular languages, which is also the case for visibly pushdown languages [START_REF] Alur | Visibly pushdown languages[END_REF] (complementation can be performed in exponential time and causes -only-an exponential blow-up [START_REF] Alur | Visibly pushdown languages[END_REF]). Moreover, by [START_REF] Verma | On the complexity of equational Horn clauses[END_REF], from a VPA, one can compute in linear time a simple Presburger formula whose solutions are the Parikh image of its language. This may allow us to extend [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]. Hence, boosted by the decidability and complexity results from [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF] for PDL with VPA and by the nice properties of VPLs, we aim at understanding how much of the power of context-free constraints can be added to EML while still preserving decidability.

Our contributions. We can distinguish three types of contributions: showing that different extensions of EML have identical expressive power, proving undecidability results when context-free constraints are present in formulae and establishing decidability for the satisfiability problem of EML extended with restricted context-free constraints.

• EML extended with VPL-constraints such that at each depth, there are at most i such constraints (written EML i (VPL)) is expressively equivalent to EML extended with CFL-constraints such that at each depth, there are at most i such constraints (written EML i (CFL)).

• We show that a strict fragment of EML 2 (CFL), with only positive CFLconstraints, and a strict fragment of EML 1 (CFL), with a single CFL-constraint occurring negatively, have undecidable satisfiability problems.

• Last, but not least, we show that EML + 1 (CFL), a fragment of EML 1 (CFL) but a substantial extension of EML, has a decidable satisfiability problem by extending the proof technique from [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]. Herein, EML + 1 (CFL) denotes the fragment of EML 1 (CFL) in which at each depth, there is at most one context-free constraint and it occurs positively plus additional more technical conditions. Positive occurrences of constraints shall be defined in Section 2 and this notion slightly differs from the one that only counts the number of negations. This is the best we can hope for in view of the previous results.

It was unexpected that EML 2 (VPL) is already undecidable. Decidability can be regained if only one VPL-constraint occurs positively at each depth. If only one VPL-constraint may occur negatively at each depth, then undecidability is back. This contrasts with the decidability of PDL extended with VPAs [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF] or with the undecidability of LTL extended with a fixed VPA [START_REF] Demri | Chapter 'Specification and Verification using Temporal Logics' in Modern Applications of Automata Theory[END_REF]. Since modal logic K is a fragment of PDL, this seems to contradict the undecidability of EML 2 (CFL). However, language-based constraints on PDL are related to paths whereas in EML it is related to the ordering of successor worlds. Moreover, a CFL-constraint L(p 1 , . . . , p n ) on the children can be turned into an arithmetical constraint by using Parikh's Theorem [START_REF] Parikh | On context-free languages[END_REF]. In a sense, CFL-constraints on the successor worlds can be handled by arithmetical constraints. Again, this seems to contradict the undecidability of EML(CFL) fragments; this contradiction vanishes if we recall that the Parikh image of L is not equal to the complement of the Parikh image of L and the Parikh image of the intersection of two CFLs is not equal to the intersection of the Parikh images of the languages. Hence, only isolated CFL-constraints (without other language-based constraints) can be safely replaced by arithmetical constraints.

Preliminaries

In this section, we recall the extended modal logic EML and we present extensions based on CFLs. In particular, we shall recall what VPLs are.

Extended Modal Logic EML

The logics studied in this paper extend the logic EML that has Presburger and regularity constraints. Given a countably infinite set AT = {p 1 , p 2 , . . . } of propositional variables, the set of terms and EML formulae is inductively defined as follows

t ::= a × ϕ | t + a × ϕ ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | t > b | t ≡ k c | L(ϕ 1 , . . . , ϕ n ) where • b, c ∈ N, k ∈ N \ {0, 1}, a ∈ Z \ {0}.
• L is any regular language specified by a finite-state automaton.

A model for EML is a structure T, R, (< s ) s∈T , l where T is the (possibly infinite) set of nodes and R ⊆ T 2 such that the set {t ∈ T : s, t ∈ R} is finite for each s ∈ T . Each relation < s is a total ordering on the R-succesors of s and l : T → 2 AT is the valuation function. We write R(s) = s 1 < • • • < s m if the children of s are s 1 , . . . , s m and they are ordered this way. The satisfaction relation is inductively defined as follows (we omit Boolean clauses):

• M, s |= p iff p ∈ l(s), • M, s |= i a i ϕ i ≡ k c iff there is n ∈ N such that i a i R ϕi (s) = nk + c with R ϕi = { s , s ∈ T 2 : s , s ∈ R, and M, s |= ϕ i } and R ϕi (s) = card(R ϕi (s)), • M, s |= i a i ϕ i > b iff i a i R ϕi (s) > b,
• M, s |= L(ϕ 1 , . . . , ϕ n ) iff the finite sequence of children of the node s induces a finite pattern from L. More precisely, iff there is

a i1 • • •a im ∈ L such that given the children of s, R(s) = s 1 < • • • < s m , for every j ∈ [1, m], we have M, s j |= ϕ ij (L is any regular language).
A formula ϕ is satisfiable iff there is a model M and a node s such that M, s |= ϕ. The satisfiability problem is defined accordingly. Observe that although arithmetical constraints are only allowed to use >, the operators {=, <, } can be easily defined using Boolean combinations and constants (no exponential blow-up occurs if renaming is used). Hence, we will use them as abbreviations.

Modalities from K and graded modal logic can also be defined in EML. We use the abbreviation 2ϕ def = ¬( ¬ϕ > 0). Despite the fact that EML extends graded modal logics with richer arithmetical constraints but also with regularity constraints, the satisfiability problem for EML is pspace-complete [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]. Now, let us recall what formula trees are. They will be used to define the different fragments that we will be working with. A finite tree T is a finite subset of (N \ {0}) * such that ε ∈ T and if s•i ∈ T , then s ∈ T and s•j ∈ T for j ∈ [1, i -1]. The nodes of T are its elements. The root of T is the empty word ε. All notions such as parent, child, subtree and leaf, have their standard meanings. A formula tree is a labelled tree T , representing a formula ϕ (the label set being a set of subformulae), i.e. EML formulae are encoded as formula trees and occurrences of ψ in ϕ correspond to nodes of the formula tree for ϕ that are labelled by ψ. Given a formula tree T , , we define its polarity tree T , POL as follows:

• (ε) = ϕ. If (s) = ψ 1 ⊕ ψ 2 with ⊕ ∈ {∨,
Intuitively, this last definition assigns the modal-arithmetical depth to the subformula in each node. By way of example, we present the formula tree for ¬( p > 3) ∨ ¬L(p, q) together with its polarity tree and its depth tree.

ε 1 2 2•1 2•1•1 2•1•2 1•1 1•1•1 ¬( p > 3) ∨ ¬L(p, q) ¬( p > 3) ¬L(p, q) L(p, q) p q ( p > 3)

Extensions with CFL-constraints

Let us briefly fix some notations about pushdown automata. A pushdown automaton (denoted by PDA) M is a tuple Q, Σ, Γ, δ, q 0 , ⊥, F where Q is a finite set of states, Σ (resp. Γ) is the finite input (resp. stack) alphabet, δ is a mapping of Q × (Σ ∪ {ε}) × Γ into finite subsets of Q × Γ * , q 0 ∈ Q is the initial state, ⊥ is the initial stack symbol, F ⊆ Q is the set of accepting states. A configuration q, α, γ is an element of Q × Σ * × Γ * . Initial configurations are of the form q 0 , ε, ⊥ . The one-step relation (with respect to M ) between configurations is defined as follows: q, α, bγ q , αa, γ γ whenever there is q , γ ∈ δ(q, a, b). As usual, * is the reflexive and transitive closure of . We write L(M ) to denote the language accepted by the pushdown automaton M when acceptance is by final states, i.e. L(M ) = {α ∈ Σ * : q 0 , ε, ⊥ * q, α, γ with q ∈ F }.

A pushdown alphabet Σ is an alphabet equipped with a partition Σ c , Σ i , Σ r such that the letters in Σ c are calls (corresponding to push actions on the stack), the letters in Σ i are internal actions (no action on the stack) and the letters in Σ r are returns (corresponding to pop actions on the stack). A visibly pushdown automaton (VPA) over Σ is defined as a PDA except that the input letters in Σ determine which actions are performing on the stack according to the partition Σ c , Σ i , Σ r . More precisely, a VPA M over a pushdown alphabet Σ c , Σ i , Σ r is a PDA without ε-transitions and such that for all states q, input symbols a ∈ Σ and stack symbols b ∈ Γ,

• a ∈ Σ c and q , γ ∈ δ(q, a, b) imply γ = b b for some b ∈ Γ (call),

• a ∈ Σ i and q , γ ∈ δ(q, a, b) imply γ = b (internal action),

• a ∈ Σ r and q , γ ∈ δ(q, a, b) imply γ = ε (return).

A visibly pushdown language (VPL) is a language accepted by a VPA. By [START_REF] Alur | Visibly pushdown languages[END_REF], given two VPLs L 1 and L 2 over the same pushdown alphabet Σ, L 1 ∪L 2 , L 1 ∩L 2 and Σ * \ L 1 are also VPLs and one can effectively compute the corresponding VPA.

Given a class C of languages (made of finite words from finite alphabets), we define the modal logic EML(C) interpreted over finitely-branching Kripke structures such that EML(C) is an extension of EML by allowing formula L(ϕ 1 , . . . , ϕ n ) with L ∈ (C ∪ REG) where REG is the class of regular languages. In this paper, C is either the class of context-free languages (denoted by CFL) or the class of visibly pushdown languages (denoted by VPL). Of course, elements of C need to be represented finitely; to do so, when L ∈ CFL, L is specified either by a PDA or by a context-free grammar (CFG). Moreover, when L ∈ VPL, L is specified by a VPA. Obviously, EML = EML(REG). Let EML i (C) be the set of formulae ϕ in EML(C) such that for any depth j in its depth tree, there are at most i nodes labelled by formulae of the form L(

• • •) with L ∈ C. For example, L 1 (p, q) ∧ L 2 (p, q) ∧ ¬L 3 (p, q) ∈ EML 1 (CFL) with L 1 , L 2 ∈ REG and L 3 ∈ CFL.

Properties expressible in EML(CFL)

It is obvious that EML(CFL) is at least as expressive as EML. However, the fact that there are context-free languages that are not regular is not sufficient to conclude that EML(CFL) is strictly more expressive than EML since the languages are embedded in a logical context. In fact, in Section 3, we show that EML(VPL) is as expressive as EML(CFL) even though VPL is strictly included in CFL. In the paragraphs below, we explore the relationships between properties expressible in EML and those expressible in EML(CFL). Towards the end of the section, we finally show that EML(CFL) is strictly more expressive.

Let us express in EML(CFL) that there are no children of distance exactly 2 N +1 such that the first child satisfies p and the second one satisfies q. This property can be instrumental for reducing tiling problems and, with it, establish complexity lower bounds. Let L be the language defined by the context-free grammar below (S is the axiom):

S → T aS N S N bT, T → c, T → T T, T → ε, S N → S N -1 S N -1 , S N → S N -1 S N -1 , • • • , S 2 → S 1 S 1 , S 2 → S 1 S 1 , S 1 → cc, S 1 → c
One can check that ¬L(p, q, ) whenever there are no children of distance exactly 2 N +1 such that the first child satisfies p and the second one satisfies q. Note that L is a regular language (even though it is defined with a CFG) and therefore such a property can be also expressed in EML. However, this can be done much more succinctly in EML(CFL) since the context-free grammar is of linear size in N . So, we can conclude that EML(CFL) is at least a succinct version of EML.

Now, let us turn to a genuine context-free property: the sequence of children can be divided into two sequences of equal cardinality such that every child of the first part satisfies p and every child of the second part satisfies q which is a quite natural property to express. In EML(CFL), this statement can be expressed by L(p ∧ ¬q, q ∧ ¬p) with the context-free language L = {a i b i : i ∈ N} However, it is not difficult to show that the formula ( p = q)∧L (p∧¬q, q ∧¬p) in EML can also express exactly the same property where L = a * b * . In a sense, formulae in EML(CFL) can be viewed as macros for formulae from EML. This is analogous to the situation in modal logic K for which we may consider only one of the operators 2 and 3 or both in order to make the formulae clearer. So, EML(CFL) is at least a more friendly version of EML.

The key question remains whether EML(CFL) is strictly more expressive than EML. By generalizing the above reasoning, one can show that contextfree constraints of the form L(• • •) can be expressed in EML if there are a formula ψ from PrA and a regular language L such that for every α ∈ Σ * , we have α ∈ L iff the Parikh image of α satisfies ψ and α ∈ L . Note that {a i b i : i ∈ N} precisely satisfies this condition. Such context-free languages L definable by a Presburger formula and by a regular language are exactly the context-free languages definable by so-called Parikh automata, see e.g. [START_REF] Cadilhac | On the expressiveness of Parikh automata and related models[END_REF].

The constraints on children that are expressible in EML are Boolean combinations of arithmetical constraints and regular constraints. Such formulae can be reduced equivalently to a disjunction such that each disjunct is a conjunction made of a Boolean combination of arithmetical constraints and made of a regular constraint of the form A(• • •). Indeed, a conjunction of positive or negative regular constraints can be equivalently turned into a single regular constraint. Hence, EML(CFL) is strictly more expressive than EML if there is a context-free language that cannot be recognized by a Parikh automaton. Let us consider the language L REV = {αcα rev : α ∈ {a, b}} where α rev is the reverse of α. For instance L REV (p ∧ ¬q ∧ ¬r, q ∧ ¬p ∧ ¬r, r ∧ ¬p ∧ ¬q) roughly states that the sequence of children can be divided into three parts such that the sequence of the first part is the mirror image of the sequence of the third part and the second part is reduce to a single child satisfying r ∧ ¬p ∧ ¬q. By adapting the proof of [8, Proposition 3], one can show that L REV is a context-free language that is not definable by a Parikh automaton and therefore EML(CFL) is stricly more expressive that EML, which is after all not a big surprise.

On the Expressive Power of EML(VPL)

We show that the logic EML(VPL) has the same expressive power as EML(CFL). It is clear that every VPL is a CFL and therefore EML(CFL) is at least as expressive as EML(VPL). For the other direction, we state that every CFL L over an alphabet Σ can be transformed into a VPL L over the pushdown alphabet Σ × {c}, Σ × {i}, Σ × {r} such that π 1 (L ) = L where π 1 is the projection over the first component, i.e. π 1 erases the second component whose value is among {c, i, r}. With this 'embedding' we will be able to show that EML(VPL) is as expressive as EML(CFL) using a truth-preserving reduction.

Theorem 3.1 ([2, Theorem 5.2]) For any CFL L over the alphabet Σ, we can effectively build a VPA M over the alphabet Σ M = Σ×{c}, Σ×{i}, Σ×{r} such that for all α ∈ Σ * , we have α ∈ L iff there is α ∈ L(M ) s.t. π 1 (α ) = α.

Proof. Let M = Q, Σ, Γ, q 0 , δ, ⊥, F be a PDA such that L(M ) = L. Without loss of generality we can also assume that (i) no ε-transitions are used and (ii) the net effect (on the stack) of any transition is null or it pushes or pops one symbol. Define the VPA M = Q, Σ M , Γ, q 0 , δ , ⊥, F with Σ M = Σ×{c}, Σ×{i}, Σ×{r} such that δ is the minimum relation satisfying

for every transition q → q in M there is a transition q → q in M reading w/stack top action reading w/stack top pushing Call a b push b a, c b b b Return a b pop b a, r b ε Internal a b - a, i b b
Intuitively, we simulate the associated PDA by annotating the input word with information on how the stack is managed. The proof follows from the fact that there is a 1-to-1 correspondence between the transitions of M and M . 2

Now we can show that the fragment EML(VPL) is at least as expressive as EML(CFL). This result is surprising because, as we said before, the class of VPLs is strictly included in the class of CFLs. To prove this claim, we give a truth-preserving translation T : EML(CFL) → EML(VPL) defined inductively over the terms and formulae. T is defined homomorphically for all Boolean connectives; arithmetical and periodicity constraints are translated as

T(t > b) def = T(t) > b, T(t ≡ k c) def = T(t) ≡ k c and the terms are defined as fol- lows T(a × ϕ) def = a × T(ϕ), T(t + a × ϕ) def = T(t) + a × T(ϕ).
The translation is handled differently for regular and context-free languages.

T(L(ϕ1, . . . , ϕn))

def = L(T(ϕ1), . . . , T(ϕn)) if L ∈ REG T(L(ϕ1, . . . , ϕn)) def = L (T(ϕ1), T(ϕ1), T(ϕ1), . . . , T(ϕn), T(ϕn), T(ϕn)) if L ∈ CFL.
where L is a VPL built thanks to Theorem 3.1. Note that this is only needed if L is a CFL (hence represented by a PDA) whereas when L is in REG, the translation is homomorphic. The different numbers of arguments are due to the fact that the cardinal of the alphabet of M is equal to three times the cardinal of Σ. Assuming that the alphabet of M is grouped by their first component, the above translation assigns the same formula to symbols sharing the same first component. So, T(ϕ) can be effectively computed from ϕ. Moreover, an exponential blow-up is observed if formulae are encoded as formula trees, unlike the case when formulae are encoded as directed acyclic graphs. Proof. We prove the result by structural induction. The base case as well as the cases in induction step for Boolean connectives, regularity constraints and arithmetical constraints are by an easy verification. We focus on the remaining case with context-free constraints.

Left to right: Suppose that M, s |= L(ϕ 1 , . . . , ϕ n ) and the alphabet of L is Σ = {a 1 , . . . , a n }. There is a word α = a j1 . . . a jm ∈ L and children s 1 , . . . , s m such that s i |= ϕ ji for i ∈ [1, m]. Using the properties satisfied by L ∈ VPL, we know that there is α ∈ L such that π 1 (α ) = α. It is enough to show that for all i, if π 1 (α (i)) = a j then s i |= T(ϕ j ) and this is clearly satisfied by M by induction hypothesis.

For the other direction, suppose that M, s |= T(L(ϕ 1 , . . . , ϕ n )). Hence, there exist α ∈ L and children s 1 , . . . , s m . Using again the properties satisfied by L ∈ VPL, it is clear that π 1 (α ) ∈ L. Observe also that any child s j k corresponding to a symbol (a j k , action) satisfies s j k |= T(ϕ j k ). With this observation we conclude, by induction hypothesis, that s 1 , . . . , s m satisfy the needed formulae and thus M, s |= L(ϕ 1 , . . . , ϕ n ).

2

Observe that the translation T preserves the number of context-free constraints at each depth. Furthermore, polarity of the subformulae is preserved. Consequently, we can state the following result for several fragments. The exponential blow-up in T for EML(CFL) formulae can be avoided using the renaming technique, whence by introducing new propositional variables. The formula and its translation would not be logically equivalent but they would be equi-satisfiable. Theorem 3.3 states relationships between fragments that will have an important impact on the expressive power and decidability of the logic EML(VPL). Recall that the class of VPLs forms a Boolean algebra and they behave nicely with other logics. Hence, we expected to be able to get numerous positive decidability results as well. From Theorem 3.3, we can conclude that adding VPLs to EML is as powerful as adding the full class of CFLs. In the forthcoming section, we investigate the decidability status of several extensions of EML with CFL-constraints or VPL-constraints.

Undecidable Extensions of Presburger Modal Logics

We start by extending EML with CFLs and VPLs and show that they are already undecidable when we allow two positive language constraints to appear simultaneously. Moreover, we show that if we allow negative occurrences of language constraints, we already get undecidability with just one language constraint.

Undecidability of WEML + 2 (CFL). Let WEML + 2 (C) be the fragment of EML 2 (C) defined as the restriction of the set of formulae specified by

ϕ ::= p | ¬p | ϕ ∧ ϕ | L(ψ 1 , . . . , ψ n )
where L ∈ C, ψ i are propositional formulae and ϕ has at most two language constraints from C.Observe that this fragment does not include arithmetical constraints.

Theorem 4.1 The satisfiability problem for WEML + 2 (CFL) is undecidable. Proof. The proof is by reduction from the nonemptiness problem for the intersection of CFLs. Let L 1 , L 2 be two CFLs. We assume that both languages share the same alphabet Σ = {a 1 , . . . , a n } (if it is not the case, we take Σ as the union of their alphabets). Let ϕ i be a formula stating that p i is the only propositional variable holding among {p 1 , . . . , p n }.

Let ψ = L 1 (ϕ 1 , . . . , ϕ n ) ∧ L 2 (ϕ 1 , . . . , ϕ n ). We prove that ψ is satisfiable iff L 1 ∩ L 2 = ∅.
For the 'if' direction suppose that M, s |= ψ and there exist a sequence of children s 1 , . . . , s k and words

α 1 ∈ L 1 , α 2 ∈ L 2 such that |α 1 | = |α 2 | = k. Let w 1 = a i1 . . . a i k and w 2 = a j1 . . . a j k . Note that for ∈ {1, 2}, α (i) = a j iff s i |= p j .
As only one propositional variable can be true of a given child then we can conclude that α 1 = α 2 and therefore L 1 ∩ L 2 = ∅. For the 'only if' direction: Let α ∈ L 1 ∩ L 2 and |α| = k. Take the model M, s with children s 1 , . . . , s k such that s i |= p j iff α(i) = a j . It is easy to check that this model satisfies ψ.

2

Undecidability of EML 2 (VPL). We show that the satisfiability problem for EML(VPL) is undecidable. Moreover, the EML 2 (VPL) fragment is already undecidable. In contrast with CFLs, there is one more parameter to be taken into account in our analysis: every VPL is defined over a pushdown alphabet. Therefore, given many VPLs occurring in a formula, we analyze how the relationship among their partitions relates to the undecidability result.

Corollary 4.2

The satisfiability problem for WEML + 2 (VPL) is undecidable, even restricted to formulae such that every two distinct VPLs occurring at the same depth share the same pushdown alphabet.

Proof. Undecidability is by reduction from the satisfiability problem for the fragment WEML + 2 (CFL) (see Theorem 4.1). Given a formula ϕ ∈ WEML + 2 (CFL), we can use the translation T to obtain a formula T(ϕ) in WEML + 2 (VPL). By truth-preservation of T, we obtain that the satisfiability problem for WEML + 2 (VPL) is undecidable. Observe that we can always assume that for ϕ ∈ WEML + 2 (CFL), if two distinct context-free languages occur at the same modal depth, then they share the same pushdown alphabet. In this way, we get a translation T(ϕ) in the fragment mentioned in the statement of the theorem.

2

Considering T, the translation of a CFL provides the same pushdown alphabet and formula arguments. One could argue that it is exactly this connection through the pushdown alphabet that allows us to encode the nonemptiness problem for the intersection of CFLs. In the following theorem we show that, even if the VPLs do not share the pushdown alphabet, we can still encode the same problem using propositional variables that play the role of 'binders'.

Theorem 4.3

The satisfiability problem for WEML + 2 (VPL) is undecidable even restricted to formulae such that every two distinct VPLs occuring at the same modal depth do not share the pushdown alphabet.

Proof. Let L 1 , L 2 be CFLs over the alphabet Σ. By Theorem 3.1, one can build two VPA M 1 and M 2 over the pushdown alphabet Σ × {c}, Σ × {i}, Σ × {r} such that for all words α ∈ Σ * , we have [START_REF] Alur | Visibly pushdown languages[END_REF]

α ∈ L 1 iff there is α ∈ L(M 1 ) such that π 1 (α ) = α and (2) α ∈ L 2 iff there is α ∈ L(M 2 ) such that π 1 (α ) = α.
Let Σ 1 and Σ 2 be two distinct alphabets of cardinality 3 × card(Σ) with Σ 1 ∩ Σ 2 = ∅ and, σ 1 : Σ × {c, r, i} → Σ 1 and σ 2 : Σ × {c, r, i} → Σ 2 be two bijective renamings. Recall that VPLs are closed under renamings and one can easily compute VPA M 1 and M 2 such that L(M 1 ) = σ 1 (L(M 1 )) and L(M 2 ) = σ 2 (L(M 2 )). Note that M 1 and M 2 are defined over distinct pushdown alphabets. Again, for all words α ∈ Σ * , we have [START_REF] Alur | Visibly pushdown languages[END_REF]

α ∈ L 1 iff there is α ∈ L(M 1 ) such that π 1 (σ -1 1 (α )) = α and (2 ) α ∈ L 2 iff there is α ∈ L(M 2 ) such that π 1 (σ -1 2 (α )) = α. Let Σ = {a 1 , . . . , a n }, Σ 1 =
{s 1 , . . . , s 3n } and Σ 2 = {s 1 , . . . , s 3n }. Let ϕ i be a formula that states that the only propositional variable true among {p 1 , . . . , p 3n } at a given node is p i . We define a function which identifies each symbol from the original alphabet Σ with a propositional variable. Let g : Σ × {c, r, i} → {ϕ 1 , . . . , ϕ 3n } be defined as g((a i , action)) = ϕ i and let

θ i j = g(σ -1 i (s j )) then we define ψ = L(M 1 )(θ 1 1 , . . . , θ 1 3n ) ∧ L(M 2 )(θ 2 1 , . . . , θ 2 3n
). It is easy to prove that ψ is satisfiable iff L(M 1 ) ∩ L(M 2 ) = ∅ using an argu-ment similar to that of Theorem 4.1. We conclude that L 1 ∩ L 2 = ∅ iff ψ is satisfiable.

2

Undecidability of WEML - 1 (CFL). Let WEML - 1 (CFL) be the restriction of EML 1 (CFL) defined as a fragment specified by

ϕ ::= p | ¬p | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬L(p 1 , . . . , p n ) | 2ψ
where L ∈ CFL, ψ is a propositional formula and ϕ has at most one contextfree constraint. Given a CFL L over the alphabet Σ = {a 1 , . . . , a k }, we build a formula ϕ L in WEML - 1 (CFL) such that L = Σ * iff ϕ L is satisfiable. Since the universality problem for CFLs is undecidable (see e.g. [START_REF] Ibarra | Restricted one-counter machines with undecidable universe problems[END_REF]) we conclude that the satisfiability problem for WEML - 1 (CFL) is undecidable too. Let ϕ uni (p 1 , . . . , p k ) be a formula in WEML - 1 (CFL) enforcing that any child satisfies exactly one propositional variable among {p 1 , . . . , p k }, we define

ϕ L = ϕ uni (p 1 , . . . , p k ) ∧ ¬L(p 1 , . . . , p k ) Theorem 4.4 The satisfiability problem for WEML - 1 (CFL) is undecidable. Proof. First, suppose that L = Σ * ; hence there is a word w = a i1 • • • a in / ∈ L.
Let us consider the model M with a root node s and children

s 1 < • • • < s n such that for every j ∈ [1, n], s j |= ϕ ij . It is clear that M, s |= ϕ uni (p 1 , . . . , p k ).
The crucial observation is that, given a model where exactly one propositional variable holds at each child, forming the sequence p i1 , . . . , p in then M, s |= L(p 1 , . . . , p k ) iff a i1 • • • a in ∈ L. Hence, M, s |= ¬L(p 1 , . . . , p k ). Now suppose that there is a model M and a node s such that M, s |= ϕ L . If s has no successor, then / ∈ L, otherwise M, s |= L(p 1 , . . . , p k ). In that case L = Σ * . Now suppose that s has children s 1 < . . . < s n with n 1. As before, the propositional variables true at the children form a sequence p i1 , . . . , p in and M, s |= L(p 1 , . . . , p k ) iff a i1 • • • a in ∈ L. Therefore there exists a word

a i1 • • • a in / ∈ L which implies L = Σ * . 2
As a corollary, the satisfiability problem for EML - 1 (VPL) is undecidable too.

Decidability of EML + 1 (CFL)

We saw that it is enough to have two positive occurrences (i.e., with nonzero polarity) of CFL-constraints or one negative occurrence (i.e., with zero polarity) of a CFL-constraint to have an undecidable satisfiability problem. It remains one interesting extension of EML to be studied: let EML + 1 (CFL) be the fragment in which there is at most one CFL-constraint at each depth, occurring positively. EML + i (C) is defined as the subset of EML i (C) such that every formula's tree node labelled by a formula of the form

1. L(• • •) with L ∈ C has a positive polarity,

2.

i a i ϕ i > b with a positive polarity has all a i , b > 0 or all ϕ i ∈ EML(REG), 3.

i a i ϕ i > b with a negative polarity has each ϕ i ∈ EML(REG),

4.

i a i ϕ i ≡ k c has ϕ i ∈ EML(REG). For example, L 3 (p, q) ∧ L 1 (L 3 (p, q), q) ∈ EML + 1 (CFL) with L 1 ∈ REG, L 3 ∈ CFL. We show that the satisfiability problem for EML + 1 (CFL) is decidable, which is the main decidability result of the paper. Even though the above definition has been finely tailored for our proof to work, we think that it is probably the only potentially interesting fragment left to be analyzed. Nonetheless, this fragment adds extra power over EML: suppose you have an XML file containing 'buy' and 'sell' records. With EML + 1 (CFL) you can require that for every 'sell' there is a matching 'buy' record before it whereas that cannot be done in EML.

We provide a decision procedure for EML + 1 (CFL) generalizing the one for EML [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]. A major difference is that we have to deal with CFL-constraints with a fine-tuned procedure. Whereas EML satisfiability is in pspace, our algorithm for EML + 1 (CFL) requires strictly more space since we need to store the stack content which can be of double exponential length in the worst-case, preventing us from using an on-the-fly algorithm as done for EML. Our decidability result is established thanks to a Ladner-like algorithm [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] (see also [START_REF] Spaan | The complexity of propositional tense logics[END_REF][START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]). The original algorithm from [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] allows to show that the satisfiability problem for modal logic K is in pspace and it can be viewed as a tableaux-like procedure with non-determinism but without tableaux rules. The beauty of Ladner-like algorithms rests on their simple structure with fine-tuned recursivity; moreover it does not use any specific formalism such as tableaux, automata, sequents etc. Our algorithm below extends the one presented in [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF] for the satisfiability of the basic EML. We start by defining the closure for finite sets of formulae. Intuitively, the closure cl(X) of X contains all formulae useful to evaluate the truth of formulae in X. Definition 5.1 Let X be a finite set of formulae, cl(X) is the smallest set satisfying

• X ⊆ cl(X), cl(X) is closed under subformulae,

• if ψ ∈ cl(X), then ¬ψ ∈ cl(X) (we identify ¬¬ψ with ψ),

• let K be the least common multiple (lcm) of all the constants k occurring in subformulae of the form t

≡ k c. If t ≡ k c ∈ cl(X), then t ≡ K c ∈ cl(X) for every c ∈ [0, K -1].
Observe that, since EML + 1 (CFL) is not closed under negation, formulae in cl(X) may not belong to EML + 1 (CFL) even if X is a set of EML + 1 (CFL) formulae. A set X of formulae is said to be closed iff cl(X) = X. We refine the notion of closure by introducing a new parameter n: each set cl(n, ϕ) is a subset of cl({ϕ}) that corresponds to a closed set obtained from subformulae of depth n. We have cl(0, ϕ) ⊇ cl(1, ϕ) ⊇ cl(2, ϕ) • • • and the sets are defined by peeling of modalities layer by layer.

Definition 5.2 Let ϕ ∈ EML + 1 (CFL); for n ∈ N, cl(n, ϕ) is the smallest set such that • cl(0, ϕ) = cl({ϕ}), for every n ∈ N, cl(n, ϕ) is closed,
• for all n ∈ N and ψ occurring in some formula of cl(n, ϕ), ψ ∈ cl(n + 1, ϕ),

• for all n ∈ N and L(ϕ 1 , . . . , ϕ m ) ∈ cl(n, ϕ), then {ϕ 1 , . . . , ϕ m } ⊆ cl(n + 1, ϕ).

We will concentrate on subsets of cl(n, ϕ) whose conjunction of elements is EML + 1 (CFL) satisfiable. A necessary condition to be satisfiable is to be consistent locally, i.e. at the propositional level and at the level of arithmetical constraints. Let K be the lcm of all the constants k occurring in subformulae of ϕ of the form t ≡ k c. Definition 5.3 A set X ⊆ cl(n, ϕ) is said to be n-locally consistent iff:

• if ¬ψ ∈ cl(n, ϕ), then ¬ψ ∈ X iff ψ ∈ X, • if ψ 1 ∧ ψ 2 ∈ cl(n, ϕ), then ψ 1 ∧ ψ 2 ∈ X iff ψ 1 , ψ 2 ∈ X, • if ψ 1 ∨ ψ 2 ∈ cl(n, ϕ), then ψ 1 ∨ ψ 2 ∈ X iff ψ 1 ∈ X or ψ 2 ∈ X, • if t ≡ k c ∈ cl(n, X), then there is a unique c ∈ [0, K-1] such that t ≡ K c ∈ X, • if t ≡ k c ∈ cl(n, X), then ¬t ≡ k c ∈ X iff there is c ∈ [0, K -1] such that t ≡ K c ∈ X and not c ≡ k c,
The kernel of an n-locally consistent set X is ker(X) = X ∩ EML + 1 (CFL). As we have observed, the closure operation may introduce formulae outside EML + 1 (CFL). Negation of EML formulae is not a problem (since they are also in EML) whereas negation of EML + 1 (CFL) formulae may lead to undecidability (e.g., because of a negative polarity). That is why, in our algorithm, we shall only try to satisfy formulae from ker(X) and this shall be sufficient from the way the fragment EML + 1 (CFL) is designed. A slight variation in the definition of EML + 1 (CFL) may lead to undecidability of the satisfiability problem. Regarding size, observe that card(cl(X)) is exponential in card(X). Nevertheless, consistent sets of formulae that are satisfiable contain exactly one formula from the set {t ≡ K c : c ∈ [0, K -1]} for each constraint t ≡ k c in X. Hence, as explained in [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF], encoding consistent sets will only require polynomial space. Definition 5.4 Let ϕ be an EML + 1 (CFL) formula, N be a natural number and M be a finite tree model such that M, s |= ϕ for some node s. We say that M, s is N -bounded for ϕ iff for every node s of distance d from s, the number of successors of s is bounded by nb(d + 1) × N where nb(d + 1) is the number of distinct (d + 1)-locally consistent sets (with respect to ϕ).

We define the function SAT (see below) such that ϕ is EML + 1 (CFL) satisfiable in some N -bounded model iff there is X ⊆ cl(0, ϕ) such that ϕ ∈ ker(X) and SAT(X, 0) has a computation returning true. Indeed, the function SAT(X, d) is globally parameterized by some natural number N and by the formula ϕ. These two parameters should be understood as global variables. The main difference with the algorithm in [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF] is related to the update of the stack and we restrict ourselves to formulae in ker(X).

function SAT(X, d) (consistency) if X is not d-locally consistent then abort; (base case) if X contains only propositional formulae then return true; (initialization-counters) for every ψ ∈ ker(cl(d + 1, ϕ)) that is not a periodicity constraint of the form t ≡K c, C ψ := 0; (initialization-fsa) for every FSA A(ψ1, . . . , ψα) ∈ ker(X), the state variable q A(ψ 1 ,...,ψα) := q0 for some initial state q0 of A; (initialization-fsa-complement) for every FSA ¬A(ψ1, . . . , ψα) ∈ ker(X), Z ¬A(ψ 1 ,...,ψα) := I where I is the set of initial states of A; (initialization-pda) for every CFL-constraint C(ψ1, . . . , ψα) ∈ ker(X) where C is a PDA, the state variable q C(ψ 1 ,...,ψα) := q0 for some initial state q0 of C and the stack variable S C(ψ 1 ,...,ψα) := ⊥ for the initial stack symbol ⊥ of C; (guess-number-children) guess NB in {0, . . . , nb(d + 1) × N }; (guess-children-from-left-to-right) for i = 1 to NB do (i) guess x ∈ {1, . . . , nb(d + 1)};

(ii) if not SAT(Yx, d + 1) then abort;

(iii) for every ψ ∈ ker(cl(d+1, ϕ)) different from some t ≡K c such that ψ ∈ Yx do C ψ := C ψ + 1; (iv) for every finite state automaton A(ψ1, . . . , ψα) ∈ ker(X), a. guess a transition q A(ψ 1 ,...,

-→ q in A with ΣA = a1, . . . , aα; b. if ψi ∈ Yx, then q A(ψ 1 ,...,ψα) := q , otherwise abort; (v) for every finite state automaton ¬A(ψ1, . . . , ψα) ∈ ker(X), Z ¬A(ψ 1 ,...,ψα) := {q : ∃ q ∈ Z ¬A(ψ 1 ,...,ψα) , q a i -→ q, ψi ∈ Yx}; (vi) for every CFL-constraint C(ψ1, . . . , ψα) ∈ ker(X), a. let S C(ψ 1 ,...,ψα) = b1 . . . b k be the stack content of C, guess a transition q C(ψ 1 ,...,ψα) a i -→ q poping b1 and pushing γ in C with ΣC = a1, . . . , aα; b. if ψi ∈ Yx, then q A(ψ 1 ,...,ψα) := q and S C(ψ 1 ,...,ψα) := γb2 . . . b k , otherwise abort;

(final-checking) (i) for every i ai ψi ∼ b ∈ X, if i ai × C ψ i ∼ b does not hold, then abort, (ii) for every i ai ψi ≡ k c ∈ X, if i ai × C ψ i ≡ k c does not hold, abort, (iii)
for every (either finite-state or pushdown) automaton A(ψ1, . . . , ψα) ∈ X, if q A(ψ 1 ,...,ψα) is not a final state of A, then abort; (iv) for every FSA ¬A(ψ1, . . . , ψα) ∈ X, if Z ¬A(ψ 1 ,...,ψα) contains a final state of A, then abort; (return-true) return true.

We shall later fix N which will be doubly exponential in |ϕ| (see Lemma 5.9). The first argument X is intended to be a subset of cl(d, ϕ) and the (d + 1)locally consistent sets are denoted by Y i for some 1 i nb(d + 1). A call to SAT(X, d) performs the following actions. First it checks whether X is dlocally consistent and if the modal degree is zero, then it returns true in case of d-locally consistency. In order to check that ker(X) is satisfiable, children of the node are guessed from left to right (providing an ordering of the successors). For each ψ ∈ ker(X), there is a counter C ψ which contains the current number of children that should satisfy ψ. Similarly, we keep track of periodicity constraints. For each subformula in ker(X) whose outermost connective is automata-based, we introduce a variable that encodes the current state and stack content. At the end of the guess of the children, this variable should be equal to a final state of the automaton. By contrast, for each formula in ker(X) whose outermost connective is the negation of some automata-based formula, we introduce a variable that encodes the set of states that could be reached so far in the automaton (simulating a subset construction of the underlying automaton). We never have a negation of a CFL-constraint. At the end of the guess of the children, this variable should not contain any final state of the automaton. After guessing at most N × nb(d + 1) children, there is a final checking which verifies that periodicity and arithmetical constraints are satisfied. Keeping track of the stack may hurt a lot, i.e., the resulting size could be linear on the number of children. Therefore, of exponential space. Lemma 5.5 For all 0-locally consistent sets X and computations of SAT(X, 0) (i) the recursive depth is linear in |ϕ|, (ii) each call requires space polynomial in the sum of the space for encoding 0-locally consistent sets and N + 2 |ϕ| , Proof. Since cl(|ϕ|, ϕ) = ∅, the size of the stack of recursive calls to SAT is at most |ϕ|.

In the function SAT, the steps (consistency), (base case), (initialization-counters), (initialization-fsa), (initialization-fsacomplement) and (initialization-pda) can be obviously checked in polynomial time in ϕ (and therefore in polynomial space). Indeed, every n-locally consistent set has cardinal at most 2 × |ϕ| and can be encoded with a polynomial amount of bits with respect of |ϕ|; moreover given X ⊆ cl(0, ϕ) of cardinal at most 2 × |ϕ| and n ∈ N, one can decide in polynomial-time in |ϕ| whether X is n-locally consistent. In the step (guess-children-from-left-to-right), one needs a counter to count at most until nb(d + 1) × N . A polynomial amount of bits in |ϕ| + log(N ) suffices. All the non-recursive instructions in (guess-childrenfrom-left-right) can be done in time polynomial in |ϕ| + log(N ). Since at the end of the step (guess-children-from-left-right), the values of the counters are less than or equal to nb(d + 1) × N , checking the points (i) and (ii) in (finalchecking) can be done in polynomial space in |ϕ| + log(N ) (remember that the encoding of constants a i , b and c and k are already in linear space in |ϕ|). The only variables that requires polynomial space in 2 |ϕ| + N are those containing stack contents since the number of children N B is bounded by nb(d + 1) × N .2 An analogous of [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]Lemma 5] is shown below. Lemma 5.6 Let X ⊆ cl(0, ϕ), if SAT(X, 0) has successful computation and ϕ ∈ ker(X), then ϕ is EML + 1 (CFL) satisfiable in an N -bounded model. Proof. Assume that SAT(X, 0) has an accepting computation with ϕ ∈ ker(X). Let us build a model M = T, R, (< s ) s∈T , l for which there is s ∈ T such that for every ψ ∈ ker(X) we have M, s |= ψ.

From an accepting computation of SAT(X, 0), we consider the following finite ordered tree T, R, (< s ) s∈T , that corresponds to the calls tree of SAT(X, 0).

• T, R, (< s ) s∈T is a finite ordered tree, • for each s ∈ T , (s) = Y, d for some d-consistent set Y ,

• the root node s 0 is labelled by X, 0 ,

• for each node s with s 1 < s • • • < s s n , the call related to (s) recursively calls SAT with the respective arguments (s 1 ), . . . , (s n ) and in this very ordering.

The model M we are looking for, is precisely M = T, R, (< s ) s∈T , l for which l(s) = Y ∩ AT where (s) = Y, d for each s.

By structural induction on ψ, we shall show that for all s ∈ T with labeling (s) = Y, d we have, ψ ∈ ker(Y ) implies M, s |= ψ. Consequently, we then get M, s 0 |= ϕ. The case when ψ is a propositional variable is by definition of l. Suppose s has children s 1 , . . . , s NB such that (s i ) = Y xi , d + 1 . Given an arbitrary word γ = ψ j1 . . . ψ jNB ∈ L suppose that ψ ji ∈ Y ji for all i. In this case the step (guess-children-from-left-to-right) would finish with a set of states including a final state and therefore (final-checking) would abort. Hence, there exists ψ j k / ∈ Y j k . By the definition of n-locally consistent set, this implies that ¬ψ j k ∈ Y j k . As ψ ∈ EML + 1 (CFL) and going through language constraints preserve polarity we know that ¬ψ j k ∈ EML + 1 (CFL) too. We conclude that ¬ψ j k ∈ ker(Y j k ) and using the induction hypothesis it is easy to see that M, s k |= ψ j k and therefore M, s |= L(ψ 1 , . . . , ψ k ). Case 1: All the subformulae ψ i belong to EML.

Arithmetical constraint: ψ = i=α i=1 a i ψ i > b. Let s ∈ T such that (s) = Y,
There are exactly C ψi children satisfying ψ i by induction hypothesis and by the fact that either ψ i or ¬ψ i belongs to Y xi . The sum of the terms will be at least b + 1 and together with the steps (initialization-counters), (guesschildren-from-left-to-right) and (final-checking) guarantee that M, s |= ψ.

Case 2: Some formula ψ i does not belong to EML. There are at least C ψi children satisfying ψ i by induction hypothesis. Observe that, given a formula ψ i belonging to some set ker(Y xj ) we know that M, s j |= ψ i . On the contrary, if ψ i / ∈ ker(Y xj ) we cannot say that M, s j |= ψ i . Therefore, the values C ψi are lower bounds for the number of children satisfying ψ i . Since each a i is strictly greater than zero, the sum of the terms will be at least b + 1 and together with the steps (initializationcounters), (guess-children-from-left-to-right) and (final-checking) guarantee that M, s |= ψ.

Negation of arithmetical constraint

: ψ = ¬ i=α i=1 a i ψ i > b.
First, observe that if ψ ∈ EML + 1 (CFL), then all ψ i ∈ EML(REG). In this case we need to show that M, s |= i=α i=1 a i ψ i b, which can be done with an argument similar to the case of positive constraints.

Periodicity constraints: ψ = i=α i=1 a i ψ i ≡ k c and ψ = ¬ i=α i=1 a i ψ i ≡ k c.
In this case, all ψ i ∈ EML(REG), therefore, ψ i ∈ EML + 1 (CFL) which lets us use the induction hypothesis on them. With this observation, these cases go through exactly as in the original proof.

The current model M is of double exponential size in |ϕ| and it is easy to show that it is N -bounded. 2

Lemma 5.7 If ϕ is EML + 1 (CFL) satisfiable in some N -bounded model then for some X ⊆ cl(0, ϕ), SAT(X, 0) has an accepting computation with ϕ ∈ ker(X).

Proof. Assume that ϕ is EML + 1 (CFL) satisfiable in some N -bounded model M = T, R, (< s ) s∈T , l . So there is s ∈ T such that M, s |= ϕ and M, s is N -bounded.

Given a formula ϕ and an EML 1 (CFL) satisfiable. For i ∈ {1, . . . , nb(d + 1)}, let Y i be the i th (d+1)-locally consistent set. We write n i to denote the number of times that the set Y i holds in the children of s , i.e., n i = card({Y i = X[s , d + 1] : s ∈ T and R (s , s )}). Observe that, since M is N -bounded, i n i nb(d + 1) × N . This is sufficient to establish that SAT(X[s , d], d) has an accepting computation. Indeed, the step (consistency) is successful because X[s , d] is d-locally consistent. The guessed number NB is obviously i n i and each set Y i is guessed n i times in the step (guess-children-from-left-to-right). Additionally, the order in which the sets Y i are guessed is precisely given by the ordering of the children of the root of M . Since M is a model for X[s , d], for every i ∈ [1, nb(d + 1)], if n i = 0, then the set Y i is satisfiable in some N -bounded model (namely M, s ). By the induction hypothesis, SAT(Y i , d + 1) returns true. Each passage to (guess-children-from-left-to-right) as well as the passage to (final-checking) are successful steps because the numbers of children is computed from M . Hence, SAT(X[s , d], d) has an accepting computation. 2 Theorem 5.8 (Correctness) A formula ϕ is EML + 1 (CFL) satisfiable in some N -bounded model iff for some X ⊆ cl(0, ϕ), SAT(X, 0) has an accepting computation and ϕ ∈ ker(X).

We are in position to establish that N is at most doubly exponential in |ϕ|. Lemma 5.9 There is a polynomial q(•) such that for every formula ϕ, ϕ is EML + 1 (CFL) satisfiable iff ϕ is satisfiable in some 2 2 q(|ϕ|) -bounded model.

checking satisfaction of subformulae on-the-fly. The optimal complexity lower bound remains unknown.

A natural question about the design of EML + 1 (CFL) is if we need to simultaneously restrict the positive occurrences of CFL-constraints and the positive occurrences of i a i ϕ i > b by imposing that either each a i > 0 and b > 0 or each ϕ i ∈ EML(REG). Indeed, if we give up this last requirement decidability is lost again. As done in Section 4, we can show that a CFL L over Σ is different from Σ * iff ¬2 ⊥ ∧ 2ϕ uni (p 1 , . . . , p k ) ∧ L(p 1 , . . . , p k ) 0 is satisfiable where Σ contains k letters (this formula is not in EML + 1 (CFL)).

Conclusion

In this paper, we have investigated the decidability status of EML extensions by adding CFL-constraints, especially those definable from VPLs. For instance, VPLs have been used to express nonregular programs [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF] for PDL. Whereas PDL augmented with VPA is decidable, we have shown that the satisfiability problem for EML 2 (VPL) is already undecidable. Also, almost every interesting restriction of this logic still leads to an undecidable fragment. By contrast, in Section 5, we establish that the satisfiability problem for EML + 1 (CFL) can be solved in 2expspace by extending proof techniques from [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF] that essentially use a Ladner-like algorithm, see e.g. [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], combined with the existence of small solutions for constraint systems. In this fragment, only one CFL-constraint may occur at each modal depth and it should have a positive polarity. Surprisingly, if only one CFLconstraint may occur negatively at each modal depth, then undecidability is back. Schema below contains the decidability status of fragments for

Lemma 3 . 2

 32 Let ϕ ∈ EML(CFL). For all models M = T, R, (< s ) s∈T , l and nodes s ∈ T , we have M, s |= ϕ iff M, s |= T(ϕ).

Theorem 3 . 3

 33 There is a reduction from EML(CFL) [resp. EML i (CFL)] satisfiability to EML(VPL) [resp. EML i (VPL)] satisfiability.

  Induction hypothesis: for all ψ such that |ψ| n, and for all s ∈ T with (s) = Y, d , if ψ ∈ ker(Y ) then M, s |= ψ.Let ψ be a formula such that |ψ| = n + 1.Basic boolean cases: ψ = ψ 1 ∧ ψ 2 and ψ = ψ 1 ∨ ψ 2 . Observe that if ψ ∈ ker(Y ) then ψ 1 , ψ 2 ∈ ker(Y ).These cases follow easily with this observation and the definition of n-locally consistent set. Negation of boolean operators: ψ = ¬(ψ 1 ∧ ψ 2 ) and ψ = ¬(ψ 1 ∨ ψ 2 ) For the first case, by definition of n-locally consistent set, at least one of ¬ψ 1 or ¬ψ 2 belongs to Y . Suppose that ¬ψ 1 ∈ Y . It is easy to check that, as ψ ∈ ker(Y ) we also have ¬ψ 1 ∈ ker(Y ). By the induction hypothesis, we get that M, s |= ¬ψ 1 and therefore M, s |= ψ. The case for ψ = ¬(ψ 1 ∨ ψ 2 ) is similar. Positive language: ψ = L(ψ 1 , . . . , ψ k ) with L ∈ REG ∪ CFL. Let s ∈ T with (s) = Y, d such that ψ ∈ cl(d, ϕ). By definition of T , SAT(Y, d) has an accepting computation. If ψ ∈ ker(Y ), then each call in the sequence SAT(Y x1 , d + 1), . . . , SAT(Y xNB , d + 1) has an accepting computation. Hence the children of s are, from left to right: s 1 , . . . , s NB such that (s i ) = Y xi , d + 1 . Then, it is not difficult to show that the steps (initialization-fsa), (initialization-pda), (guess-children-from-left-to-right) and (final-checking)(iii) guarantee that M, s |= ψ by using the induction hypothesis and the fact that each ψ i belongs to ker(Y ) too. Negation of regular language: ψ = ¬L(ψ 1 , . . . , ψ k ) with L ∈ REG. Let s ∈ T with (s) = Y, d such that ψ ∈ cl(d, ϕ). By definition of T , SAT(Y, d) has an accepting computation. Suppose s has no children, then ε / ∈ L, otherwise (final-checking) would fail. This implies M, s |= L(ψ 1 , . . . , ψ k ).

  d and ψ ∈ cl(d, ϕ). By definition of T , SAT(Y, d) has an accepting computation. If ψ ∈ ker(Y ), then each call in the sequence SAT(Y x1 , d + 1), . . . , SAT(Y x N B , d + 1) has an accepting computation. For every i ∈ [1, α], there are exactly C ψi elements in Y x1 , . . . , Y x N B that contain ψ i where C ψi is the value of the counter after the step (guess-children-from-leftto-right) in the above-mentioned successful computation for SAT(Y, d). Hence the children of s in M are the following (from left to right): s 1 , . . . , s N B with (s i ) = Y xi , d + 1 .

+ 1 (

 1 CFL) model M we use X[s , d] with s ∈ T and d ∈ [0, |ϕ|] to denote the set {ψ ∈ cl(d, ϕ) : M , s |= ψ}. We shall show that whenever M , s is N -bounded then SAT(X[s , d], d) has an accepting computation. We recall that X[s , d] is d-locally consistent. Consequently, we get that SAT(X[s, 0], 0) has an accepting computation and, by definition, ϕ ∈ ker(X[s, 0]). The proof is by induction on d max -d where d max is the maximum value such that cl(d max , ϕ) = ∅. Base case: d = d max . Any satisfiable set of literals included in cl(d max , ϕ) is consistent and leads to an accepting computation. Induction hypothesis: for all 1 n d |ϕ| and X ⊆ cl(d , ϕ) such that there exist an model M = T , R , (< s ) s∈T , l and s ∈ T with X d = {ψ ∈ cl(d , ϕ) : M , s |= ψ} and M , s is N -bounded, SAT(X[s , d ], d ) has an accepting computation. Let d = n -1 and M = T , R , (< s ) s∈T , l , with s ∈ T such that M , s is N -bounded. The set X[s , d] is, by definition, d-locally consistent and EML +

  If (s) = L(ϕ 1 , . . . , ϕ n ), then s has n children and for all j ∈ [1, n], we have (s•j) = ϕ j (formulae i a i ϕ i > b and i a i ϕ i ≡ k c have similar clauses).

	∧}, then s has two children,
	(s•1) = ψ 1 and (s•2) = ψ 2 (¬ has a similar clause).

•

  VPL}; decidable fragments appear in frames. Our work can be pursued by considering subclasses of VPA such as those definable by semisimple minded pushdown automata[START_REF] Harel | Strengthened Results on Nonregular PDL[END_REF]. Such extension are still of interest and our techniques to prove undecidability cannot be applied in that case. Also, the exact characterization of the complexity for the satisfiability problem for EML + 1 (CFL) is still open.

	EML(C)	C ∈ {CFL,
	EML 2 (C)
	EML + 2 (C)	WEML -1 (C)
	WEML + 2 (C)	EML + 1 (C)
		EML

F. Carreiro has been supported by INRIA at LSV, ENS Cachan and by CONICET Argentina at the Department of Computer Science of the University of Buenos Aires.

Acknowledgements: We thank the anonymous referees for their suggestions.

i a i ϕ i > b then for all j, we have DEP (

Proof. The proof extends that in [13, Lemma 7]. Only the main change is explained below. Suppose that C, B 1 , . . . , B , ¬B 1 , . . . , ¬B m are the automatabased formulae (or their negation) occurring in some set ker(X) ⊆ X ⊆ cl(d, ϕ) (C is the unique CFL-constraint, if any). First, we build a new PDA C + , over the alphabet Σ = {Y 1 , . . . , Y nb(n+1) } where Y 1 , . . . , Y nb(n+1) are the only (n+1)locally consistent sets. The automata C + and C have the same sets of states, initial states, stack symbols and final states and q

for some ψ ∈ Y . For each transition, the action on the stack in the new PDA should be the same as in the original one. The FSAs are also converted into new FSA B + 1 , . . . , B + , B - 1 , . . . , B - m in the same way as before (obviously, without handling the stack). Next we synchronize all the automata C + , B + 1 , . . . , B + and the complement of B - 1 , . . . , B - m into a product PDA C * over the alphabet Σ. Observe that this can be done because the intersection of all the FSA yields a FSA and the intersection of a PDA and a FSA provides a PDA. The automaton

Observe first that there is a CFG G such that L(G) = L(A * ) and the size of G is polynomial in |A * |. Moreover, there exists a FSA A * such that L(A * ) and L(G) have the same Parikh image (see e.g. [START_REF] Parikh | On context-free languages[END_REF]) and |A * | is exponential in |G|, see e.g. [START_REF] Esparza | Parikh's Theorem: A simple and direct automaton construction[END_REF]. Consequently, there is a FSA A * whose size is at most of double exponential in |ϕ|, which is one exponential higher than the bound obtained in [13, Lemma 7] for that part of the argument. The rest of the proof follows that of [START_REF] Demri | Complexity of modal logics with Presburger constraints[END_REF]Lemma 7] except that we carry values with one exponential higher.

2

Note that for CFGs in Chomsky normal form (every CFG can be converted to such form in polynomial time) a lower bound for the size of an equivalent FSA with identical Parikh image is Ω(2 n ), see e.g. [START_REF] Esparza | Parikh's Theorem: A simple and direct automaton construction[END_REF]. Hence, the reasoning performed in the proof sketch of Lemma 5.9 can be hardly improved. Another technique would be needed for substantial improvement.

Theorem 5.10 The satisfiability problem for EML + 1 (CFL) is in 2expspace. Proof. By Theorem 5.8 and Lemma 5.9, ϕ is EML + 1 (CFL) satisfiable iff SAT(X, 0) has an accepting computation and ϕ ∈ ker(X) with N = 2 2 q(|ϕ|) . By Lemma 5.5, in that case SAT runs in space polynomial in 2 |ϕ| + N , whence the complexity upper bound 2expspace by Savitch's Theorem.

2

Remark 5.11 The 2expspace bound can be shown alternatively. Indeed, by Lemma 5.9, ϕ is satisfiable iff ϕ is satisfiable by a tree-like model whose depth is bounded by |ϕ| and branching factor is at most 2 2 q(|ϕ|) . A nondeterministic 2expspace algorithm consists in guessing a model of double exponential size and then in performing a model-checking call on it, which can be done in 2expspace. Savitch's Theorem allows to regain the 2expspace bound. Note that running SAT consists in guessing the very large model by pieces while