David Baelde

Anthony Lick

Sylvain Schmitz

A Hypersequent Calculus with Clusters for Linear Frames

Keywords: modal logics, proof systems, hypersequents, clusters

The logic Kt4.3 is the basic modal logic of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words. In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity-coNP in this case. In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for Kt4.3 but does not yield any decision procedure. We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for Kt4.3. We obtain a sound and complete calculus with an associated coNP proof search algorithm. These results extend naturally to the cases of unbounded and dense frames, and to the complexity of the two-variable fragment of first-order logic over total orders.

Introduction

Modal logics are expressive and intuitive languages for describing properties of relational structures. Accordingly, when investigating properties of linear frames, it is often quite useful to express them using a tense logic [START_REF] Prior | Time and Modality[END_REF] able to reason on temporal flows. For instance, LTL [START_REF] Pnueli | The temporal logic of programs[END_REF][START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] and CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] are widely used for verifying computer programs.

When studying a logic, a common approach is to design a proof system, such as a sequent calculus. Our own interest in (enriched) sequent calculi, compared to e.g. axiomatisations, is that their associated proof-search procedures often yield decidability and even complexity results for the satisfiability and validity problems. They are also modular, allowing them to be easily adapted to handle extensions or fragments of the logic at hand. However, basic sequent calculi are often ill-suited for modal logics, as the class of frames underlying the logic is typically difficult to capture. Therefore, more expressive variants of the Work funded by ANR grant ANR-14-CE28-0005 prodaq.

sequent calculus have been developed, such as labelled sequents [START_REF] Negri | Proof analysis in modal logic[END_REF], nested sequents [START_REF] Brünnler | Deep sequent systems for modal logic[END_REF][START_REF] Poggiolesi | The method of tree-hypersequents for modal propositional logic[END_REF], linear nested sequents [START_REF] Lellmann | Linear nested sequents, 2-sequents and hypersequents[END_REF] or hypersequents [START_REF] Avron | Hypersequents, logical consequence and intermediate logics for concurrency[END_REF][START_REF] Indrzejczak | Cut-free hypersequent calculus for S4.3[END_REF][START_REF] Indrzejczak | Eliminability of cut in hypersequent calculi for some modal logics of linear frames[END_REF][START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF][START_REF] Indrzejczak | Cut elimination theorem for non-commutative hypersequent calculus[END_REF].

In this paper, we focus on K t 4.3 [START_REF] Cocchiarella | Tense and Modal Logic: a Study in the Topology of Temporal Reference[END_REF][START_REF] Blackburn | Modal Logic[END_REF], the tense logic of linear frames. Somewhat surprisingly for the logic lying at the heart of LTL with past modalitieswhich is largely studied in verification [START_REF] Lichtenstein | The glory of the past[END_REF][START_REF] Laroussinie | Temporal logic with forgettable past[END_REF]-, to the best of our knowledge, a sound and complete sequent-style calculus for K t 4.3 was only recently proposed by Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF]. This is an ordered hypersequent calculus, where the structure of the hypersequents reflects the linear structure of K t 4.3 frames. However, this calculus does not yield a proof-search algorithm, even though K t 4.3 satisfiability is known to be decidable and even NP-complete [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]. The issue here is that ordered hypersequents correspond to strictly ordered linear frames, which are arguably not the most adequate structures for the logic. Although every satisfiable K t 4.3 formula has a model whose underling frame is a strict total order, there are examples of invalid formulae (like G ⊥ ∨ F G ⊥), whose strictly ordered counter-models are all infinite. On such invalid instances, the hypersequent calculus of Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF] yields a proof tree with some infinite failure branches, thus proof-search does not terminate.

The decidability of the satisfiability problem of K t 4.3 comes from its finite model property, shown by Ono and Nakamura [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]Thm. 3]. But this property can only be obtained when working with weak total orders, i.e. allowing some worlds of the models to be equivalent for the order relation. Such groups of nodes are commonly called 'clusters.' Note that the logic itself is not able to distinguish between a weakly ordered frame and any of its 'bulldozed' strict orders [START_REF] Blackburn | Modal Logic[END_REF]Thm. 4.56].

In the remainder of this paper, we capture the syntactic aspects of these model-theoretic results. In Section 3, we show how to enhance the hypersequent calculus of Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF] by capturing the model-theoretic ideas in hypersequents with clusters and annotations. This leads to a sound and complete proof system where proof search always terminates, furthermore with a coNP complexity-which is optimal for the validity problem. Moreover, this proof system is also modular: we consider some classical extensions of K t 4.3 in Section 4, and provide new rules for our hypersequent calculus to handle these extensions; these new rules still yield an optimal coNP proof search. Finally, Manuel and Sreejith [START_REF] Manuel | Two-variable logic over countable linear orderings[END_REF] have recently shown that validity in first-order logic with two variables over strict total orders is in coNEXP. The same statement can be derived from our results and further extended to dense linear orders, by first converting the first-order formulae into equivalent exponential-sized K t 4.3 formulae [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF]; see Section 5.

We start by recalling the definition of K t 4.3 in Section 2.

Modal Logic on Weak Total Orders

We consider tense logics with two unary temporal operators, over a set Φ of propositional variables, with the following syntax:

ϕ ::= ⊥| p | ϕ ⊃ ϕ | G ϕ | H ϕ (where p ∈ Φ)
Formulae G ϕ and H ϕ are called modal formulae. Intuitively, G ϕ expresses that ϕ holds 'globally' in all future worlds reachable from the current one, while H ϕ expresses that ϕ holds 'historically' in all past worlds from which the current world is accessible. Other Boolean connectives may be encoded from ⊥ and ⊃, and we define, as is common, F ϕ = ¬G ¬ϕ expressing that ϕ will hold 'in the future' and P ϕ = ¬H ¬ϕ expressing that ϕ was true 'in the past.'

Semantics

As is standard, our formulae shall be evaluated on Kripke structures. A frame is a pair F = (W, ), where W is a set of worlds, and ⊆ W × W is a binary relation over W . A structure is a pair M = (F, V ), where F = (W, ) is a frame, and V : Φ → 2 W is a valuation function. Given such a structure, we define the satisfaction relation M, w |= ϕ, where w ∈ W and ϕ is a formula, by structural induction on ϕ:

M, w |=⊥ M, w |= p iff w ∈ V (p) M, w |= ϕ ⊃ ψ iff if M, w |= ϕ then M, w |= ψ M, w |= G ϕ iff ∀w ∈ W such that w w , M, w |= ϕ M, w |= H ϕ iff ∀w ∈ W such that w w, M, w |= ϕ
When M, w |= ϕ, we say that (M, w) is a model of ϕ.

A formula that is satisfied in all worlds of all structures is said to be valid. In this paper, we shall not consider the validity problem in general, but only in restricted classes of structures. Namely, we will consider the logic of weak total orders, i.e., the formulae that hold in all structures whose accessibility relation is transitive and total. This logic can be defined axiomatically, as shown next. Later in Section 4, we will study further restrictions of the logic.

The choice of the symbol for our frames' accessibility relations is in line with our focus on weak total orders. When working on such orders, it is useful to define x ≺ y when x y but not y x. Note that ≺ may not be a strict total order: it is transitive but not necessarily total.

Weak Total Orders

The logic K t 4.3 is defined as the set of theorems generated by necessitation, modus ponens and substitution from classical tautologies and the axioms:

G (p ⊃ q) ⊃ (G p ⊃ G q) (K r ) H (p ⊃ q) ⊃ (H p ⊃ H q) (K ) p ⊃ G P p (t r ) p ⊃ H F p (t ) F F p ⊃ F p (4) F p ∧ F q ⊃ F (p ∧ F q) ∨ F (p ∧ q) ∨ F (q ∧ F p) (.3 r ) P p ∧ P q ⊃ P (p ∧ P q) ∨ P (p ∧ q) ∨ P (q ∧ P p) ( .3 )
The first two axioms are simply the Kripke schema, given for each modality. Next we find the t axioms, which are obviously satisfied in our setting since the two modalities are converses of each other. 1 The next axiom, dubbed 4, corresponds to the transitivity of . More precisely, canonical models of 4 are transitive [START_REF] Blackburn | Modal Logic[END_REF]. Similarly, canonical models of the trichotomy axioms .3 have accessibility relationships that are non-branching to the left and to the right. All together, this implies the following completeness result:

Fact 2.1 ([2, p. 220]) A formula is a theorem of K t 4.3 iff it is
valid in all structures whose relation is transitive and total, i.e., in weak total orders. The logic K t 4.3 is perhaps better known for being complete wrt. the class of strict total orders [START_REF] Blackburn | Modal Logic[END_REF]Thm. 4.56]. As we shall see, focusing on this characterisation would however be counterproductive for our purposes. As a simple illustration of when weak total orders could be beneficial, note that some formulae admit finite weak total orders as models but only infinite strict total orders. It is the case, for example, of (G F )∧(F ), which admits a single-world model that is a weak total order. The use of weak total orders is instrumental in order to derive decidability and complexity results.

Hypersequents with Clusters

Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF] proposed a complete calculus for K t 4.3 using the framework of ordered hypersequents (aka. linear nested sequents [START_REF] Lellmann | Linear nested sequents, 2-sequents and hypersequents[END_REF]): his calculus works with lists of sequents rather than the usual multisets of sequents of hypersequent calculi. The semantics of ordered hypersequents relies on a mapping from ordered sequents to worlds that are ordered accordingly. This extension allows for a natural calculus, enjoying the subformula property and extending nicely to accommodate semantic restrictions such as unboundedness and density.

For example, the calculus of [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF] allows the following inference:

Γ ∆; ϕ Γ ∆, G ϕ
It expresses that, if w |= G ϕ for an arbitrary world w, there must be a w w such that w |= ϕ.

Unfortunately, Indrzejczak's completeness argument is quite complex, and does not yield a decision procedure. The argument is Hintikka-style: if a careful exhaustive proof search fails in his calculus, then some failed proof-search branch yields a counter-model of the conclusion hypersequent. In Indrzejczak's calculus, that failure branch may be infinite, in which case the extracted counter-model is obtained as a limit, and is itself infinite. Finite Models and Hypersequents with Clusters. In fact, the countermodels extracted from failure branches of Indrzejczak's calculus are always strictly (and totally) ordered, hence they must be infinite in some cases. The model theory of K t 4.3 provides us with a way to circumvent this problem. Indeed, K t 4.3 enjoys a finite model property for weak total orders [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]Thm. 3]; the desired finite model is obtained from the original model by applying Lemmon's filtration (see Appendix A for details).

This insight leads us to consider ordered hypersequents with clusters, corresponding semantically to sets of worlds which are all equivalent with respect to the weak total order, i.e. where w w and w w for all w, w in the cluster. In itself, this only complicates the calculus as it only creates more premises (and indeed some rules in our calculus have a large number of premises), and does not allow us to bound failure branches. For example, the inference shown above would be modified as follows:

Γ ∆; ϕ {Γ ∆ ϕ} {Γ ∆} ; ϕ {Γ ∆, G ϕ } Γ ∆, G ϕ
The bottom inference expresses that, if w |= G ϕ, then either there is w ≺ w such that w |= ϕ (first premise) or w is reflexive (second premise). In the latter case, the next inference expresses that there must be a w such that w |= ϕ satisfying either w w w (first premise) or w ≺ w (second one). Extremal Models and Annotations. Crucially, this new formalism allows us to benefit from another model-theoretic insight. It is known that satisfiability in K t 4.3 is NP-complete because any satisfiable formula ϕ admits a model of size linear in the size of the formula [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]Thm. 5] (see also [START_REF] Blackburn | Modal Logic[END_REF]Thm. 6.38]). We shall not exploit this result as such, but the construction behind it: the linear-sized model is obtained by keeping, for each subformula F ψ (resp. P ψ) of ϕ, only the rightmost (resp. leftmost) world of the original model that satisfies ψ.

Viewing our hypersequent calculus as a search for counter-models, we constrain it to search for 'extremal' counter-models as above. Concretely, we annotate some sequents with modal formulae, requiring that a modal formula occurs at most once as an annotation. For example, the previous inferences are enriched as follows (with the annotations between parentheses and in violet):

Γ ∆; ϕ (G ϕ) {Γ ∆ ϕ (G ϕ)} {Γ ∆} ; ϕ (G ϕ) { Γ ∆, G ϕ } Γ ∆, G ϕ
The annotation indicates a maximal sequent for the contradiction of the considered modal formula. This is then reflected by special inferences, for example . . . ; Γ ∆ (G ϕ) ; . . . ; Π Σ, G ϕ ; . . . which expresses that, for the (complete) class of counter-models that we are considering, there is no counter-model, since G φ would have to be contradicted strictly after a rightmost contradicting world.

With this in place, we finally obtain a calculus where failure branches are finite. This allows for an elementary completeness argument, extracting finite weakly ordered counter-models from failure branches. For the soundness argument, we indirectly make use of the extremal counter-model construction of [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]Thm. 4]. Another consequence is that proof search in our calculus directly yields an optimal coNP procedure for validity.

Definitions and Basic Meta-Theory

We shall now formally describe our calculus. We first define hypersequents with clusters and their semantics in terms of embeddings into weak total orders. We then extend them with annotations, and present our system of deduction rules. Hypersequents with Clusters. A sequent (denoted S) is a pair of two finite sets of formulae, written Γ ∆. It is satisfied in a world w of a model M if, in that world, the conjunction of the formulae of Γ implies the disjunction of the formulae of ∆. In that case, we write M, w |= Γ ∆.

In this paper, a hypersequent is a list of cells, each cell being either a sequent or a list of sequents called a (syntactic) cluster. We shall use the following abstract syntax, where both operators ';' and ' ' are associative with unit '•':

H ::= • | C ; H (hypersequents) C ::= S | {S Cl } (cells) Cl ::= • | S Cl (clusters)
The main feature of hypersequents with clusters is that their structures are weak total orders. The order of cells in a hypersequent is relevant, as it yields a strict ordering in the semantics. The order of sequents inside a cluster is semantically irrelevant; nevertheless, assuming an ordering as part of the syntactic structure of clusters is sometimes useful, as in the upcoming definition. Underlying Frames and Embeddings. Let H be a hypersequent containing n sequents, counting both the sequents found directly in its cells and those in its clusters. We call a natural number i ∈ [1; n] a position of H, and we write H(i) for the i-th sequent of H. We define the underlying frame of H as F(H) = ([1; n], ) where i j iff either the i-th and j-th sequents are in the same cluster, or the i-th sequent is in a cell that lies strictly to the left of the cell of the j-th sequent. In particular, a position can only be reflexive in the underlying frame of a hypersequent if it is in a cluster.

Let F = (W, ) and F = (W , ) be two frames. We say that µ :

W → W is an embedding of F into F if, for all (w 1 , w 2 ) ∈ W 2 , • w 1 w 2 implies µ(w 1 )
µ(w 2 ) and

• w 1 ≺ w 2 implies µ(w 1 ) ≺ µ(w 2 ).
In that case, we write F → µ F . We simply write H → µ F when F(H) → µ F . An example embedding is shown in Figure 1. Note that it is possible that µ(i) is reflexive when i is not. However, positions from distinct cells cannot be embedded into worlds of a same cluster. By contrast, distinct positions belonging to the same cluster may be mapped to the same (reflexive) world.

• • • ; Γ 1 ∆ 1 ; Γ 2 ∆ 2 ; • • • ; {Γ n ∆ n Γ n+1 ∆ n+1 • • • } ; • • • µ µ µ µ µ µ µ Fig. 1.
Embedding of a hypersequent in a weak total order. Definition 3.1 (semantics) Let M = (F, V ) be a structure. Given an embedding H → µ F, we say that (M, µ) is a model of a hypersequent H, written M, µ |= H, when there exists a position i of H such that M, µ(i) |= H(i). We say that a hypersequent is valid if for any weak total order M = (F, V ) and any embedding

H → µ F, we have M, µ |= H. 2
Annotations. We finally introduce annotations, and their semantics. An annotated sequent is a sequent that may be annotated with modal formulae. We simply write Γ ∆ for a sequent carrying no annotation, otherwise we write, e.g., Γ ∆ (H ϕ, G ψ, . . .). Then, annotated hypersequents are hypersequents whose sequents are annotated, with the constraint that an annotation may only occur once in an annotated hypersequent. Formally, we can see annotations as partial functions from the set of modal formulae to the set of positions of the hypersequent. For instance, Γ ∆ (G ϕ)

; {Π Σ (H ϕ)} is an annotated hypersequent but Γ ∆ (H ϕ, G ϕ) ; {Π Σ (H ϕ)}
is not allowed because of the two occurrences of H ϕ as an annotation. Since we use these annotations to guide the search for a finite counter-model, we only define a semantics for annotated hypersequents over finite structures. Definition 3.2 (annotation semantics) Given an annotated hypersequent H and a finite structure M = (F, V ), an embedding H → µ F is annotationrespecting if, for all i such that H(i) carries the annotation (G ϕ) (resp. (H ϕ)), there is no w ∈ W such that M, w |= ¬ϕ and µ(i) ≺ w (resp. w ≺ µ(i)).

An annotation-respecting model of H is a model ((F, V ), µ) of H where H → µ F is annotation-respecting. The sequent H is annotation-respecting valid if, for any finite weak total order M = (F, V ) and any annotation-respecting embedding H → µ F, we have M, µ |= H. 2

A peculiarity of our system is that it is sound with respect to the annotationrespecting validity of Definition 3.2, but only complete with respect to the general validity of Definition 3.1: if a hypersequent is annotation-respecting valid but not valid in general, it might not have a derivation. Thus our annotation system may be seen as a proof search strategy over a more standard, annotation-free system. 2 In any case, our proof system is sound and complete for hypersequents without annotations, since the two notions of validity coincide in that case. Rules of the Hypersequent Calculus. The rules are given in figures 2 to 4, making use of a few notations. First, we use hypersequents with holes. One-placeholder hypersequents, cells, and clusters are defined by the syntax

(ax) H [ϕ, Γ ∆, ϕ] H [ϕ ⊃ ψ, Γ ∆, ϕ] H [ϕ ⊃ ψ, ψ, Γ ∆] H [ϕ ⊃ ψ, Γ ∆] (⊃ ) (⊥) H [Γ, ⊥ ∆] H [ϕ, Γ ∆, ψ, ϕ ⊃ ψ] H [Γ ∆, ϕ ⊃ ψ] ( ⊃)
H [] ::= H ; C [] ; H C [] ::= | { Cl [] } Cl [] ::= Cl Cl
Two-placeholder cells and hypersequents have two holes identified by 1 and 2 :

H [] [] ::= H ; C [] [] ; H | H[ 1 ] ; H[ 2 ] C [] [] ::= { Cl [ 1 ] Cl [ 2 ] } | { Cl [ 2 ] Cl [ 1 ] } As usual, C [S] (resp. C [Cl ]
) denotes the same cell with S (resp. Cl ) substituted for ; two-placeholder cells and hypersequents with holes behave similarly. In terms of the frames underlying hypersequents with two holes, observe that the positions i and j associated resp. to 1 and 2 are such that i j. Second, we do not write explicitly the annotations that sequents may carry in rule applications. These annotations are implicitly the same in a conclusion sequent and the corresponding sequents in premises, or updated by adding the explicit annotation; freshly created sequents always have an explicit annotation. Annotations can prevent a rule application if the addition of an annotation would break the single-annotation constraint.

Third, we use a convenient notation for enriching a sequent: if S is a sequent Γ ∆ (A), then S (Γ ∆ (A )) is the sequent Γ, Γ ∆, ∆ (A, A ). Moreover, we sometimes need to enrich an arbitrary sequent of a cluster C with a sequent S; then C S denotes the cluster with its leftmost sequent enriched.

Modal Rules. After the usual propositional rules of Figure 2, we give in Figure 3 the introduction rules for modalities. The left introduction rules are symmetric for our two modalities. The first two, (G ) and (G ), express that if G ϕ holds at some position, then ϕ must also hold at a position to its right in the underlying frame.

Regarding the right introduction rules for modalities, let us start with the particular case where these modalities occur in extremal cells. In rule ( G), we introduce a formula G ϕ to the right of a principal sequent that is in the rightmost cell of the hypersequent. The premises cover all the ways in which a world could occur to the right of (the embedding of) the principal sequent: • If the active sequent does not belong to a cluster, i.e., if C = , it may still be embedded in a cluster in a frame, so we have to consider a premise where the last cell is changed into a single-sequent cluster.

(G ) H [G ϕ, Γ ∆] [ϕ, Π Σ] H [G ϕ, Γ ∆] [Π Σ] H 1 ; {Cl 1 ϕ, G ϕ, Γ ∆ Cl 2 } ; H 2 H 1 ; {Cl 1 G ϕ, Γ ∆ Cl 2 } ; H 2 (G ) (H ) H [ϕ, Π Σ] [H ϕ, Γ ∆] H [Π Σ] [H ϕ, Γ ∆] H 1 ; {Cl 1 ϕ, H ϕ, Γ ∆ Cl 2 } ; H 2 H 1 ; {Cl 1 H ϕ, Γ ∆ Cl 2 } ; H 2 (H ) H ; C [Γ ∆, G ϕ] ; ϕ (G ϕ) H ; {Γ ∆, G ϕ} if C = H ; C [Γ ∆, G ϕ ϕ (G ϕ)] if C = H ; C [Γ ∆, G ϕ] ( G) ϕ (H ϕ) ; C [Γ ∆, H ϕ] ; H {Γ ∆, H ϕ} ; H if C = C [Γ ∆, H ϕ ϕ (H ϕ)] ; H if C = C [Γ ∆, H ϕ] ; H ( H) H [C [Γ ∆, G ϕ] ; ϕ (G ϕ) ; C ] H [C [Γ ∆, G ϕ] ; C ( G ϕ)] H [C [Γ ∆, G ϕ] ; C ( ϕ (G ϕ))] if C is not a cluster H [{Γ ∆, G ϕ} ; C ] if C = H [C [Γ ∆, G ϕ ϕ (G ϕ)] ; C ] if C = H [C [Γ ∆, G ϕ] ; C ] ( G ) H [C ; ϕ (H ϕ) ; C [Γ ∆, H ϕ]] H [C ( H ϕ) ; C [Γ ∆, H ϕ]] H [C ( ϕ (H ϕ)) ; C [Γ ∆, H ϕ]] if C is not a cluster H [C ; {Γ ∆, H ϕ}] if C = H [C ; C [Γ ∆, H ϕ ϕ (H ϕ)]] if C = H [C ; C [Γ ∆, H ϕ]] ( H )
• Alternatively, if C = , the active sequent belongs to a cluster and we need the last premise when ϕ is falsified in an arbitrary world of that cluster.

Rule ( H) is, as expected, symmetric. Note that the ( G) and ( H) rules cannot apply when the principal formula already belongs to the annotations of some sequent of the hypersequent, since it would then create a new cell with that annotation. The rules ( G ) and ( H ), where the active sequent is not extremal, follow the same idea but have extra premises corresponding to the case where ϕ is falsified in the next cell C or beyond. Annotation Rules. Finally, the rules of Figure 4 allow special deduction steps based on the annotations, leveraging the annotation-respecting semantics. The ((G)) rule allows to derive any hypersequent where G ϕ occurs strictly to the right of a sequent carrying the annotation (G ϕ), and symmetrically for ((H)): such hypersequents cannot have annotation-respecting counter-models. The ({(G)}) and ({(H)}) rules express that, if a hypersequent features a sequent containing a modal formula both in its right hand side and in its set of annotations, then that sequent must occur in a cluster for the hypersequent to have an annotation-respecting counter-model.

((G)) H 1 [Γ ∆ (G ϕ)] ; H 2 [Π Σ, G ϕ] H 1 ; {Γ ∆, H ϕ (H ϕ)} ; H 2 H 1 ; Γ ∆, H ϕ (H ϕ) ; H 2 ({(H)}) ((H)) H 1 [Π Σ, H ϕ] ; H 2 [Γ ∆ (H ϕ)] H 1 ; {Γ ∆, G ϕ (G ϕ)} ; H 2 H 1 ; Γ ∆, G ϕ (G ϕ) ; H 2 ({(G)})
Invertibility. Note that our rules are formulated in an invertible style, keeping the principal formula in the premises. This eases the proof of completeness, where proof search induces a form of saturation. The following weakening rules are admissible in our system, and we shall use them implicitly in examples to avoid carrying around useless formulae:

H[Γ ∆] H[Γ, ϕ ∆] H[Γ ∆] H[Γ ϕ, ∆]
We prove invertibility with respect to Definition 3.1.

Lemma 3.3 (invertibility)

For any instance of a deduction rule where the conclusion hypersequent is valid, all premisses are also valid.

Proof. Considering a rule instance with a counter-model (M, µ) of a premise H, we build a counter-model (M, µ ) of the conclusion H . Depending on the rule that is applied, H and H will either have exactly the same structure, or H will have a new cell, or H will have a cluster cell where H contains a simple sequent cell. Accordingly, we take µ to be the restriction of µ to the positions of H (and adapt it accordingly for the positions that have been shifted). It is indeed a proper embedding of H into M. It is then easy to see that (M, µ ) is a counter-model of H , since any sequent

H (i) is contained in the corresponding sequent H(j): M, µ(j) |= H(j) implies M, µ (i) |= H (i). 2
Example 3.4 We provide on the next page a proof of the hypersequent {H p, G p, p G H p} in our system. At each inference, the principal formula is indicated in orange and weakenings are implicit.

Example 3.5 Consider the hypersequent G ¬G ⊥ G ⊥, which has finite counter-models with a weak total order, but no finite counter-models with a strict total order (a counter-model of this sequent must be unbounded to the right). When trying to prove this sequent with the calculus of Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF], the proof search strategy underlying its completeness argument unfolds the

P (G ) (ax) {H p, G p, p (G H p) p p (H p)} {H p, G p, p (G H p) p (H p)} p p (H p) ; {H p, G p, p (G H p)} (ax) p (H p) ; {H p, G p, p (G H p)} (H ) {H p, G p, p H p (G H p)} ( H) {H p, G p, p G H p} ( G)
where P is:

(ax) {H p, G p, p H p} ; (G H p) {H p, G p, p } ; p p (H p) ; (G H p) (ax) {H p, G p, p } ; p (H p) ; (G H p) (G ) P {H p, G p, p } ; H p (G H p) ( H )
where P is:

{H p, G p, p H p} ; { (G H p)} (ax) {H p, G p, p } ; p p (H p) ; { (G H p)} (ax) {H p, G p, p } ; p (H p) ; { (G H p)} (G ) {H p, G p, p } ; { (G H p) p p (H p)} (ax) {H p, G p, p } ; { (G H p) p (H p)} (G ) {H p, G p, p } ; { H p (G H p)} ( H )
following infinite derivation, by alternating the right and left introduction rules for G (with implicit uses of the left rules for ⊃ and ⊥): . . .

G ¬G ⊥ G ⊥ ; G ⊥, ⊥ ; ⊥ G ¬G ⊥ G ⊥ ; G ⊥, ⊥ G ¬G ⊥ G ⊥ ; ⊥ G ¬G ⊥ G ⊥
Principal formulas shown in orange, useless formulas in gray.

In our calculus, a derivation of that same hypersequent would necessarily contain several branches. The analogue of the one shown above will quickly lead to a point where only ({(G)}) applies, after which no rule applies: . . .

G ¬G ⊥ G ⊥ ; { G ⊥, ⊥ (G ⊥)} G ¬G ⊥ G ⊥ ; G ⊥, ⊥ (G ⊥) ({(G)}) G ¬G ⊥ G ⊥ ; ⊥ (G ⊥) (G ) . . . G ¬G ⊥ G ⊥ ( G)
In other words, it is a finite failure branch. As we shall see, we can extract from it a finite counter-model featuring a reflexive world. 2

Soundness

We show two soundness statements, relative to definitions 3.2 and 3.1.

Lemma 3.6 (annotation-respecting soundness) All the rules of our hypersequent calculus with clusters are sound with respect to the annotationrespecting semantics.

Proof. We prove the contrapositive. Considering a rule instance whose conclusion H admits an annotation-respecting counter-model (M, µ), we show that one of its premises also admits an annotation-respecting counter-model (M, µ ). Below, embeddings and counter-models are implicitly annotation-respecting. We first consider the case of rule ( G ), applied on a principal sequent Γ ∆, G ϕ at position i in H. Since M, µ(i) |= G ϕ, there exists w such that µ(i) w and M, w |= ¬ϕ. Since M is finite we can take w to be a rightmost world invalidating ϕ, i.e., such that there is no w ≺ w such that w |= ¬ϕ.

• We first consider the case where µ(i) and w are two worlds (distinct or not) of the same cluster. If i is not in a cluster in the underlying frame of H, i.e., if C = , then the rule has a premise

H [{Γ ∆, G ϕ} ; C ] of which (M, µ) is a counter-model. Otherwise, the premise H [C [Γ ∆, G ϕ ϕ (G ϕ)]
; C ] is available. We extend µ into µ , mapping the new sequent, at position i + 1, to the world w : µ (k) = µ(k) for all k ≤ i, µ (i + 1) = w , and µ (k + 1) = µ(k) for all k > i. Then (M, µ ) is a counter-model of the premise. In particular, the annotation (G ϕ) at position i + 1 is respected, as we have chosen µ (i + 1) = w such that for any µ (i + 1) ≺ w , w |= ϕ.

• Otherwise, µ(i) ≺ w . Let j be the first position in the cell C . If w ≺ µ(j),

we obtain a counter-model of premise

H [C [Γ ∆, G ϕ] ; ϕ (G ϕ) ; C ]
by adapting µ into an embedding µ that assigns w to the new position. If µ(j) w then we have a counter-model of the second premise

H [C [Γ ∆, G ϕ] ; C ( G ϕ)],
with the same embedding µ. Otherwise, µ(j) = w and µ(j) is not reflexive, hence the next premise is available, namely

H [C [Γ ∆, G ϕ] ; C ( ϕ (G ϕ))]. Our counter-model (M, µ) is a counter-model of that premise.
In the case of rule ({(G)}) applied on a principal sequent Γ ∆, G ϕ (G ϕ) at position i in H, i cannot be in a cluster. Since (M, µ) is a counter-model of H, we have M, µ(i) ¬G ϕ, i.e., there is a world w of M such that µ(i) w and M, w ¬ϕ. Since H(i) carries the annotation (G ϕ), we cannot have µ(i) ≺ w, hence µ(i) = w or w µ(i). Either way, µ(i) is reflexive, hence (M, µ) is still a counter-model of the premise of the rule, which creates a cluster at position i.

We finally consider the case of rule ((G)). We show that there cannot be a counter-model (M, µ) of the conclusion

H 1 [Γ ∆ (G ϕ)] ; H 2 [Π Σ, G ϕ].
Let i ≺ j be the respective positions of the two active sequents in the rule application. Since M, µ(j) ¬G ϕ, there exists w such that µ(j) w and M, w ¬ϕ. Since µ(i) ≺ w, this contradicts the fact that µ was assumed annotation-respecting.

The other rules are analogous, or easy to handle. 2

Theorem 3.7 (soundness) Our hypersequent calculus with clusters is sound: if an annotation-free hypersequent is provable, then it is valid.

Proof. We prove the contrapositive. If an annotation-free hypersequent has a counter-model, then it has a finite counter-model M as a consequence of the finite model property of K t 4.3 [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF] recalled in Lemma A.2, Appendix A. Since M is finite and H does not carry any annotations, M is also an annotation-respecting counter-model of H. So, by Lemma 3.6, H is not provable. 2

Completeness and Complexity

We now turn to establishing completeness for our calculus, and to showing that proof search yields an optimal coNP procedure for deciding K t 4.3 validity. These results follow from two properties of our calculus: deduction rules are invertible wrt. the (annotation-blind) semantics (recall Lemma 3.3), and proof search branches are polynomially bounded (as shown next in Lemma 3.8).

In this section, we call partial proof a finite open derivation tree: each node corresponds to a rule application, but some leaves may be left open. Partial proofs arise from (backward) proof search. We require that the conclusion hypersequent of any rule application differs from all of the premisses of that rule-this amounts to forbidding useless proof search steps.

In general, proof search may diverge by expanding partial proofs infinitely, or require backtracking due to (finite) choices in rule applications. Lemma 3.8 shows that divergence cannot happen with our calculus, regardless of the way rules are applied. Lemma 3.3 shows that backtracking is not necessary either. Hence, proof search in our calculus simply consists in expanding one proof attempt, either reaching a complete proof or obtaining a partial proof with at least one open leaf that cannot be derived by any rule application.

We define |H| to be the maximum of the number of positions in H and the number of distinct subformulae occurring in H. Lemma 3.8 (small branch property) For any partial proof of a hypersequent H, any branch of the proof is of length at most 4|H| 2 + 2|H|.

Proof. Let H be a hypersequent of size |H|, P a partial proof of it, and β a branch of P. Remark that the number of positions in hypersequents of β is bounded by 2|H|: we have at most |H| positions initially, and a new position may only be created together with a new annotation among at most |H| formulae. Any rule application adds some subformula among |H| to the left or to the right of the turnstile at a position among 2|H|, hence with 4|H| 2 choices, or changes a simple cell among 2|H| into a cluster. Thus β is of length at most 4|H| 2 + 2|H|. 2 Theorem 3.9 (completeness) Our hypersequent calculus with clusters is complete: every annotation-free valid hypersequent H has a proof.

Proof. Assume that a hypersequent H is not provable. Consider a partial proof P of H that cannot be expanded any more: its leaves cannot be obtained as the conclusion of a rule instance. Such a partial proof exists by Lemma 3.8. By invertibility, it suffices to exhibit a counter-model for an open leaf of P to obtain a counter-model of H as required.

We thus consider a leaf hypersequent H , which cannot be derived by any rule (excluding rule applications which would have H itself as a premise). Let F = (W, ) be the underlying frame of H . Let V be the valuation defined for all i ∈ W by V (p) = {i ∈ W | p appears on the left-hand side of H (i)} . Finally, let M = (F, V ). We shall establish that (M, µ) is a counter-model of H , where µ is the identity embedding H → µ F. More precisely, we prove by structural induction on ϕ that, for every position i of H :

• If ϕ appears on the left of the turnstile in H (i), then M, i |= ϕ.

• If ϕ appears on the right of the turnstile in H (i), then M, i |= ϕ.

We reason by case analysis on ϕ. We only detail below the case where ϕ = G ϕ , since the other cases are either standard or analogous.

• If G ϕ appears on the left-hand side of a sequent H (i), then, since rules (G ) and (G ) cannot be applied on H , ϕ appears on the left-hand side of every sequent H (j) such that i j. By induction hypothesis, M, j |= ϕ for all i j. Hence M, i |= G ϕ .

• If G ϕ appears on the right-hand side of H (i), there must be some position j such that H (j) carries the annotation (G ϕ ), as otherwise, either ( G) or ( G ) would apply. Moreover, by inspection of our rules and since H was initially annotation-free, necessarily j must contain ϕ on its right-hand side. By totality, we have i j, j i or i = j. If i = j, since rule ({(G)}) does not apply, i is in a cluster. If j i, since rule ((G)) does not apply, i and j must be in the same cluster. So we have i j in any case. By induction hypothesis on ϕ , we have M, j |= ϕ , hence M, i |= G ϕ . 2 Proposition 3.10 Proof search in our hypersequent calculus is in coNP.

Proof. Proof search can be implemented in an alternating Turing machine maintaining the current hypersequent on its tape, where existential states choose which rule to apply to which principal sequent(s) and formula, and universal states choose a premise of the rule. By Lemma 3.8, the computation branches are of length bounded by a polynomial. By Lemma 3.3, the non-deterministic choices in existential states can be replaced by arbitrary deterministic choices, thus this Turing machine has only universal states, hence is in coNP. 2

Extensions

The logic K t 4.3 can be extended by additional axioms to further restrict the class of frames. We consider here two examples of such extensions also considered by Indrzejczak [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF]: density and unboundedness. For each extension, we show that our calculus can be adapted by adding new rules corresponding to the new axioms, and yields the same coNP upper bound. These new rules are rather different from Indrzejczak's, and exploit our use of hypersequents with clusters. Together, these rules extend our calculus into a sound and complete proof system with a coNP proof search algorithm for K t Q, the logic of dense unbounded linear frames, consisting of K t 4.3 with both extensions.

Density. A frame F = (W, ) is dense if ∀(x, y) ∈ W 2 , if x y then ∃z ∈ W such that x z y.
Density is axiomatised by adding the following axiom:

F p ⊃ F F p (Den)
This new logic also has a finite model property as well as a small model property [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]. Moreover, a finite weak total order is dense if and only if it never has two consecutive worlds that are not in clusters. This last property leads to the following new rule for our calculus to handle density:

H [{S 1 } ; S 2 ] H [S 1 ; { } ; S 2 ] H [S 1 ; {S 2 }] H [S 1 ; S 2 ] (den)
Proposition 4.1 Adding (den) to our calculus yields a sound and complete proof system for K t 4.3 ∪ (Den), where proof search is in coNP.

Proof. Our rule is obviously sound, as it closely reflects the shape of dense finite weak total orders. It is also invertible, since the underlying frame of the conclusion of the rule is always a subframe of its premises. Hence Theorem 3.7 and Lemma 3.3 still hold.

To obtain that proof search is in coNP, it suffices to check that Lemma 3.8 carries over to our extension. This is true because the rule (den) can only be applied on two consecutive non-cluster cells, and whenever the rule (den) is applied on such a bad occurrence, this occurrence is no longer present in the premises. Hence, every time the rule (den) is applied, we reduce at least by one the number of bad occurrences, so we can only apply the rule (den) a finite number of times between applications of other rules creating new cells such as ( G) and ( H). Finally, since new cells can only be created polynomialy many times by those other rules thanks to our initial strategy, the new rule (den) can, in the end, only be applied polynomialy many times along a branch. So the branches of our proof tree are still polynomial.

Finally, completeness is obtained as in Theorem 3.9. It only remains to show that the underlying frame of a hypersequent found at the end of a failing branch is dense. Indeed, if its underlying frame was not dense, we could apply the rule (den) which would contradict the fact that no rules can be applied any more on this hypersequent. 2

Unboundedness. A frame F = (W, ) is unbounded to the right if ∀x ∈ W , ∃y ∈ W such that x y. Symmetrically, a frame F = (W, ) is unbounded to the left if ∀x ∈ W , ∃y ∈ W such that y x. These frame properties can be axiomatised by adding the following axiom(s):

G p ⊃ F p (D r ) H p ⊃ P p (D )
The logics we obtain when adding these axioms still have a finite model property and a small model property [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]. Moreover, a finite weak total order is unbounded to the right (resp. left) if and only if its rightmost (resp. leftmost) world is in a cluster. This leads to the following new rules for our calculus to handle unboundedness: Proof. It is easy to check that rule (D r ) is sound, as it reflects the shape of rightunbounded finite weak total orders. It is also invertible, since the underlying frame of the conclusion of the rule is always a subframe of its premises. Hence Theorem 3.7 and Lemma 3.3 still hold.

To obtain that proof search is in coNP, it suffices to check that Lemma 3.8 carries over to our extension. This is true because the rule (D r ) can only be applied when the last cell of the hypersequent is not a cluster, and whenever the rule (D r ) is applied, the last cell of its premises is always a cluster. Hence, the rule (D r ) can only be applied once between applications of other rules creating new cells such as ( G) and ( H). Finally, since new cells can only be created polynomialy many times by those other rules thanks to our initial strategy, the new rule (D r ) can, in the end, only be applied polynomialy many times along a branch. So the branches of our proof tree are still polynomial.

Finally, completeness is obtained as in Theorem 3.9. It only remains to show that the underlying frame of a hypersequent found at the end of a failing branch is unbounded to the right. Indeed, if its underlying frame was not unbounded to the right, we could apply the rule (D r ) which would contradict the fact that no rules can be applied any more on this hypersequent.

2

One can see that all rules can be taken together to form a sound and complete calculus for K t Q, with coNP proof search. Note that the rules proposed in this section differ from the ones proposed by Indrzejczak for density and unboundedness [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF]. These rules would be sound but would break our polynomial bound on the length of proof branches.

First-Order Logic with Two Variables

We show here a coNEXP upper bound on the complexity of validity in the two-variable fragment of first-order logic over linear orders, re-proving and extending recent results by Manuel and Sreejith [START_REF] Manuel | Two-variable logic over countable linear orderings[END_REF]. Syntax and Semantics. We consider first-order formulae with two variables x and y over the signature (=, <, (p) p∈Φ ) where = and < are binary relational symbols and each p is a unary relational symbol:

ψ ::= z = z | z < z | p(z) | ⊥ | ψ ⊃ ψ | ∀z.ψ (first-order formulae)
where z, z range over {x, y} and p over Φ. We call this logic FO 2 (<). We interpret our formulae over structures M = (W, <, V ) where = is interpreted as the equality over W , < as the strict total ordering of W , and each p as V (p) for the valuation V : Φ → 2 W . Equivalence with K t 4.3. Given an FO 2 (<) formula ψ(z) with one free variable z, Etessami et al. [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF] show how to construct a K t 4.3 formula ϕ such that, for all strict totally ordered structures M = (W, <, V ), M, [w/z] |= ψ if and only if M, w |= ϕ, where [w/z] is the variable assignment mapping z to w. Although the proof of [6, Thm. 2] is given for the case of the strict total order ωi.e., for ω-words over the alphabet 2 Φ -, it actually does not rely on this specific frame and applies similarly to arbitrary strict total orders.

We have therefore the following, where the NEXP upper bounds in items (i-iii) were already shown by Manuel and Sreejith [14, Thm. 15] using automata-based techniques. Let us reiterate that the complexity bounds on the satisfiability problem for the modal logics in question were already known [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF], so the interest here lies in the use of proof search in our hypersequent proof system rather than a brutal enumeration of all potential models up to some bound. Theorem 5.2 The following problems are in NEXP: satisfiability of FO 2 (<) over (i) arbitrary strict total orders, (ii) countable strict total orders, (iii) scattered strict total orders, and (iv) dense strict total orders.

Proof. Regarding (i), given an FO 2 (<) formula ψ, we first turn it into the equisatisfiable formula ∃y.ψ with one free variable x. Fact 5.1 then allows to construct a K t 4.3 formula ϕ of exponential size, which is equisatisfiable over strict total orders. By Fact 2.1, it is also equisatisfiable over weak total orders, and Theorem 3.10 shows that satisfiability can be checked in non-deterministic polynomial time in |ϕ|, hence in NEXP overall.

Regarding (ii) and (iii), by [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]Thm. 3], the above-constructed ϕ is satisfiable over weak total orders if and only if it is satisfiable over finite weak total orders. The bulldozing construction used to prove Fact 2.1 (see [START_REF] Blackburn | Modal Logic[END_REF]Thm. 4.56]) consists essentially in turning each cluster into a direct product ω * • ω (i.e., a copy of Z), which shows that ϕ is satisfiable over finite weak total orders if and only if it is satisfiable over countable scattered strict total orders.

Finally, regarding (iv), by adapting [2, theorems 4.41 and 4.56] to bulldoze clusters over Q rather than Z, ψ is satisfiable over dense strict total orders if and only if the above-constructed ϕ is satisfiable over dense weak total orders as a K t 4.3 ∪ (Den) formula. By Proposition 4.1, the latter can be checked in non-deterministic polynomial time in |ϕ|, hence in NEXP overall. 2

Discussion

We have designed a sound and complete hypersequent calculus with clusters for the modal logic K t 4.3 of linear temporal frames. The proof system relies on the finite model property of our logic in the presence of clusters to bound the length of branches during a proof search, which yields a proof search with optimal coNP complexity for the validity problem. Moreover, the approach is modular, as these results remain true when extending the proof system to handle density and unboundedness, yielding a sound and complete system for K t Q with the same complexity, and a sound and complete system for FO 2 (<) with coNEXP upper bounds. This coNEXP upper bound itself is hardly surprising, but from a proof-theoretic perspective, the two-variable fragment of first-order logic is an unusual beast-eigenvariables must be avoided-, hence our solution through a proof system for a modal logic is arguably a natural one. An extension we would like to consider in future work is well-foundedness, by adding the Gödel-Löb axiom to our logic. Here, the logic of weak total orders well-founded to the left and unbounded to the right does not enjoy a finite model property.

A Finite Model Property

We recall the result from Ono and Nakamura [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF] which yields the finite model property for all logics considered in this paper. Finite models are obtained by using a filtration [2, Def. 2.36] on a structure to obtain a finite structure of the same 'shape.' The relevant filtration in this case is called the Lemmon filtration. Lemmon Filtration. Let M = (W, , V ) be a Kripke structure. Let Ψ be a set of K t 4.3 formulae closed under taking subformulae. We define a binary relation ≡ on W by: w ≡ w iff ∀ψ ∈ Ψ, M, w |= ψ ⇐⇒ M, w |= ψ are bisimilar [START_REF] Blackburn | Modal Logic[END_REF]Thm. 2.20]. The mapping µ f can be modified into µ f 1 as follows:

µ f 1 (k) =      ([µ(k)], 0) if k ∈ C and k i ([µ(k)], 1) if k ∈ C and i ≺ k [µ(k)] if k ∈ C
This fixes the failure of the second condition of embeddings on i and j, though not necessarily on other positions.

Finally, let M be the model obtained from M f after performing this duplication for all such i ≺ j; M is finite, since M f is finite and we only did finitely many copies, and the resulting µ is such that (M , µ ) is a counter-model of H.2

Fig. 2 .

 2 Fig. 2. Propositional rules of the hypersequent calculus with clusters.

Fig. 3 .

 3 Fig. 3. Modal rules of the hypersequent calculus with clusters.

Fig. 4 .

 4 Fig. 4. Annotation rules of the hypersequent calculus with clusters.

Fact 5 . 1 (

 51 [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF] Thm. 2]) Every FO 2 (<) formula ψ(z) can be converted to an equivalent K t 4.3 formula ϕ with |ϕ| ∈ 2 poly(|ψ|) .

  Adding (D r ) (resp. (D )) yields a sound and complete proof system for K t 4.3 ∪ (D r ) (resp. K t 4.3 ∪ (D )), where proof search is in coNP.

	H ; {S}	H ; S ; { }	{S} ; H	{ } ; S ; H
	(Dr)	H ; S		S ; H	(D )
	Proposition 4.2

In a standard bi-modal setting, we would have two a priori unrelated relations. The t axioms would then force the two relations to be converses of each other in canonical models.

This more standard system simply consists of the rules of figures 2 and

without annotations, ignoring the rules of Figure

It is obviously sound. For completeness, we conjecture that Indrzejczak's proof could be adapted to weak total orders. However that system is not interesting as it is subsumed by Indrzejczak's original calculus, only adding more branches.

• We always have to consider a possible new cell strictly further to the right; in that case, the cell carries the (single) annotation (G ϕ).

The relation ≡ is an equivalence relation, and we note [w] the equivalence class of a world w ∈ W . Note that, if Ψ is finite, then ≡ has finite index. Moreover, if w ≡ w , then ∀p ∈ Φ ∩ Ψ, w ∈ V (p) ⇐⇒ w ∈ V (p). Hence, we can define the Lemmon filtration of M by Ψ as M f = (W f , f , V f ) such that:

f is transitive and linear, (iii) f is unbounded to the right (resp. left) if is unbounded to the right (resp. left), and (iv) f is dense if is dense.

Hence, all the logics presented in this paper have the finite model property.

Finally, we show that our hypersequents with clusters also enjoy the finite counter-model property; the following proof also captures our extensions to dense and unbounded frames.

Lemma A.2 If H is an invalid annotation-free hypersequent with clusters, then H has a finite counter-model.

Proof. Let (M, µ) be a counter-model of H and M f its Lemmon filtration for Ψ the set of subformulae of H. For every position i of H, we have

We can avoid this problem by duplicating such clusters.

Formally, let i ≺ j and [µ

]} be the cluster containing [µ(i)] and [µ(j)]. We define a modified model

featuring two copies of C as follows:

1 w whenever w f w

We now have ([µ(i)], 0) ≺ f 1 ([µ(j)], 1) and we still have M f 1 , ([µ(i)], 0) |= H(i) and M f 1 , ([µ(j)], 1) |= H(j), because [µ(i)] and ([µ(i)], 0) (resp. [µ(j)] and ([µ(j)], 1))


Regragui Younes
email: regragui.y@ucd.ac.ma

Laroseri

Moussa Najem
email: moussa.n@ucd.ac.ma

Dynamics of Network Connectivity in Tactical MANETs

Keywords: Self-Organized Behavior, Mobility Models, Ad hoc Networks, Group mobility, Dismounted soldiers, Battlefield

In the future battlefields, communication between commanders and soldiers will be a decisive factor to complete an assigned mission. In such military tactical scenarios, network topology is constrained by the dynamics of dismounted soldiers in the battlefield. In the battlefield area, soldiers may be divided into a number of squads and fire teams with each one having its own mission, especially in some critical situation (e.g., a military response to an enemy attack or a sweep operation of houses). This situation may cause an unpredictable behavior in terms of wireless network topology state, thus increasing the susceptibility of network topology to decomposition in multiple components. This paper presents a Group Mobility Model simulating realistic battlefield behaviors and movement techniques. We also analyze wireless communication between dismounted soldiers and their squad leader deployed in a mobile ad hoc network (MANET) under different packet sending rate and perturbation factor modeled as a standard deviation parameter which may affect soldiers' mobility. A discussion of results follows, using several performance metrics according to network behavior (such as throughput, relaying rate of unrelated packets and path length).

I. INTRODUCTION

Recently, the army has been interested in developing new skills and using more efficient technological systems for dismounted soldiers which can be adapted to their needs on the battlefield area and incorporates all modern combat equipment such as making soldiers more connected [START_REF] Cotton | Millimeter-wave stealth radio for special operations forces[END_REF] in the battlefield based on modern soldiers' electronic equipment and computer technologies by using mobile wireless ad hoc networks (MANETs) [START_REF] Council | Energy-Efficient Technologies for the Dismounted Soldier[END_REF], [START_REF] Thomas | The defence and national security capability reporter[END_REF].

In the battlefield area, communications network and information sharing are more important for mission execution by dismounted soldiers. The challenges of Military Tactical Networking is related to military-style tactical operations, where dismounted soldiers should interact simultaneously with the environment (battlefield) and with each other so as to complete an assigned mission such as a sweep operation of houses or buildings in a wide area, containing features such as mountains, forests, or rivers. This stressful overcharge of interactions in battlefield area, in conjunction with the geographically variable nature of the battlefield area and the unpredictable behavior in terms of wireless network topology state, thus increasing the susceptibility of network topology to decomposition in multiple components. The network connectivity is worsened due to topology changes driven by wireless links and unpredictable mobility of soldiers. Thus, it is natural that the highly dynamic in nature of dismounted soldiers' mobility on the battlefield has a significant impact on the network topology, eventually resulting in high rate of link failures [START_REF] Regragui | Agent-based system simulation of wireless battlefield networks[END_REF]- [START_REF] Abujassar | Mitigation fault of node mobility for the manet networks by constructing a backup path with loop free: enhance the recovery mechanism for pro-active manet protocol[END_REF]. Therefore, the evaluation of the network performance during the execution of a tactical military scenario for such situations in the real world setting is in many cases not feasible since the cost can be too high and it is impossible to test in real world. Therefore, a simulation environment is very attractive for evaluating and studying the impact of soldiers' behaviors on the performance of the network and topology condition during military operations. In this paper, we propose a novel group mobility model to simulate the mobility of soldiers by using a wedge formation as basic movement technique as realistically as possible and analyze the effectiveness of wireless communications on the battlefield between dismounted soldiers.

The rest of the paper is organized as follows. The related work is presented in Section 2. Section 3 describes the collective motion approach we have used in our group mobility model. Experimental results are presented in Section 4. Section 5 concludes the paper and discusses the future research.

II. RELATED WORK

In this section, we will review existing Group mobility models and tactical networks in MANET in the literature which make efforts to realistically model the mobility of nodes and scenarios for tactical military applications in MANETs. The Reference Point Group Mobility Model (RPGM) [START_REF] Hong | A group mobility model for ad hoc wireless networks[END_REF] is the most widely known of the group mobility models. Each group has a logical "center" which defines the entire group's motion behavior, including location, speed, direction and acceleration. In [START_REF] Wang | Group mobility and partition prediction in wireless ad-hoc networks[END_REF], the Reference Velocity Group Mobility Model (RVGM) extends the RPGM model by proposing two categories of velocity vectors: group velocity of logical center or the lead point, and the local deviation velocity of each group member. In [START_REF] Williams | Group force mobility model and its obstacle avoidance capability[END_REF], the authors introduced the Group Force Mobility Model (GFMM) which is similar to RVGM in that the velocity of a group member follows the velocity of its lead point with a small random deviation.

In recent years, several approaches have been interested in MANET for tactical and emergency scenarios. For example, in [START_REF] Fongen | A military mobility model for manet research[END_REF], the authors proposed a mobility model (Hierarchical Group Mobility model) designed for modeling a military operation in order to study the connectivity of a MANET established through wireless communication between the moving objects (ships, vehicles or foot soldiers, and aircraft). In [START_REF] Ning | Diamond group mobility model for ad hoc network in military[END_REF], the authors introduced a new group mobility model called the Diamond Group Mobility (DGM), where a group of soldiers is restricted in a diamond region with one dismounted soldier at the center considered as (commander). In [START_REF] Zhou | Group and swarm mobility models for ad hoc network scenarios using virtual tracks[END_REF], the authors proposed a virtual track based group mobility model (VT model) which closely approximates the mobility patterns in military MANET scenarios. In [START_REF] Oh | Content centric networking in tactical and emergency manets[END_REF], the authors proposed tactical MANET Content Centric Networking (CCN) for emergency wireless ad hoc environments. In [START_REF] Wang | Implementing mobile ad hoc networking (manet) over legacy tactical radio links[END_REF], the authors described the networking usage requirements for MANET over legacy narrowband tactical waveforms and discussed the common characteristics of legacy tactical radio waveforms and the implications of such characteristics for the MANET implementation.

III. CHARACTERISING AND MODELLING DISMOUNTED SOLDIERS' MOBILITY

This section presents the basic concept of our group mobility model which govern the various aspects of mobility within the group environment. It describes how the movement of dismounted soldiers is modeled on the battlefield based on a set of simple rules in order to make soldiers move collectively. These rules also are able to make each soldier behaves autonomously without a central control. The selforganized behavior of independent agents is inspired by observable characteristics of many categories of social cohesion and animals' aggregation behavior which are found in nature (e.g. ant colonies, birds flock flying and fish swarms, soldiers in the battlefield) carry out their tasks collectively in order to contribute to a common goal [START_REF] Reynolds | Flocks, herds and schools: A distributed behavioral model[END_REF], [START_REF] Couzin | Collective memory and spatial sorting in animal groups[END_REF]. Thus, the mobility of an agent can be governed by three basic rules (i.e. cohesion, separation and alignment). We assume that N dismounted soldiers move at a constant speed of v 0 units per second. Each soldier is characterized by his location p i (t) and velocity s i of direction d i (t) at time t. In each time step t, a member i assesses the position and/or orientation of neighbors in its local neighborhood within two non-overlapping behavioral zones (Fig. 5) to determine its desired direction of motion d i (t+∆t) at time t+dt. After that, the member i turns towards the direction vector d i (t + ∆t) by the turning angle α i ∆t, where

α i = σ + χ ( 1
)
where σ is the turning rate, χ is a random angle taken from a circular-wrapped gaussian distribution, centered on 0, with standard deviation χ radians gaussian-distributed angle. The location of the member i at time t + ∆t is given by:

p i (t + ∆t) = p i (t) + v i (t + ∆t)∆ts i (2)

A. Behavioral rules description

In this section, we take into account the ability of grouping individuals within two independent groups (e.g., the lead team and trail team) and the degree of interaction between them needed to develop dominance relationships. These relationships allow individuals move together as one group forming a rifle squad. Based on the interactions between soldiers and teams, our potential purpose is further to model a squad column known as a movement formation and a movement technique used in battlefield area. In the battlefield area, the squad traveling movement technique is used when enemy contact is not likely. This movement technique offers the best speed and control during maneuver, the trail team follows closely behind the lead fire team. In this paper, we are interested in incorporating both the movement formation and movement technique of a squad by considering a mathematical modeling and a set of simple rules responsible of soldiers' behaviors. 1) Repulsion behavior: Each dismounted soldier i attempts to maintain a minimum distance from neighbors within the repulsion zone (ZoR), modeled as a circle, centered on the dismounted soldier i with radius R 1 . If n r neighbors are present in this zone at time t, the direction of repulsion from neighbors is given as follows:

d i (t + ∆t) = - nr j =i r ij |r ij | (3)
where r ij = (p j -p i )/|(p j -p i )| is the unit vector from the location point of soldier i in the direction of the neighbor j.

2) Attraction and orientation behaviors: Each dismounted soldier i attempts to become attracted towards n a , and aligned with n o neighbours within both the zone of attraction and orientation (ZoA and ZoO), centered on the dismounted soldier i with radius R 2 .

d i (t + ∆t) = no j h j v j |v j | + na j =i h j r ij |r ij | (4)
where v j is a unit direction vector of soldier j. In our scenario, h j is always equals to 1 except of squad leader, where h j = 2 so as to give him a higher priority [START_REF] Freeman | Modelling group navigation: dominance and democracy in homing pigeons[END_REF].

Here d i (t+∆t) is converted to the corresponding unit vector

d(t + ∆t) = d i (t + ∆t)/|d i (t + ∆t)|.
To incorporate the influence of informed group members, a proportion of the individuals p are given information about a preferred direction (simulated as a unit vector g) representing the destination to a known resource or enemy location [START_REF] Couzin | Effective leadership and decision-making in animal groups on the move[END_REF]. However, in our considered scenario (p = 1). Then, the informed individuals balance the influence of their preferred direction and their social interactions with weighting term ω, as follows:

d i (t + ∆t) = di (t + ∆t) + ωg | di (t + ∆t) + ωg| (5)
where ω is weighting term used by the members of lead team, whereas the members of trail team use ω as weighting term towards the lead team (e.g. the destination of trail team is the lead team). The destination position is chosen randomly within the simulation area.

After a detailed analysis of the variation of ω as a function of ω (see Fig. 6), we found that ω is given as follows:

ω =              d d 0 exp(d -d 0 ) + ln( ω 4 ) ω < 1, d d 0 exp(d -d 0 ) + ω Otherwise. (6)
where Fig. 6 shows the variation of distance between trail team and lead team based on definition of ω in Eq.6. The results show that the distance d keep almost equals to the limit distance d 0 ( 20 m). After the above process has been performed for every member, all members can turn through an angle of, at most, α i ∆t radians towards the desired direction di (t + ∆t) at time (t + ∆t) by the turning rate σ;if the angle between v i (t) and di (t + ∆t) is less than α i ∆t, they achieve alignment with their desired vector, v i (t + ∆t) = di (t + ∆t), otherwise they turn α i ∆t towards it. We apply this process at each time step ∆t, where each member is able to independently perform behavioural responses to maintain interactions with other members in its neighborhood.

B. Network Model

Our group mobility model has been implemented using Java and is able to generate mobility traces. To evaluate our model in terms of network performance, we perform NS-2 simulations to observe and analyze the impact of soldiers' dynamics on reliability of communications using the mobility traces of soldiers in the battlefield area generated from our Java simulator. The squad leader can exchange communications with their neighbors in the squad.

Our network contained N mobile nodes/soldiers deployed close to each other in a simulation area of 5000×5000 m 2 . At each time step dt. The soldiers/nodes are able to exchange data packets based on AODV routing protocol with a data generation rate (λ).

IV. SIMULATION RESULTS

In this paper, to study the impact of soldiers' dynamic in the battlefield area on the performance of the network, we evaluated the network performance under different packet sending rate λ and perturbation levels χ (standard deviation). The perturbation of the soldiers' mobility is expected to simulate several effective factors in the mobility environment such as obstacles, crossing forests, and rivers. From Fig. 8, it is shown that the average throughput decreases significantly as a function of the standard deviation. Moreover, when the standard deviation becomes higher, the throughput highly decreases, especially in the range [1.8,2]. We can explain that by the fact that the increase in the standard deviation can hardly cause a topology change due mainly to perturbation of the collective motion of dismounted soldiers allowing soldiers to move with a low accuracy. As a consequence, an arbitrary partition of the network topology occurs when the standard deviation reaches a higher level. observed that the relaying rate of packets is also affected by the increase in the standard deviation. This illustrates that the nodes encounter a difficulty to find stable paths for relaying unrelated packets as the standard deviation increases. This is due mainly to bad condition of network topology which results from an increase in the link failures when the distance between two soldiers becomes higher than the transmission range. Fig. 10 shows that the path length increases as the standard deviation increases until reaching a maximum length at 0.5. But, it starts decreasing as the standard deviation continues increasing. We can explain that by the fact that the network topology is elongated when the standard deviation is (<= 0.5). However, when the standard deviation is increased enough (> 0.5), the network is partitioned info small clusters and isolated nodes. This is sufficient to explain why the path length is decreased: the source node cannot establish a path with the destination node if there are sufficient nodes which can participate as relay nodes in this path.

V. CONCLUSIONS

In this paper, we have presented a battlefield collective motion model for dismounted soldier squad, including the interaction between tail and lead teams respectively, based on a detailed modeling and analysis of the dynamic of both teams in the battlefield area. We considered a wedge formation as basic movement technique as realistically as possible. Moreover, we analyzed extensively the considered network scenario under different packet sending rate and perturbation levels of the collective motion of dismounted soldiers.

The simulation results show that the network performance is more sensitive to the dynamic of soldiers in the simulation area. Moreover, the standard deviation has a much higher impact on the throughput, relaying rate of unrelated packets and path length. Moreover, a significant perturbation of network topology is noticed when increasing the standard deviation. This reflects a worse case of the network and its limitation for assuring reliable communications under a high dynamic of soldiers in the battlefield. In our future work, we plan to extend our research to widely adopt a tactical network with several squads, where dismounted soldiers are organized into a platoon and following different tactical formations depending on the current situation on the battlefield area.

Fig. 1 .

 1 Fig. 1. Illustration of dismounted soldier group in military modern communications infrastructure.

Fig. 2 .

 2 Fig. 2. Organizational structure of a platoon.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Squad Traveling.

Fig. 5 .

 5 Fig. 5. Representation of a member in the model centered at the origin: R 1 =zone of repulsion, R 2 =zone of orientation and attraction, and α is the field of perception ahead of the member.

Fig. 9 Fig. 6 .

 96 Fig.[START_REF] Abujassar | Mitigation fault of node mobility for the manet networks by constructing a backup path with loop free: enhance the recovery mechanism for pro-active manet protocol[END_REF]. Effect of increasing the weighting ω on the between trail team and lead team in the case of ω = 0.5 (a) and with ω = 1 (b) respectively.

Fig. 7 .

 7 Fig. 7. Effect of increasing the weighting ω on the distance between trail team and lead team.

Fig. 8 .

 8 Fig. 8. Effect of increasing the standard deviation on the network throughput.

Fig. 9 .Fig. 10 .

 910 Fig.9. Effect of increasing the standard deviation on the relaying rate of unrelated packets per node.

TABLE I .

 I Mobility model parameters used in the simulation.

	Parameter	Symbol	Value
	Number of soldiers	N	9
	Zone of repulsion	ZoR	10 m
	Zone of attraction	ZoA	50 m
	Zone of orientation	ZoO	50 m
	Number of groups	-	1
	Number of teams	-	2
	Turning rate	σ	2 rad
	Initial velocity of nodes	v 0	1 (m/s)
	Packet sending rate	λ	2 and 5 (packets/s)
	Time step	dt	0.2 (s)
	Standard deviation	χ	[0,2] rad

TABLE II .

 II Network model parameters used in the simulation.

	Parameter	Value
	Propagation model	Propagation/TwoRayGround
	Network area	5000m × 5000m
	Packet generator	CBR
	Transmission range	60 m
	Simulation time	1000 s
	Queue size	64 packets
	Transport protocol	UDP
	Routing Protocol	AODV
	CBR packet size	1000 bytes