Joëlle Despeyroux
email: joelle.despeyroux@inria.fr

Carlos Olarte
email: carlos.olarte@gmail.com

Elaine Pimentel
email: elaine.pimentel@gmail.com

Hybrid and Subexponential Linear Logics Technical Report

HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In HyLL, truth judgments are labelled by worlds and hybrid connectives relate worlds with formulas. In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and an ordering on such labels defines the provability relation among resources in those locations. It is well known that SELL, as a logical framework, is strictly more expressive than LL. However, so far, it was not clear whether HyLL is more expressive than LL and/or SELL. In this paper, we show an encoding of the HyLL's logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also propose an encoding of HyLL into SELL ⋓ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. We conclude our expressiveness study by showing that previous attempts of encoding Computational Tree Logic (CTL) operators into HyLL cannot be extended to consider the whole set of temporal connectives. We show that a system of LL with fixed points is indeed needed to faithfully encode the behavior of such temporal operators.

Introduction

Logical frameworks are adequate tools for specifying proof systems, since they support levels of abstraction that facilitate writing declarative specifications of object-logic proof systems. Many frameworks have been used for the specification of proof systems, and linear logic [START_REF] Girard | Linear logic[END_REF] (LL) is one of the most successful ones. This is mainly because LL is resource conscious and, at the same time, it can internalize classical and intuitionistic behaviors (see, for example, [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF][START_REF] Cervesato | A Linear Logical Framework[END_REF]).

However, since specifications of object-level systems into the logical framework should be natural and direct, there are some features that cannot be adequately captured in LL, in particular modalities different from the ones present in LL.

Extensions of LL have been proposed in order to fill this gap. The aim is to propose stronger logical frameworks that preserve the elegant properties of linear logic as the underlying logic. Two of such extensions are HyLL (Hybrid Linear Logic)1 [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF] and SELL (Subexponential Linear Logic) [START_REF] Vincent Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF][START_REF] Olarte | Subexponential concurrent constraint programming[END_REF]. These logics have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. The difference between HyLL and SELL relies on the way modalities are handled.

In HyLL, truth judgments are labeled by worlds and two hybrid connectives relate worlds with formulas: the satisfaction at which states that a proposition is true at a given world, and the localization ↓ which binds a name for the (current) world the proposition is true at. These constructors allow for the specification of modal connectives such as A (A is true in all the accessible worlds) and ♦A (there exists an accessible world where A holds). The underlying structure on worlds allows for the modeling of transitions systems and the specification of temporal formulas [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF][START_REF] De | A logical framework for systems biology[END_REF].

In SELL, the LL exponentials (!, ?) are decorated with labels: the formula ? a A can be interpreted as A holds in a location, modality, or world a. Moreover, A can be deduced in a location b related to a (b a). On the other side, the formula ? a ! a A means that A is confined into the location a, that is, the information A is not propagated to other worlds/locations related to a. While linear logic has only seven logically distinct prefixes of bangs and question-marks (none, !, ?, !?, ?!, !?!, ?!?), SELL allows for an unbounded number of such prefixes (e.g., ! a ? c ? d ). Hence SELL enhances the expressive power of LL as a logical framework.

Up to now, it was not clear how HyLL is related to LL and/or SELL. In this paper we answer that question by showing a direct encoding of the HyLL's logical rules into LL with the highest level of adequacy. Hence, we show that HyLL is actually as expressive as LL.

We also propose an encoding of HyLL into SELL ⋓ (SELL with quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we represent HyLL formulas as formulas in SELL and encode the logical rules as formulas in SELL ⋓ . We show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This explains better why the worlds in HyLL do not add any expressive power to LL: they cannot control the logical context as the subexponentials do with the promotion rule.

HyLL has been shown to be a flexible framework for the specification of biological systems [START_REF] De | A logical framework for systems biology[END_REF] where both the system and its properties are specified using the same logic. More precisely, the properties of interest are first written in Computational Tree Logic (CTL) and later encoded as HyLL formulas. However, there was no a formal statement about the CTL fragments that can be adequately captured in HyLL. Hence, the last contribution of this paper is to continue our study of HyLL theory and to push forward previous attempts of using this logic for the specification of transition systems and formulas in CTL. We show that it is not possible to adequately encode, in HyLL, the universal path quantifier A (for all paths), nor the temporal formula EGQ (there exists a path where Q always holds). The definition of such formulas is recursive, hence one needs to use induction, at the meta-level, to accurately capture their behavior. Instead of using metareasoning, as done in [START_REF] De | A logical framework for systems biology[END_REF], we use a logical framework featuring fixed point constructs. More precisely, we use additive multiplicative LL with fixed point operators (µMALL) [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] for the encoding of CTL. We show that the well known fixed point characterization of CTL [BCM + 92] can be matched by the fixed point operators of µMALL.

The rest of the paper is organized as follows. We briefly recall LL in Section 2.1, HyLL in Section 2.2 and SELL in Section 2.3. The encoding of HyLL logical rules into LL is discussed in Section 3.1. Section 3.2 presents the encoding of HyLL into SELL ⋓ . We also prove that information confinement, a feature in SELL that is needed to specify spatial systems, cannot be captured in HyLL. Section 4 shows how to encode CTL into µMALL. Section 5 concludes the paper.

Preliminaries

Although we assume that the reader is familiar with linear logic [START_REF] Girard | Linear logic[END_REF] (LL), we review some of its basic proof theory in the following sections.

Linear Logic and Focusing

Literals are either atomic formulas (p) or their negations (p ⊥ ). The connectives ⊗ and . . . . . . . . and their units 1 and ⊥ are multiplicative; the connectives ⊕ and & and their units 0 and ⊤ are additive; ∀ and ∃ are (first-order) quantifiers; and ! and ? are the exponentials (called bang and question-mark, respectively).

First proposed by Andreoli [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] for linear logic, focused proof systems provide normal form proofs for cut-free proofs. The connectives of linear logic can be divided into two classes. The negative connectives have invertible introduction rules: these connectives are . The positive connectives ⊗, 1, ⊕, 0, ∃, and ! are the de Morgan duals of the negative connectives. A formula is positive if it is a negated atom or its top-level logical connective is positive. Similarly, a formula is negative if it is an atom or its top-level logical connective is negative.

Focused proofs are organized into two phases. In the negative phase, all the invertible inference rules are eagerly applied. The positive phase begins by choosing a positive formula F on which to focus. Positive rules are applied to F until either 1 or a negated atom is encountered (and the proof must end by applying the initial rules) or the promotion rule (!) is applied or a negative subformula is encountered, when the proof switches to the negative phase.

This change of phases on proof search is particularly interesting when the focused formula is a bipole [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF].

Definition 1. We call a monopole a linear logic formula that is built up from atoms and occurrences of the negative connectives, with the restriction that ? has atomic scope. Bipoles, on the other hand, are positive formulas built from monopoles and negated atoms using only positive connectives, with the additional restriction that ! can only be applied to a monopole.

Focusing on a bipole will produce a single positive and a single negative phase. This two-phase decomposition enables us to adequately capture the application of object-level inference rules by the meta-level linear logic, as will be shown in Section 3.

The focused system LLF for classical linear logic can be found in the appendix.

Hybrid Linear Logic

Hybrid Linear Logic (HyLL) is a conservative extension of intuitionistic first-order linear logic (ILL) [START_REF] Girard | Linear logic[END_REF] where the truth judgments are labeled by worlds representing constraints on states and state transitions. Judgments of HyLL are of the form "A is true at world w", abbreviated as A @ w. Particular choices of worlds produce particular instances of HyLL. Typical examples are "A is true at time t", or "A is true with probability p". HyLL was first proposed in [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF] and it has been used as a logical framework for specifying biological systems [START_REF] De | A logical framework for systems biology[END_REF]. Formally, worlds are defined as follows.

Definition 2 (HyLL worlds). A constraint domain W is a monoid structure W, ., ι . The elements of W are called worlds and its reachability relation :

W × W is defined as u w if there exists v ∈ W such that u.v = w.
The identity world ι is -initial and it is intended to represent the lack of any constraints. Thus, the ordinary first-order linear logic is embeddable into any instance of HyLL by setting all world labels to the identity. A typical, simple example of constraint domain is T = IN , +, 0 , representing instants of time.

Atomic propositions (p, q, . . .) are applied to a sequence of terms (s, t, . . .), which are drawn from an untyped term language containing constants (c, d, . . .), term variables (x, y, . . .) and function symbols (f, g, . . .) applied to a list of terms ( t). Non-atomic propositions are constructed from the connectives of first-order intuitionistic linear logic and the two hybrid connectives. Namely, satisfaction (at), which states that a proposition is true at a given world (w, ι, u.v, . . .), and localization (↓), which binds a name for the (current) world the proposition is true at. The following grammar summarizes the syntax of HyLL.

t

::= c | x | f ( t) A, B ::= p( t) | A ⊗ B | 1 | A → B | A & B | ⊤ | A ⊕ B | 0 | !A | ∀x. A | ∃x. A | (A at w) | ↓ u. A | ∀u. A | ∃u.
A Note that world u is bounded in the propositions ↓ u. A, ∀u. A and ∃u. A. World variables cannot be used in terms, and neither can term variables occur in worlds. This restriction is important for the modular design of HyLL because it keeps purely logical truth separate from constraint truth. We note that ↓ and at commute freely with all non-hybrid connectives [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF].

The sequent calculus [START_REF] Gentzen | Investigations into logical deductions[END_REF] presentation of HyLL uses sequents of the form Γ; ∆ ⊢ C @ w where Γ (unbounded context ) is a set and ∆ (linear context ) is a multiset of judgments of the form A @ w. Note that in a judgment A @ w (as in a proposition A at w), w can be any expression in W, not only a variable.

The inference rules dealing with the new hybrid connectives are depicted below (the complete set of rules can be found in the appendix). Γ; ∆ ⊢ A@u Γ; ∆ ⊢ (A at u)@w atR Γ; ∆, A@u ⊢ C@w Γ; ∆, (A at u)@v ⊢ C@w atL

Γ; ∆ ⊢ A[w/u]@w Γ; ∆ ⊢↓ u.A@w ↓ R Γ; ∆, A[v/u]@v ⊢ C@w Γ; ∆, ↓ u.A@v ⊢ C@w ↓ L
Note that (A at u) is a mobile proposition: it carries with it the world at which it is true. Weakening and contraction are admissible rules for the unbounded context. The most important structural properties are the admissibility of the general identity (i.e. over any formulas, not only atomic propositions) and cut theorems. While the first provides a syntactic completeness theorem for the logic, the latter guarantees consistency (i.e. that there is no proof of .; . ⊢ 0 @ w).

Theorem 1 (Identity/Cut). 1. Γ; A @ w ⊢ A @ w 2. If Γ; ∆ ⊢ A @ u and Γ; ∆ ′ , A @ u ⊢ C @ w, then Γ; ∆, ∆ ′ ⊢ C @ w 3. If Γ; . ⊢ A @ u and Γ, A @ u; ∆ ⊢ C @ w, then Γ; ∆ ⊢ C @ w.

HyLL is conservative with respect to intuitionistic linear logic: as long as no hybrid connectives are used, the proofs in HyLL are identical to those in ILL. Moreover, HyLL is more expressive than S5, as it allows direct manipulation of the worlds using the hybrid connectives, while HyLL's δ connective (see Section 4) is not definable in S5. We also note that HyLL admits a complete focused [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] proof system. The interested reader can find proofs and further meta-theoretical theorems about HyLL in [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF].

Subexponentials in Linear Logic

Linear logic with subexponentials2 (SELL) shares with LL all its connectives except the exponentials: instead of having a single pair of exponentials ! and ?, SELL may contain as many subexponentials [DJS93, NM09, OPN15], written ! a and ? a , as one needs. The grammar of formulas in SELL is as follows:

F ::= 0 | 1 | ⊤ |⊥| p( t) | F 1 ⊗ F 2 | F 1 ⊕ F 2 | F 1 . . . .
F 2 | F 1 & F 2 | ∃x.F | ∀x.F | ! a F | ? a F
The proof system for SELL is specified by a subexponential signature Σ = I, , U , where I is a set of labels, U ⊆ I is a set specifying which subexponentials allow weakening and contraction, and is a pre-order among the elements of I. We shall use a, b, . . . to range over elements in I and we will assume that is upwardly closed with respect to U , i.e., if a ∈ U and a b, then b ∈ U .

The system SELL is constructed by adding all the rules for the linear logic connectives except those for the exponentials.

The rules for subexponentials are dereliction and promotion of the subexponential labeled with a ∈ I

⊢ ? a1 F 1 , . . . ? an F n , G ⊢ ? a1 F 1 , . . . ? an F n , ! a G ! a ⊢ Γ, G ⊢ Γ, ? a G ? a
Here, the rule ! a has the side condition that a a i for all i. That is, one can only introduce a ! a if all other formulas in the sequent are marked with indices that are greater than or equal to a. Moreover, for all indices a ∈ U , we add the usual rules of weakening and contraction to ? a . We can enhance the expressiveness of SELL with the subexponential quantifiers ⋓ and ⋒ ( [NOP13, OPN15]) given by the rules (omitting the subexponential signature)

⊢ Γ, G[l e /l x ] ⊢ Γ, ⋓l x : a.G ⋓ ⊢ Γ, G[l/l x ] ⊢ Γ, ⋒l x : a.G ⋒
where l e is fresh. Intuitively, subexponential variables play a similar role as eigenvariables. The generic variable l x : a represents any subexponential, constant or variable in the ideal of a. Hence l x can be substituted by any subexponential l of type b (i.e., l : b) if b a. We call the resulting system SELL ⋓ . As shown in [START_REF] Nigam | A general proof system for modalities in concurrent constraint programing[END_REF][START_REF] Olarte | Subexponential concurrent constraint programming[END_REF], SELL ⋓ admits a cut-free, complete focused proof system (presented in the appendix). That will be the system used throughout this text.

Theorem 2. SELL ⋓ admits cut-elimination for any subexponential signature Σ.

Relative Expressiveness Power of HyLL and SELL

We observe that, while linear logic has only seven logically distinct prefixes of bangs and question-marks, SELL allows for an unbounded number of such prefixes, e.g., ! i , or ! i ? j . Hence, by using different prefixes, we allow for the specification of richer systems where subexponentials are used to mark different modalities/states. For instance, subexponentials can be used to represent contexts of proof systems [START_REF] Nigam | Specifying proof systems in linear logic with subexponentials[END_REF]; to specify systems with temporal, epistemic and spatial modalities [NOP13, OPN15] and soft-constraints or preferences [START_REF] Pimentel | A proof theoretic study of soft concurrent constraint programming[END_REF]; to specify Bigraphs [START_REF] Chaudhuri | An adequate compositional encoding of bigraph structure in linear logic with subexponentials[END_REF]; and to specify and verify biological [START_REF] Olarte | A proof theoretic view of spatial and temporal dependencies in biochemical systems[END_REF] and multimedia interacting systems [START_REF] Arias | Foundations for reliable and flexible interactive multimedia scores[END_REF].

One may wonder whether the use of worlds in HyLL increases also the expressiveness of LL. In this section we prove that this is not the case by showing that HyLL rules can be directly encoded into LL by using the methods proposed in [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF].

HyLL and Linear Logic

In [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF] classical linear logic (LL) was used as the logical framework for specifying a number of logical and computational systems. The idea is simple: use two meta-level predicates ⌊•⌋ and ⌈•⌉ for identifying objects that appear on the left or on the right side of the sequents in the object logic, respectively. Hence, object-level sequents of the form B 1 , . . . , B n ⊢ C 1 , . . . , C m (where n, m ≥ 0) are specified as the multiset ⌊B 1 ⌋, . . . , ⌊B n ⌋, ⌈C 1 ⌉, . . . , ⌈C m ⌉. If an object-formula B is in a (object-level) classical context, it will be specified in LL as ?⌊B⌋ or ?⌈B⌉ (depending on the side of B in the original sequent). Hence HyLL sequents of the form ∆; Γ ⊢ C will be encoded in LL as ?⌊∆⌋

. ). As a matter of example, the additive version of the inference rules for conjunction in classical logic

∆, A -→ Γ ∆, A ∧ B -→ Γ ∧ L1 ∆, B -→ Γ ∆, A ∧ B -→ Γ ∧ L2 ∆ -→ Γ, A ∆ -→ Γ, B ∆ -→ Γ, A ∧ B ∧ R
can be specified as

∧ L : ∃A, B.(⌊A ∧ B⌋ ⊥ ⊗ (⌊A⌋ ⊕ ⌊B⌋)) ∧ R : ∃A, B.(⌈A ∧ B⌉ ⊥ ⊗ (⌈A⌉ & ⌈B⌉))
The following definition shows how to encode HyLL inference rules into LL.

Definition 3 (HyLL rules into LL). Let w, d, h and o denote, respectively, the types for worlds, (first-order) objects, HyLL judgments and LL formulas. Let ⌈•⌉ and ⌊•⌋ be predicates of the type h → o and A, B, C have, respectively, types w → h, d → h and h. The encoding of HyLL inference rules into LL is depicted in Figure 1 (we omit the encoding of most of the linear logic connectives that can be found in [START_REF] Miller | A formal framework for specifying sequent calculus proof systems[END_REF]).

Observe that left and right inference rules for the hybrid connectives (at and ↓) are the same (see Section 2.2). This is reflected in the duality of the encoding where we only replace ⌈•⌉ with ⌊•⌋. Observe also that the inference rules for the quantifiers (first-order and worlds) look the same. The difference is on the type of

⊗ R : ∃C, C ′ , w.(⌈(C ⊗ C ′ )@w⌉ ⊥ ⊗ ⌈C@w⌉ ⊗ ⌈C ′ @w⌉) ⊗ L : ∃C, C ′ , w.(⌊(C ⊗ C ′ )@w⌋ ⊥ ⊗ (⌊C@
@w⌋)) at R : ∃C, u, w.(⌈(C at u)@w⌉ ⊥ ⊗ ⌈C@u⌉) at L : ∃C, u, w.(⌊(C at u)@w⌋ ⊥ ⊗ ⌊C@u⌋) ↓ R : ∃A, u, w.(⌈↓ u.A@w⌉ ⊥ ⊗ ⌈(A w)@w⌉) ↓ L : ∃A, u, w.(⌊↓ u.A@w⌋ ⊥ ⊗ ⌊(A w)@w⌋) ∀R(F ) : ∃B, u.(⌈∀x.B@u⌉ ⊥ ⊗ ∀x.⌈(B x)@u⌉) ∀L(F ) : ∃B, u.(⌊∀x.B@u⌋ ⊥ ⊗ ∃x.⌊(B x)@u⌋) ∀R(W ) : ∃A, u.(⌈∀v.A@u⌉ ⊥ ⊗ ∀v.⌈(A v)@u⌉) ∀L(W ) : ∃A, u.(⌊∀v.A@u⌋ ⊥ ⊗ ∃v.⌊(A v)@u⌋) ! L
: ∃C, w.(⌊!C@w⌋ ⊥ ⊗ ?⌊C@w⌋) Init : ∃C, w.(⌊C@w⌋ ⊥ ⊗ ⌈C@w⌉ ⊥ )

Figure 1: HyLL rules into LL. (Definition 3) the variables involved. Since A has type w → h, the encoding clause ∀R(W ) guarantees that the variable v has type w. Analogously, since B has type d → h, then x has type d in the clause ∀R(F ). This neat way of controlling the behavior of objects by using types is also inherited by the encoding of the other object level inference rules.

The following theorem shows that, in fact, the encoding of HyLL into LL is adequate in the sense that a focused step in FLL corresponds exactly to the application of one inference rule in HyLL.

Theorem 3 (Adequacy). Let Υ be the set of clauses in Figure 1. The sequent Γ; ∆ ⊢ F @w is provable in HyLL iff Υ, ⌊Γ⌋; ⌊∆⌋, ⌈F @w⌉ ⇑ • is provable in FLL. Moreover, the adequacy of the encodings is on the level of derivations meaning that, when focusing on a specification clause, the bipole derivation corresponds exactly to applying the introduction rule at the object level.

Proof. We will illustrate here the case for rule at L , the other cases are similar. Applying the object level rule Γ; ∆, A@u ⊢ C@v Γ; ∆, (A at u)@w ⊢ C@v at L corresponds to deciding on the LL formula given by the encoding of the rule at L (stored in Υ). Due to focusing, the derivation in LL has necessarily the shape Υ, ⌊Γ⌋; ⌊(A at u)@w⌋ ⇓ ⌊(A at u)@w⌋ ⊥ I 1 Υ, ⌊Γ⌋; ⌊∆⌋, ⌈C@v⌉, ⌊A@u⌋ ⇑ • Υ, ⌊Γ⌋; ⌊∆⌋, ⌈C@v⌉ ⇓ ⌊A@u⌋ R ⇓, R ⇑ Υ, ⌊Γ⌋; ⌊∆⌋, ⌊(A at u)@w⌋, ⌈C@v⌉ ⇓ ⌊(A at u)@w⌋ ⊥ ⊗ ⌊A@u⌋ ⊗ Υ, ⌊Γ⌋; ⌊∆⌋, ⌊(A at u)@w⌋, ⌈C@v⌉ ⇓ ∃C, u, w.(⌊(C at u)@w⌋ ⊥ ⊗ ⌊C@u⌋)

3 × ∃ Υ, ⌊Γ⌋; ⌊∆⌋, ⌊(A at u)@w⌋, ⌈C@v⌉ ⇑ • D 2
That is, the LL formula corresponding to (A at u)@w is consumed and, in the end of the focused phase, the encoding of A@u is stored into the linear context. This mimics exactly the application of the Rule at L in HyLL.

HyLL and SELL

Linear logic allows for the specification of two kinds of context maintenance: both weakening and contraction are available (classical context) or neither is available (linear context). That is, when we encode (linear) judgments in HyLL belonging to different worlds, the resulting meta-level atomic formulas will be stored in the same (linear) LL context. The same happens with classical HyLL judgments and the classical LL context. Although this is perfectly fine, encoding HyLL into SELL ⋓ allows for a better understanding of worlds in HyLL as we shall see. We use subexponentials to represent worlds, where each world has its own linear context. More precisely, a HyLL judgment of the shape F @w in the (left) linear context is encoded as the SELL ⋓ formula ? w ⌊F @w⌋. Hence, HyLL judgments that hold at world w are stored at the w linear context of SELL ⋓ . A judgment of the form G@w in the classical HyLL context is encoded as the SELL ⋓ formula ? c ? w ⌊G@w⌋. That is, the encoding of G@w is stored in the unbounded (classical) subexponential context c.

⊗ R : ∃C, C ′ . ⋒ w : ∞.(! w ⌈(C ⊗ C ′ )@w⌉ ⊥ ⊗ ? w ⌈C@w⌉ ⊗ ? w ⌈C ′ @w⌉) at R : ∃A. ⋒ u : ∞, w : ∞.(! w ⌈(A at u)@w⌉ ⊥ ⊗ ? u ⌈A@u⌉) at L : ∃A. ⋒ u : ∞, w : ∞.(! w ⌊(A at u)@w⌋ ⊥ ⊗ ? u ⌊A@u⌋) ↓ R : ∃A. ⋒ u : ∞, w : ∞.(! w ⌈↓ u.A@w⌉ ⊥ ⊗ ? w ⌈(A w)@w⌉) ↓ L : ∃A. ⋒ u : ∞, w : ∞.(! w ⌊↓ u.
A@w⌋ ⊥ ⊗ ? w ⌊(A w)@w⌋) ∀R(F ) : ∃A, ⋒w : ∞.(! w ⌈∀x.B@w⌉ ⊥ ⊗ ∀x.? w ⌈(B x)@w⌉) ∀R(W ) : ∃A, ⋒w : ∞.(! w ⌈∀v.A@w⌉ ⊥ ⊗ ⋓v : ∞.? w ⌈(A v)@w⌉) ! L : ∃C, ⋒w : ∞.(! w ⌊!C@w⌋ ⊥ ⊗ ? c ? w ⌊C@w⌋) The next definition introduces the encoding of HyLL inference rules into SELL ⋓ . Observe that, surprisingly, the subexponential structure needed is flat and it does not reflect the order on worlds. This is explained by the fact that worlds in HyLL do not control the context on rules as the promotion rule in SELL does. This also explains why HyLL does not add any expressive power to LL. Note that w : ∞ represents any subexponential in the ideal of ∞. This means that, in ⋒w : ∞.F , the subexponential variable w could be substituted, in principle, by any element of I. But note that, since world symbols are restricted to W, substituting w by c or ∞ would not match any encoded formula in the context. That is, the proposed subexponential signature correctly specifies the role of worlds in HyLL.

The following theorem shows that our encoding is indeed adequate.

Theorem 4 (Adequacy). Let Υ be the set of formulas resulting from the encoding in Definition 4. The sequent Γ; ∆ ⊢ F @w is provable in HyLL iff c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, ? w ⌈F @w⌉; • ⇑ is provable in SELL ⋓ .3 Moreover, the adequacy of the encodings is on the level of derivations.

Proof. Again, we will consider the rule at L , as the other cases are similar. If we decide to focus on the SELL ⋓ formula corresponding to the encoding of at L (stored in ? c Υ), we obtain w : ⌊(A at u)@w⌋; • ⇑ ⌊(A at u)@w⌋ ⊥ D, I c : {Υ, ⌊Γ⌋}, w : ⌊(A at u)@w⌋; • ⇓ ! w ⌊(A at u)@w⌋ ⊥ ! s c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, v : ⌈C@v⌉, u : ⌊A@u⌋; • ⇑ • c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, v : ⌈C@v⌉; • ⇓ ? u ⌊A@u⌋ R ⇑, ? s c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, w : ⌊(A at u)@w⌋, v : ⌈C@v⌉; • ⇓ ! w ⌊(A at u)@w⌋ ⊥ ⊗ ? u ⌊A@u⌋ ⊗ c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, w : ⌊(A at u)@w⌋, v : ⌈C@v⌉; • ⇓ ∃C, ⋒u, w.(! w ⌊(C at u)@w⌋ ⊥ ? u ⊗ ⌊C@u⌋) ∃, ⋒ c : {Υ, ⌊Γ⌋}, w i : ⌊∆⌋, w : ⌊(A at u)@w⌋, v : ⌈C@v⌉; • ⇑ D Observe that, in a (focused) derivation proving ! w F , the only contexts that can be present are w and the ∞ contexts due to the promotion rule and the ordering in Σ. Since the encoding does not store any formula into the context ∞, the formula ! w F must necessarily be proved from the formulas stored in w. Thus, unlike the LL derivation after Theorem 3, the context c is weakened in the left-hand side derivation since c w. Hence ⌊(A at u)@w⌋ stored initially in the location w is substituted by ⌊A@u⌋ in the location u in one focused step.

Information Confinement

One of the features needed to specify spatial modalities is information confinement : a space/world can be inconsistent and this does not imply the inconsistency of the whole system. We finish this section by showing that information confinement, a feature that can be specified in SELL, cannot be modeled in HyLL.

In [START_REF] Nigam | A general proof system for modalities in concurrent constraint programing[END_REF] the combination of subexponentials of the form ! w ? w was used in order to specify information confinement in SELL. More precisely, since the sequents (in a 2-sided sequent presentation) ! w ? w 0 ⊢ 0 and ! w ? w 0 ⊢ ! v ? v 0 are not provable in SELL, it is possible to specify systems where inconsistency is local to a given space and does not propagate to the other locations.

In HyLL, however, it is not possible to confine inconsistency: the HyLL rule Γ; ∆, 0@u ⊢ F @w 0L

shows that any formula F in any world w is derivable from 0 appearing in any world u. Observe that, even if we exchange the rule 0L for a weaker version Γ; ∆, 0@w ⊢ F @w 0 ′ L the rule 0L would still be admissible

Γ; ∆, 0@w ⊢ (0 at v)@w 0 ′ L Γ; ∆, 0@v ⊢ F @v 0 ′ L Γ; ∆, (0 at v)@w ⊢ F @v at L Γ; ∆, 0@w ⊢ F @v cut
4 Computation Tree Logic (CTL) in Linear Logic.

Hybrid linear logic is expressive enough to encode some forms of modal operators, thus allowing for the specification of properties of transition systems. As mentioned in [START_REF] De | A logical framework for systems biology[END_REF], it is possible to encode CTL temporal operators into HyLL considering existential (E) and bounded universal (A) path quantifiers. We show in this section the limitation of such encodings and how to fully capture E and A CTL quantifiers in linear logic with fixed points. For that, we shall use the system µMALL [Bae12] that extends MALL (multiplicative, additive linear logic) with fixed point operators.

CTL connectives and path quantifiers Let us recall the meaning of the temporal operators in CTL. X (Next) means "at the next state". F (Future) means "in some future" while G (Globally) means "in all futures". ϕUψ (ϕ until ψ) means "from now, ϕ will be true in every steps until some future point (possibly including now) where ψ holds (and from that point on, ϕ can be true or false)". The CTL quantifier E (Exists) means "for some path" while A (All) means "for all paths". Formulas in CTL are built from propositional variables a, b, c, ..., the usual propositional logic connectives and the temporal connectives preceded by a path quantifier:

F ::= p | F ∧ F | F ∨ F | QXF | QFF | QGF | Q[F UF ] Q ∈ {A, E} (1)
where p is a state formula.

Transition Systems Consider a set of propositional CTL variables V = {a 1 , ..., a n }. A state s is a valuation from V into the set {true, false}. We shall use pres(a i ) (resp. abs(a i )) to denote that s(a i ) = true (resp. s(a i ) = false). Hence, a state s on the set V can be seen as a conjunction of the form p 1 (a 1 ) ∧ ... ∧ p n (a n ) where p i ∈ {pres, abs}.

We consider transition systems defined by states as above and transition rules of the form r : s → s ′ . For instance, if V = {a, b}, the transition rule r : pres

Transition Systems and HyLL

In order to specify reachability properties in transition systems, some modal connectives are defined in HyLL [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF]:

A def = ↓u. ∀w. (A at u.w) ♦A def = ↓u. ∃w. (A at u.w) δ v A def = ↓u. (A at u.v) A U B def = ↓ u. ∃v. (B at u.v & ∀w ≺ v. A at u.w)
A (resp. ♦A) represents all (resp. some) state(s) satisfying A and reachable in some path from now. The connective δ represents a form of delay: δ v A stands for an intermediate state in a transition to A. Informally it can be thought to be "v before A". AUB represents that A holds in all the steps until B holds.

We may use such modal operators in order to encode some features of transition systems as HyLL formulas as follows. Consider a set V = {a 1 , ..., a n } of propositional variables, let s = p 1 (a 1 ) ∧ • • • ∧ p n (a n ) represent a state where p i ∈ {pres, abs} and r : s → s ′ be a rule specifying a state transition. We define the encoding [[•]] from CTL states and state transitions to HyLL as

[[pres(a i )]] = pres(a i ) [[abs(a i )]] = abs(a i ) [[s]] = i∈1..n [[p i (a i )]] [[r : s → s ′ ]] = ∀w. (([[s]] at w) -• δ 1 ([[s ′ ]]) at w)
Moreover, let F, G be CTL formulas built from states and the connectives ∧, ∨, U, EX, EF. We can define

C[[F ]] as C[[s]] = [[s]] C[[F ∧ G]] = C[[F ]] & C[[G]] C[[F ∨ G]] = C[[F ]] ⊕ C[[G]] C[[E[F UG]]] = C[[F ]]U C[[G]] C[[EXF ]] = δ 1 C[[F ]] C[[EFF ]] = ♦C[[F ]]
It is easy to see that such encodings are faithful, that is, a (CTL) formula F holds at state s in the system defined by the transition rules R if and only if the sequent [

[R]]@0; [[s]]@w ⊢ C[[F ]]@w
is provable in HyLL (see the appendix). In fact, since the left linear context is always constituted by atoms, the only action that can be performed is to apply transition rules up to reaching the state satisfying F , which is reachable in a finite number of steps for this CTL's limited grammar.

However, the above encodings cannot be extended to consider formulas of the shape EGF . In fact, the natural choice would be C[[EGF ]] = C[[F ]], but this encoding would not be adequate. Consider, for instance, a system with only one rule R = {r : s → s} that loops on the same state. Clearly, in CTL, s satisfies the formula EGs. Now, consider the HyLL sequent [ [R]]@0; [[s]]@w ⊢ C[[s]]@w. If we decide to introduce the connectives on the right, we obtain a derivation of the shape

[[R]]@0; [[s]]@w ⊢ [[s]]@w.v [[R]]@0; [[s]]@w ⊢ C[[s]]@w ↓ R , ∀ R , at R
where v is fresh. Furthermore, if we use the implication in [ [R]]@0, we obtain a derivation of the shape:

[[R]]@0; [[s]]@(w + 1) ⊢ G [[R]]@0; [[s]]@w ⊢ G copy, ∀ L , -• L
Therefore, the left and right states in the sequent

[[R]]@0; [[s]]@(k + n) ⊢ [[s]
] v @w.v will never match, and this sequent is not provable. Saying this in other way, the resources in the context are enough for proving the property for a (bounded) n but not for all natural numbers. For proving this, one necessarily needs (meta-level) induction which is the same as using fixed points. The next section shows how to do that with linear logic with fixed point operators.

Encoding E and A quantifiers in linear logic with fixed points

In order to prove (in CTL) the formula AFF at state s, we have to check if s satisfies F . If this is not the case, we have to check that AFF holds for all the successors of s (i.e., for all s ′ s.t. s r ==⇒ s ′ for some transition rule r). Hence, the definition of AF is recursive and it is usually characterized as a (least) fixed point.

One way to capture this behavior would by adding fixed point operators to HyLL. But it is simpler to rely on existing systems for linear logic with fixed points. In the following, we show that it is possible to characterize the CTL formulas built from the syntax (1) into the system µMALL [Bae12] that adds to linear logic (without exponentials) least and greatest fixed points. µMALL shares with linear logic all the proof rules for the additive and multiplicative connectives plus the following two rules4 ⊢ ∆, S t x ⊢ B S x, (S x)

⊥ ⊢ ∆, νB t ν ⊢ ∆, B(µB) t ⊢ ∆, µB t µ
where S is the (co)inductive invariant. The µ rule corresponds to unfolding while ν allows for (co)induction.

Path quantifiers as fixpoints

The usual interpretation of the CTL quantifiers as fixed points (see e.g.,

[BCM + 92]) is EFF = µY.F ∨ EXY EGF = νY.F ∧ EXY E[F U G] = µY.G ∨ (F ∧ EXY ) AFF = µY.F ∨ AXY AGF = νY.F ∧ AXY A[F U G] = µY.G ∨ (F ∧ AXY )
In CTL, the considered transition system is assumed to be serial, i.e. every state has at least one successor. This means that, in every state, there is at least one fireable rule.

The next definition shows how to encode CTL formulas into µMALL.

Definition 5 (CTL into µMALL). Let R be a set of transition rules. The encoding of QX, QF and QG, for Q ∈ {A, E} is in Figure 3. Given a state s = p 1 (a 1 ) ∧ • • • ∧ p n (a n ) (as in Section 4.1), we define

[[pres(a i )]] = a i [[abs(a i )]] = a ⊥ i [[s]] = [[p 1 (a 1 )]] ⊥ . . . .
(a n )]] ⊥ [[p]] = pos(p) pos(s) = [[p 1 (a 1 )]] ⊗ • • • ⊗ [[p n (a n )]] = [[s]] ⊥ neg(s) = ([[p 1 (a 1 )]] ⊥ ⊗ ⊤) ⊕ • • • ⊕ ([[p n (a n )]] ⊥ ⊗ ⊤)
where p is a state formula.5 Finally, we map the CTL connectives ∧ and ∨ into & and ⊕, respectively.

Let us give some intuition. Consider the rule r : s → s ′ . The formula pos(s) (resp. neg(s)) tests if r can (resp. cannot) be fired at the current state. The encoding of the temporal quantifiers relies on the following principles. For each transition rule, we test if the rule can be fired or not. If it can be fired, then the current state is transformed into the new state. The encoding of A (resp. E) test all (resp. one) of the fireable rules. This explains the use of & (resp. The premises correspond to proving if the rule r i is fireable or not. If r i : s i → s ′ i is fireable, we observe a derivation of the shape:

⊢ [[s ′ i ]], µB ⊢ [[s]], pos(s i ) ⊗ ([[s ′ i ]]

B).

The first is stronger than the second in the sense that B can choose the branch to move up with (L or R), while the second forces B to stick with R. Since the desired behavior is the second, offering an extra possibility is not good for proof search.

Theorem 5. Let V = {a 1 , ..., a n } be a set of propositional variables, R be a set of transition rules on V, F be a CTL formula and s |= R CT L F denote that F holds at state s in the transition system defined by R. Then,

s |= R CT L F iff the sequent ⊢ [[s]], C[[F ]] R is provable in µMALL. Proof sketch.
In the case of the least fixed point, the result comes easily since unfolding will always substitute s by a reachable state s ′ (see derivation in Example 1). For the greatest fixed point, we show that we can always provide the needed invariant. For example, assume that the states in S = {s 1 , ..., s n } satisfy the formula AGF . We can show that

I = [[s 1 ]] ⊥ ⊕ • • • ⊕ [[s n ]] ⊥ is the greatest invariant for proving the sequent ⊢ [[s]], C[[AGF ]] R .
See appendix for the detailed proof.

Our encodings assume that each rule "uses" all the variables (either present or absent). This greatly simplifies the encodings and the adequacy proofs. In [START_REF] De | A logical framework for systems biology[END_REF], this restriction is not imposed, giving rise to more compact rules. Note that our restrictions on the use of variables are without loss of generality: if a rule does not use all the variables, we can preprocess the input and generate accordingly a set of rules satisfying our requirements.

It it worth noticing that, in Definition 5, we do not encode the transition rules as a theory (as we did in Section 4.1). The reason in the following. On one hand, the presence of a formula [ [R]] in the context, encoding the rules, may allow us to move from the current state to a successor one. On the other hand, fixed points operators must be applied in order to go through paths, checking properties on them. These two actions should be coordinated, otherwise one would lose adequacy in the encodings. More precisely, by focusing on [[R]], we may "jump" a state without checking the needed property in that state. Therefore, the use of fixed points excludes the use of theories for encoding the transition system and we must internalize the transition rules in the definition of the path quantifiers (see Definition 5). This seems to be the accurate way of controlling the use of rules in CTL.

Finally, note that the encoding of the CTL operators does not use the exponentials. That is, only the multiplicative/additive part of the logic is enough.

Concluding Remarks and Future Work

We compared the expressiveness, as logical frameworks, of two extensions of linear logic (LL). We show that it is possible to encode the logical rules of HyLL into LL. In order to better analyze the meaning of worlds in HyLL, we show that a flat subexponential structure suffices to encode HyLL into SELL ⋓ . We also show that information confinement cannot be specified in HyLL. Finally, with better insights about the meaning of HyLL's words, we pushed forward previous attempts of using HyLL to encode Computational Tree Logic (CTL). We showed that only by using meta-level induction (or fixed points inside the logic) it is possible to faithfully encode CTL path quantifiers.

There are some other logical frameworks that are extensions of LL, for example, HLF [START_REF] Reed | Hybridizing a logical framework[END_REF]. Being a logic in the LF family, HLF is based on natural deduction, hence having a complex notion of (βη) normal forms as well as lacking a focused system. Thus adequacy (of encodings of systems in HLF) results are often much harder to prove in HLF than in HyLL or in SELL.

While logical frameworks should be general enough for specifying and verifying properties of a large number of systems, some logical frameworks may be more suitable for dealing with specific applications than others. Hence, it makes little sense to search for "the universal logical framework". However, it is often salutary to establish connections between frameworks, specially when they are meant to reason about the same set of systems.

In this context, both HyLL and SELL have been used for formalizing and analyzing biological systems [START_REF] De | A logical framework for systems biology[END_REF][START_REF] Olarte | A proof theoretic view of spatial and temporal dependencies in biochemical systems[END_REF]. This work indicates that SELL is a broader framework for handling such systems, since it can encode HyLL's rules naturally and directly. However, the simplicity of HyLL may be of interest for specific purposes, such as building tools for diagnosis in biomedicine. And we can use the encoding of HyLL into LL in order to perform automatic proofs of properties of systems encoded in HyLL, for example.

Formal proofs in HyLL were implemented in [START_REF] De | A logical framework for systems biology[END_REF], in the Coq proof assistant. It would be interesting to extend the implementations of HyLL given there to SELL. Such an interactive proof environment would enable both formal studies of encoded systems in SELL and formal meta-theoretical study of SELL itself.

We may pursue the goal of using HyLL/SELL for further applications. That might include neuroscience, a young and promising science where many hypotheses are provided and need to be verified.

A One Side Focused Proof System for Linear Logic

Negative rules

Ψ; ∆ ⇑ L Ψ; ∆ ⇑ ⊥, L [⊥] Ψ; ∆ ⇑ F, G
Ψ; ∆ ⇑ ⊤, L [⊤] Ψ; ∆ ⇑ F, L Ψ; ∆ ⇑ G, L Ψ; ∆ ⇑ F & G, L [&] Ψ; ∆ ⇑ F [y/x], L Ψ; ∆ ⇑ ∀x.F, L [∀]
Positive rules

Ψ; • ⇓ 1 [1] Ψ; ∆ 1 ⇓ F Ψ; ∆ 2 ⇓ G Ψ; ∆ 1 , ∆ 2 ⇓ F ⊗ G [⊗] Ψ; • ⇑ F Ψ; • ⇓ ! F [!] Ψ; ∆ ⇓ F 1 Ψ; ∆ ⇓ F 1 ⊕ F 2 [⊕ l ] Ψ; ∆ ⇓ F 2 Ψ; ∆ ⇓ F 1 ⊕ F 2 [⊕ r ] Ψ; ∆ ⇓ F [t/x] Ψ; ∆ ⇓ ∃x.F [∃]
Identity, Decide, and Reaction rules

Ψ; A ⇓ A ⊥ [I 1 ] Ψ, A; • ⇓ A ⊥ [I 2 ] Ψ; ∆ ⇓ F Ψ; ∆, F ⇑ • [D 1 ] Ψ, F ; ∆ ⇓ F Ψ, F ; ∆ ⇑ • [D 2 ] In [I 1 ] and [I 2 ], A is atomic; in [D 1 ] and [D 2 ], F is not an atom. Ψ; ∆, F ⇑ L Ψ; ∆ ⇑ F, L [R ⇑] provided that F is positive or an atom Ψ; ∆ ⇑ F Ψ; ∆ ⇓ F [R ⇓]
provided that F is negative Figure 4: Focused proof linear logic system LLF.

⊢ K : Γ ⇑ L, A ⊢ K : Γ ⇑ L, B ⊢ K : Γ ⇑ L, A & B & ⊢ K : Γ ⇑ L, A, B ⊢ K : Γ ⇑ L,
⊢ K : Γ ⇑ L ⊢ K : Γ ⇑ L, ⊥ ⊥ ⊢ K : Γ ⇑ L, ⊤ ⊤ ⊢ K + l A : Γ ⇑ L ⊢ K : Γ ⇑ L, ? l A ? l ⊢ K : Γ ⇑ L, A{c/x} ⊢ K : Γ ⇑ L, ∀x.A ∀ ⊢ K : Γ ⇑ G[l e /l x ] ⊢ K : Γ ⇑ ⋓l x : a.G ⋓ R ⊢ K : Γ ⇓ A i ⊢ K : Γ ⇓ A 1 ⊕ A 2 ⊕ i ⊢ K 1 : Γ ⇓ A ⊢ K 2 : ∆ ⇓ B ⊢ K 1 ⊗ K 2 : Γ, ∆ ⇓ A ⊗ B ⊗, given (K 1 = K 2 )| U ⊢ K : • ⇓ 1 1, given K[I \ U] = ∅ ⊢ K : Γ ⇓ A{t/x} ⊢ K : Γ ⇓ ∃x.A ∃ ⊢ K : Γ ⇓ G[l/l x ] ⊢ K : Γ ⇓ ⋒l x : a.G ⋒ L ⊢ K ≤ l : • ⇑ A ⊢ K : • ⇓! l A ! l , given K[{x | l x ∧ x / ∈ U}] = ∅ ⊢ K : Γ ⇓ A ⊥ t I, given A t ∈ (Γ ∪ K[I) and (Γ ∪ K[I \ U]) ⊆ {A t } ⊢ K + l P : Γ ⇓ P ⊢ K + l P : Γ ⇑ • D l , given l ∈ U ⊢ K : Γ ⇓ P ⊢ K + l P : Γ ⇑ • D l , given l / ∈ U ⊢ K : Γ ⇓ P ⊢ K : Γ, P ⇑ • D 1 ⊢ K : Γ ⇑ N ⊢ K : Γ ⇓ N R ⇓ ⊢ K : Γ, S ⇑ L ⊢ K : Γ ⇑ L, S R ⇑
Figure 5: Focused linear logic system with (quantified) subexponentials. Here, L is a list of formulas, Γ is a multi-set of formulas and positive literals, A t is an atomic formula, P is a non-negative literal, S is a positive literal or formula and N is a negative formula.

• (K 1 ⊗ K 2 )[i] = K 1 [i] ∪ K 2 [i] if i / ∈ U K 1 [i] if i ∈ U • K[S] = {K[i] | i ∈ S} • (K + l A)[i] = K[i] ∪ {A} if i = l K[i] otherwise • K ≤ i [l] = K[l] if i l ∅ if i l • (K 1 ⋆ K 2 ) | S is true if and only if (K 1 [j] ⋆ K 2 [j])
Figure 6: Specification of operations on contexts. Here, i ∈ I, j ∈ S, S ⊆ I, and the binary connective ⋆ ∈ {=, ⊂, ⊆}.

D Adequacy Proofs D.1 CTL in HyLL

Proposition 1. Let V be a set of variables and R = {r 1 , ..., r m } be a set of transition rules on V. Then,

s ri ==⇒ s ′ iff the sequent [[r 1 ]]@0, • • • , [[r n ]]@0; [[s]]@w ⊢ δ 1 [[s ′ ]]@w
is provable in HyLL.

Proof. We will use the focused version of the HyLL system [START_REF] Despeyroux | A hybrid linear logic for constrained transition systems[END_REF] and assume that atoms have positive bias. Observe that [[s]]@w and δ 1 [[s ′ ]]@w will be decomposed in the negative phase, giving rise to a sequent of the shape

[[r 1 ]]@0, • • • , [[r n ]
]@0; s 1 @w, . . . , s n @w ⊢ s ′ 1 @w.1 ⊗ . . . ⊗ s ′ n @w.1 where s i , s ′ i ∈ {pres(a i ), abs(a i )}. Since each s i is a literal in the world w and the literals in s ′ i belong to the world w.1, it is not possible to focus on s ′ 1 @0 ⊗ . . . ⊗ s ′ n @0. Hence, the only possibility of proceeding with the proof is by focusing on one of the formulas [[r i ]]@0. Due to the shape of [[r i ]]@0, in one focused step, we consume all atoms from [[s]]@w and add to the context the formula [[s ′ ]]@w.1. This mimics exactly the transition s ri ==⇒ s ′ . Now we can focus on the right of the sequent and the proof finishes. Note that focusing again in a formula [[r i ]]@0 is pointless since the atoms will be produced at the world w + n (n > 1) and hence, never matching the formulas on the right.

CTL Formulas in HyLL

The next proposition considers only the encoding of the fragment of CTL into HyLL presented in Section 4.1.

Proposition 2. The CTL formula F holds at state s iff [[R]]@0; [[s]]@w ⊢ C[[F ]]@w is provable in HyLL.
Proof. (⇒) By induction on the structure of F . For the base case, if the state s satisfies the state formula p, it is easy to show that the sequent [

[s]]@u ⊢ [[P ]]@u is provable in HyLL. If s |= R CT L EF F , then there is a path s = s 1 r-i1 ==⇒ s 2 • • • s m-1 r-im-1
==⇒ s m where F holds at s m . Hence, at each step, we choose a rule from R until a F -state is reached. In HyLL, looking a derivation bottom-up, we focus on one of the rules and transform the state [[s i ]]@w into the state [[s i+1 ]]@w.1. The result follows by repeated applications of Proposition 1. The cases for E[F UG] and EXF follow similarly. Finally, the cases for ∧ and ∨ follow immediately by inductive hypothesis.

(⇐) Using the focusing discipline, we shall show that each focused step corresponds exactly to a "step" in the deduction of s |= R CT L F . In order to ease the proof, we shall consider an encoding slightly different. Let d + (F ) = F ⊗ 1 and d -(F ) = 1 -• F respectively. Observe that d + (F ) ⇔ d -(F ) ⇔ F . Hence, we only introduce positive or negative delays that allow us to focus / disallow focusing in a derivation. The proposed encoding is:

C[[s]] = [[s]] C[[F ∧ G]] = d + (C[[F ]] & C[[G]]) C[[F ∨ G]] = d -(C[[F ]]) ⊕ d -(C[[G]]) C[[E[F UG]]] = C[[F ]]U C[[G]] C[[EXF ]] = d + (δ 1 C[[F ]]) C[[EFF ]] = ♦C[[F ]] Consider the sequent [[R]]@0; [[s]]@w ⊢ C[[F ]]@w.
We have two choices: 1) we focus on one of the rules in R and we transform, in one focused step, the state s into the state s ′ ; or 2), we focus on the formula on the right. In the first case, we already showed that this action mimics exactly the transition s ri ==⇒ s ′ . In the second case, we note that the formula on the right must have the following shape:

F ::= S | 1 ⊗ (F & F ) | F ⊕ F |↓ u (F at u.1) |↓ u (∃w.F at u.w) | ↓ u ∃v.(F at u.v & ∀w ≺ v.F at u.w)
where S is of the shape s 1 @w ⊗ . . . ⊗ s n @w (the encoding of a state formula). The other cases represent, respectively, the encoding of CTL formulas of the shape F ∧ F , F ∨ F , EXF , EFF and E[F UF ]. In a negative phase, the only connectives we can introduce, if any, are the hybrid ones (↓ and at). This is a bureaucratic step allowing us to fix the formulas at the "current" world as in Γ; ∆ ⊢ F [x/w]@y Γ; ∆ ⊢↓ x(F at y)@w at R , ↓ R Hence, when focusing on the right, we fall in the following cases. If we focus on:

• S, the context must already have the atoms, at the right world, to prove the conjunction of atoms in S. This corresponds to proving that the state s satisfies the state property S.

• 1 ⊗ (F & G), we prove 1 and we lose focusing in F & G. Hence, after a negative phase, we have a derivation proving F and another proving G. This corresponds exactly to the step of proving F and G in CTL.

• F ⊕ G, we chose one of the branches and then, we lose focusing again (due to the negative delay in the encoding). This corresponds to proving either F or G in CTL.

• d + (δ 1 F ), we lose focusing again and we obtain, on the right, F fixed at the world w + 1. This mimics the step of proving F in the next time-unit to show that EXF holds in CTL.

• ∃w.F at u.w, we choose a world w and we lose focusing (due to at). This corresponds in CTL to proving EFF by showing that there exists a future world (u + w) where F holds.

• The case of E[F UG] is similar to the previous one.

D.2 CTL in µMALL

Theorem 5. Let V = {a 1 , ..., a n } be a set of propositional variables, R be a set of transition rules on V and F be a CTL formula. Then,

s |= R CT L F iff the sequent ⊢ [[s]], C[[F ]] R is
φ = C[[F ]] R .
In each case, for every premise we have to start a positive phase and we have to choose between neg(s i ) and pos(s i ). In the first case, if the rule is not fireable, the proof ends. In the second case, we obtain a derivation of the shape:

⊢ [[s ′ i ]], φ ⊢ [[s]], pos(s i ) ⊗ ([[s ′ i ]] .
[[F ]] R in the disjunction C[[AFF ]] R = µY.C[[F ]] R ⊕ Φ).
The other cases for least fixed point operators follow similarly. Cases for the greatest fixed point operators. Consider now the formula AGF . If this formula holds at s, then s must satisfy F and all path starting from s must also satisfy AGF . Let S = {s | s |= R CT L F and, for all s ′ , if s ==⇒ s ′ , then s ′ ∈ S} be the greatest set of states containing s. Note that the greatest fixed point in the (CTL) definition of AG computes exactly that set. Let S above be the set {s 1 , ..., s n } and

I = [[s 1 ]] ⊥ ⊕ • • • ⊕ [[s n ]] ⊥ 6
. We shall show that, for any s ∈ S, the sequent ⊢ [[s]], C[[AGF ]] R is provable using I as inductive invariant.

Once the rule ν is applied, we have to prove two premises: If the rule r i is not fireable at state s, the sequent ⊢ [[s]], R i is provable (by choosing neg(s i )).

⊢ φ, [[s]] ⊢ R 1 , [[s]] • • • ⊢ R n , [[s]] ⊢ φ & R 1 & • • • & R n ,
If r i is fireable at state s, we then have, in a focused step, the following derivation:

⊢ [[s ′ ]], I ⊢ R i , [[s]] ⊕, ⊗, &
Since S is closed under ==⇒, it must be the case that s ′ ∈ S and then, the sequent ⊢ [[s ′ ]], I is provable.

The case EG is similar. (⇐) Due to focusing, we can show that the derivations in the ⇒ part are the only way to proceed during a proof in µMALL. Hence, we match exactly a "step" in the deduction of s |= R CT L F . The only interesting case is the one of the greatest fixed point operator. Consider the CTL formula AGF and assume that we have a proof of the sequent ⊢ [[s]], νB with invariant I x . This means that we have a proof of the sequent ⊢ [[s]], I x . Moreover, due to the shape of B, we must also have a proof of ⊢ [[s ′ ]], I x for any reachable state s ′ . Then, we can show that there is a proof of ⊢ I x , & s∈S [[s]] where s ∈ S and all reachable state s ′ (from s), is also in S. Let I be the invariant in the proof of the ⇒ part. Note that I ⊥ = & s∈S [[s]] and then, we have a proof of ⊢ I x , I ⊥ (i.e., ⊢ I -• I x ). This shows that I is greater than I x and then, we also have a proof of ⊢ [[s]], νB using I. The result follows from a derivation similar to the one used in the proof of the ⇒ part.

Figure 2 :

 2 Figure 2: HyLL rules into SELL ⋓ . (Definition 4)

Definition 4 .

 4 Let w, d, h, ⌈•⌉, ⌊•⌋, A, B, C be as in Definition 3 and o be the type for SELL ⋓ formulas. Given a HyLL constraint domain W, consider a subexponential signature Σ = I, , U such that I = W ∪ {∞, c}, w ∞ for any w ∈ I and, for any u, w ∈ W ∪ {c}, u w. Moreover, U = {c, ∞}. The encoding of HyLL inference rules into SELL ⋓ is depicted in Figure 2 (we omit the encodings of the other connectives, that follow similarly).

  (a) ∧ abs(b) → abs(a) ∧ pres(b) enables a transition from a state s = {a → true, b → false} to the state s ′ = {a → false, b → true}. We shall use s r ==⇒ s ′ to denote such transitions.

1.

  Premise ⊢ [[s]], I. This sequent is easy by choosing [[s]] ⊥ from I. 2. Premise ⊢ B I, I ⊥ . The & s∈S [[s]] formula in I ⊥ forces us to prove several cases. More precisely, for each s ∈ S, we have to prove ⊢ BI, [[s]]. Consider the following derivation:

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . , ⊥, &, ⊤, ∀, and ?

  . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  Inference rules are specified by a rewriting clause that replaces the active formula in the conclusion by the active formulas in the premises. The linear logic connectives indicate how these object level formulas are connected: contexts are copied (&) or split (⊗), in different inference rules (⊕) or in the same sequent (

				. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
					. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ⌊Γ⌋ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ⌈C⌉ where, if Ψ = {F 1 , ..., F n }, then ⌊Ψ⌋ = ⌊F 1 ⌋ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ... . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ⌊F n ⌋ and ?⌊Ψ⌋ = ?⌊F 1 ⌋ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ... . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ?⌊F n ⌋ (similarly for ⌈•⌉). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  w⌋ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . ⌊C ′

  ). Consider the temporal formula AFF . We first check if F holds in the current state. If this is not the case, for each of the fireable rules, we consume [[s]] (using pos(s)) and release [[s ′ ]], thus updating the current state. For instance, consider the sequent ⊢ [[s]], C[[AFF ]] R and assume that the formula F does not hold at state s. If we decide to focus on C[[AFF ]] R we obtain a derivation of the shape

	Example 1. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	⊢ [[s]], µB	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)	µ, ⊕, &

⊢ [[s]], neg(s 1 ) ⊕ (pos(s 1 ) ⊗ ([[s ′ 1 ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB) ... ⊢ [[s]], neg(s m ) ⊕ (pos(s m ) ⊗ ([[s ′ m ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . We could have written instead [[r]] -• B, which reads closer to what we expect: "assuming that r is fired, B holds". The formulas (L -• R) -• B and L ⊗ (R -• B) are not equivalent. In fact, the first formula is equivalent to (L ⊗ R ⊥ ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	C[[AXF ]] R				. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ))
	C[[EXF ]] R	=	(pos(s) ⊗ ([[s ′ ]]	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ))
	s→s ′ ∈R C[[AFF ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
	C[[EFF ]] R	= µY. φ ⊕	(pos(s) ⊗ ([[s ′ ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
	C[[AGF ]] R C[[EGF ]] R	s→s ′ ∈R = νY. φ & & s→s ′ ∈R = νY. φ &	(neg(s) ⊕ (pos(s) ⊗ ([[s ′ ]] (pos(s) ⊗ ([[s ′ ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
			s→s ′ ∈R
	s→s ′ ∈R C[[A[F U G]]] R = µY.ψ ⊕ φ & &	(neg(s) ⊕ (pos(s) ⊗ ([[s ′ ]]	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y )))
	C[[E[F U G]]] R = µY.ψ ⊕ φ &		(pos(s) ⊗ ([[s ′ ]]	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Y ))
			s→s ′ ∈R
					. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .				. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
					. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)	⊗,	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
			⊢ [[s]], neg(s i ) ⊕ (pos(s i ) ⊗ ([[s ′ i ]]	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . = & s→s ′ ∈R (neg(s) ⊕ (pos(s) ⊗ ([[s ′ ]] . . R = µY. φ ⊕ & s→s ′ ∈R (neg(s) ⊕ (pos(s) ⊗ ([[s ′ ]] .

Figure 3: Encoding of CTL temporal operators into µMALL. Here, φ = C[[F ]] R and ψ = C[[G]] R . where s becomes s ′ i and, from that state, µB must be proved. Remark 1. Observe that, in all the clauses in Figure 3, the formula pos(s) ⊗ ([[s ′ ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . B), is present. . . . . . . . . . . . . . . . . . . . . . . . . . . . . B while the second is equivalent to L ⊗ (R ⊥ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  , L Ψ; ∆ ⇑ F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . G, L	[	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ]	Ψ, F ; ∆ ⇑ L Ψ; ∆ ⇑ ?F, L	[?]

.

  A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . B	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

.

  provable in µMALL. Proof. (⇒) We proceed by induction on the structure of the formula. The base case of a state formula P is immediate (from the encoding [[s]]). The cases for ∧ and ∨ are easy consequences from the inductive hypothesis. Cases AX and EX. Let us note that, given two different states s and s ′ : • the sequents ⊢ [[s]], pos(s) and ⊢ [[s]], neg(s ′ ) are both provable. • the sequents ⊢ [[s]], neg(s) and ⊢ [[s]], pos(s ′ ) are not provable.This means that, in a context containing a formula [[s]], we can always prove that a given rule r i ∈ R is firable or not.Consider the case AXF . In a negative phase, we obtain the following derivation:

	⊢ [[s]], &	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ))	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ)	&
	where

⊢ [[s]], neg(s 1 ) ⊕ (pos(s 1 ) ⊗ ([[s ′ 1 ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ) ... ⊢ [[s]], neg(s m ) ⊕ (pos(s m ) ⊗ ([[s ′ m ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . s→s ′ ∈R (neg(s) ⊕ (pos(s) ⊗ ([[s ′ ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . the positive phase ends. By inductive hypothesis, the sequent ⊢ [[s ′ i ]], φ is provable. The case EXF is similar. Cases for the least fixed point operators. If AFF holds in CTL at state s, then, in all paths starting at s, there is a reachable state s ′ such that F holds in that state. Let s = s 1 ==⇒ • • • ==⇒ s n = s ′ be one of such paths and consider the following derivation: ⊢ [[s]], neg(s 1 ) ⊕ (pos(s 1 ) ⊗ ([[s ′ 1 ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB) ... ⊢ [[s]], neg(s m ) ⊕ (pos(s m ) ⊗ ([[s ′ m ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . .The premises correspond to proving whether the rule r i is fireable or not. If r i : s i → s ′ i is fireable, we observe a derivation of the shape:⊢ [[s ′ i ]], µB ⊢ [[s]], pos(s i ) ⊗ ([[s ′ i ]]. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . [[s]], neg(s i ) ⊕ (pos(s i ) ⊗ ([[s ′ i ]] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . where s becomes s ′ i and, from that state, µB must be proved. Hence, we can show that [[s n ]] will be eventually added to the context. By inductive hypothesis, the sequent ⊢ C[[F ]] R , [[s n ]] is provable and then, ⊢ [[s n ]], µB is provable (by choosing C

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	⊢ [[s]], µB			. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)	µ, ⊕, &
		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µB)) ⊗, . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	⊕
		. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . φ)	⊗,	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

and . . ⊢

  Again we have several cases to prove. The first sequent ⊢ φ, [[s]] follows from inductive hypothesis.

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

[[s]] & where φ = C[[F ]] R and R i = neg(s i ) ⊕ (pos(s i ) ⊗ ([[s ′ i ]]

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . I).

Actually, HyLL is an extension of intuitionistic linear logic (ILL), while SELL can be viewed as an extension of both ILL or LL.

We note that intuitionistic and classical SELL are equally expressive, as shown in[START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF]. Hence, although we will introduce here the classical version of SELL (needed in Section

3.2), we could also present SELL as an extension of ILL.

Clarifying some notation: if ∆ = {F 1 @w 1 , . . . , Fn@wn}, then ? w i ⌊∆⌋ = ? w 1 ⌊F 1 @w 1 ⌋, . . . , ? wn ⌊Fn@wn⌋. Observe that, in the negative phase, such formulas will be stored at their respective contexts, that will be represented by w i : ⌊∆⌋.

µMALL also consider rules for equality and inequality but we do not need them in our developments.

It is useful to allow the state property to mention only a subset of the propositional variables in V. In that case, we can define [[p i (a i )]] as above if a i occurs in p and ⊤ otherwise.

We note that from a finite set of propositional variables, the set of states (containing, abs(x) or pres(x)) is finite. Hence, any infinite path in such LTS must have a loop.


Afshine Amidi

Shervine Amidi

Dimitrios Vlachakis

Nikos Paragios

Evangelia I Zacharaki

A machine learning methodology for enzyme functional classification combining structural and protein sequence descriptors

Keywords: enzyme classification, protein structure, amino acid sequence alignment, multi-class SVM, PDB database

The massive expansion of the worldwide Protein Data Bank (PDB) provides new opportunities for computational approaches which can learn from available data and extrapolate the knowledge into new coming instances. The aim of this work is to apply machine learning in order to train prediction models using data acquired by costly experimental procedures and perform enzyme functional classification. Enzymes constitute key pharmacological targets and the knowledge on the chemical reactions they catalyze is very important for the development of potent molecular agents that will either suppress or enhance the function of the given enzyme, thus modulating a pathogenicity, an illness or even the phenotype. Classification is performed on two levels: (i) using structural information into a Support Vector Machines (SVM) classifier and (ii) based on amino acid sequence alignment and Nearest Neighbor (NN) classification. The classification accuracy is increased by fusing the two classifiers and reaches 93.4% on a large dataset of 39,251 proteins from the PDB database. The method is very competitive with respect to accuracy of classification into the 6 enzymatic classes, while at the same time its computational cost during prediction is very small.

Introduction

Proteins are macromolecules which are made of amino acids. Although many distinct groups of proteins and protein families exist, enzymes constitute key pharmacological targets as their primary role is to catalyze chemical reactions. In contrast to most chemical catalysts which catalyze a wide range of reactions, enzymes are usually highly selective, catalyzing specific reactions only. The latter are classified into 6 standard categories, Oxidoreductases, Transferases, Hydrolases, Lyases, Isomerases, and Ligases, which are identified by their Enzyme Classification (EC) number.

Knowing the EC number of a given enzyme is necessary for the development of potent molecular agents. Having a large dataset of uniquely annotated (by experimental procedures) enzymes at disposal, the goal of this work is to build classification models that are able to predict the EC number of new enzymes with high precision, repeatability and small computational time. Previous work has been done on different datasets of enzymes. Dobson and Doig [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF] used only structural information and achieved an accuracy of 35% for topranked prediction using one-class versus one-class SVM on 498 enzymes from the PDB database. Others used only gene or amino acid sequences and achieved an accuracy stemming from 72.94% on the PDB database using neural network [START_REF] Osman | Hybrid Learning Algorithm in Neural Network System for Enzyme Classification[END_REF] to 96% using neural network on enzyme database [START_REF] Volpato | Accurate prediction of protein enzymatic class by N-to-1 Neural Networks[END_REF], but also accuracies between 74% [START_REF] Desjardins | Prediction of Enzyme Classification from Protein Sequence without the use of Sequence Similarity[END_REF] and 88.2% using the Swiss-Prot database [START_REF] Kumar | A top-down approach to classify enzyme functional class and sub-classes using random forest[END_REF] [START_REF] Lee | Classification of Enzyme Function from Protein Sequence based of Feature Representation[END_REF]. A systematic review on the various approaches used by different research groups, their utility and inference is presented in [START_REF] Sharma | Computational Approaches for Enzyme Functional Class Prediction: A Review[END_REF]. The methodologies have been classified according to the type of information used for descriptor generation into bioinformatics approaches and chemoinformatics approaches. In this paper we present a bioinformatics approach that exploits both structural representation and protein sequence similarity in order to predict in silico the EC number of an enzyme using machine learning techniques. The structure is encoded by the torsion angles distribution, whereas the protein sequence is characterized by its alignment error to training sequences in which the class label (EC number) is known. Structural information has been previously used either as validation criteria for newly generated models [START_REF] Read | A new generation of crystallographic validation tools for the protein data bank[END_REF] or during structure calculation to reproduce physically realistic conformational features [START_REF] Bermejo | Smooth statistical torsion angle potential derived from a large conformational database via adaptive kernel density estimation improves the quality of NMR protein structures[END_REF]. In the following we present the method, the results achieved, some discussion and future work.

Materials and methods

The outline of the method is shown in Fig. 1. Briefly, two supplementary descriptors are extracted from each protein model based on the structural information (SI) and the amino acid sequence (AA). Each descriptor is introduced into a classifier trained previously on annotated data and then the classifier outputs are fused into a single set of final class probabilities.

The method has been trained and tested on proteins from the PDB database. Enzymes that were found experimentally to catalyze more than one chemical reaction and were assigned multiple labels in the first level of the Enzyme Classification, were excluded from the analysis due to the uncertainty they introduce in both training and testing phase. Also PDB entries containing amino acids other than the 20 natural ones, were excluded from the AA analysis, as proper physicochemical parameterisation of Selenocysteine (U) and Pyrrolysine (O) was not part of this study. Same goes for ambiguous amino acids that are represented with the letters B, Z, J and X. We concluded that since the X-ray crystallogra-

Enzymes

Fusion of classifiers

Extraction of AA descriptors NN classification

Extraction of SI descriptors

SVM classification

Fig. 1. Overview of the method phy phases were incapable of giving a clear answer on which amino acid it is and provided that there were thousands of such cases in the full PDB dataset, we would introduce non-quantifiable "noise" to our dataset, which would inevitably sabotage the reliability of our findings.

The functional classes and number of enzymes obtained per class is shown in table 1.

Feature extraction

Proteins are chains of amino acids joined together by peptide bonds. The threedimensional (3D) configuration of the amino acids chain is a very good predictor of protein function, thus there has been many efforts in extracting an appropriate representation of the 3D structure [START_REF] Lie | 3D representations of amino acids-applications to protein sequence comparison and classification[END_REF]. Since many conformations of this chain are possible due to the possible rotation of the chain about each carbon (C α ) atom, the use of rotation invariant features is preferred over features based on cartesian coordinates of the atoms. In this study the two torsion angles of the polypeptide chain were used as structural features. The two torsion angles describe the rotation of the polypeptide backbone around the bonds between N-C α (angle φ) and C α -C (angle ψ). The probability density of the torsion angles φ and ψ ∈ [-180 • , 180 • ] was estimated by calculating the 2D sample histogram of the angles of all residues in the protein using equal sized bins. When the protein consisted of more than one chain, the torsion angles of all chains were included into the feature vector. Smoothness in the density function was achieved by moving average filtering, i.e. by convoluting the 2D histogram with a uniform kernel. The range of angles was discretized using 19 × 19 bins centered at 0 • (with bin size equal to 20 • for all bins except the 1 st and last) and the obtained matrix of structural features was linearized to a 361-dimensional feature vector for each enzyme.

The structural description based on the probability density of the torsion angles does not provide any information about the spatial location of the amino acids in the chain, as well as their sequence. The connectivity patterns (protein sequence) reflects the intrinsic composition of the macromolecule and is an important descriptor of spatial composition. Many methods have been developed to quantify the similarity between two protein sequences which are either based on sequence alignment [START_REF] Sharif | Enzyme Function Classification Based on Sequence Alignment[END_REF] or provide a similarity score without performing prior alignment [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF]. A common algorithm that provides a similarity score to each pair of sequences is the Smith-Waterman algorithm [START_REF] Jensen | Prediction of Human Protein Function from Post-translational Modifications and Localization Features[END_REF]. The Smith-Waterman algorithm calculates the optimal local alignment of two sequences by computing a similarity matrix that takes into account matches, mismatches, substitutions, insertions and deletions between the two sequences [START_REF] Smith | Identification of common molecular subsequences[END_REF]. Based on this algorithm, a score S(i, j) between each pair of sequences i and j was obtained and used to calculate the class probability of a sequence based on nearest neighbor classification rule.

Classification using structural and amino acid sequence information

For a given enzyme, the 361 obtained features representing the protein's structural conformation were introduced into a multi-class SVM to obtain 6 probabilistic output features. A one-versus-all classification scheme was applied in which 6 binary classifications are performed (class i versus not class i) and combined by majority voting rule to decide which of the 6 classes is the most probable. Since the SVM's decision scores are not reflecting probabilities, an additional sigmoid function was fitted to the data in order to map the SVM outputs into pseudo-probabilities [START_REF] Platt | Probabilistic Outputs for Support Vector Machines and Comparison to Regularized Likelihood Methods[END_REF]. The latter are noted (p j i ) i∈[ [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF][START_REF] Lee | Classification of Enzyme Function from Protein Sequence based of Feature Representation[END_REF]] , with p j i reflecting the probability for the enzyme j to belong to the class EC i.

In order to allow the fusion of classifiers, the scores of amino acid sequence alignment (matrix S) were also converted to pseudo-probabilistic output for the second classifier. Specifically, for a given enzyme j, the nearest neighbor of each class was found using as distance measure the alignment scores with the training samples. The alignment scores between the enzyme j and the 6 neighbors were normalized by the sum of their scores:

For each enzyme j, q j i = max

k∈training EC i k =j S(k, j) 6 l=1 max k∈training EC l k =j S(k, j)
Thus the classifier decision scores for both descriptors were appropriately scaled, such that 6 i=1 p j i = 6 i=1 q j i = 1, and allowed to be combined within a fusion scheme.

Fusion of classifiers

It has been shown that fusion techniques that combine multiple machine learning methods achieve better predictive performance than any of the constituent methods [START_REF] Mohammed | Application of a hierarchical enzyme classification method reveals the role of gut microbiome in human metabolism[END_REF]. In this work we combine the probabilistic output of each classifier, i.e. the SVM based on structural information and the nearest neighbor based on protein sequence alignment. The classification fusion is constructed by fusing the two probabilistic outputs (p j i ) and (q j i ) for each class i through a linear combination into a final probability (z j i ):

For each enzyme j, ∀i ∈ [[1 , 6]], z j i = (1 -α)p j i + αq j i
where α ∈ [0, 1] is a weight that regulates the contribution of each classifier. Thus, the problem is to find the optimal parameter α that maximizes the overall classification accuracy.

Validation scheme

The dataset was randomly split into 80% for training and 20% for testing. In order to determine the optimum α, 20% of the training set has been hold out and used as validation set, while the remaining part was used to train the classifier.

Upon selection of α based on the validation set, the classifier was retrained using the whole training set, and the optimum α was used to assess accuracy of the fusion on the testing set. The assessment of the multi-class system was based on the confusion matrix. However, the performance of the system was also evaluated in respect to the cumulative accuracy after i guesses, noted CA i (i ∈ [ [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF][START_REF] Kumar | A top-down approach to classify enzyme functional class and sub-classes using random forest[END_REF]]), which represents the classification accuracy after looking at the i highest class probabilities.

Results

Structural information and amino acid sequences

Table 2 shows the cumulative accuracy (CA1 to CA5) for each enzymatic class and each descriptor separately. Classification with amino acid sequences yields from 12,2% (EC 3) to 49,2% (EC 6) better accuracy than classification with structural information. The accuracy difference between those two approaches might indicate that amino acid sequence content (with 93.4% overall accuracy) is a better predictor of enzyme function than structural information (with 73.5% overall accuracy).

Fusion of both information

Table 3 shows the most often predicted class by each method after each guess.

It can be seen that the order of predicted classes varies when different features (SI and AA) are used for classification denoting that each descriptor captures different aspects of enzymatic function.

The fusion of information relies on the study of the function α → Acc(α), where Acc is the accuracy on the validation set obtained by weighting the probabilities obtained by the SI-based and AA-based classifiers. Fig. 2 illustrates the classification accuracy in the interval α ∈ [0.8, 1]. The value that maximizes the accuracy is α = 0.94 and was chosen for the assessment of the method on the testing dataset. As expected, the optimum α gives a more significant weight to amino acid sequences descriptors than to structural information descriptors.

The total cumulative accuracy (for multiple guesses) is shown in Fig. 3 for each of the three methods, while Fig. 4 illustrates the cumulative accuracy for each enzymatic class separately. For Transferases and Hydrolases the fusion of features induced an average increase of accuracy by 1% on each guess compared to the accuracy obtained by amino acid sequences only. For the other classes, the accuracy of the fusion is comparable to the accuracy by AA indicating that structural information does not additionaly contribute to classification. Fig. 5 shows the confusion matrix of the classification fusion. The confusion matrix allows to see whether an enzyme class is more or less predictable and shows how the classification error is distributed among classes. Each row of the confusion matrix has been normalized so that coefficient (i,j) represents the proportion of enzymes from class EC i that are predicted as belonging to EC j. The highest misclassification rates are observed for Ligases with 10.4% of them classified as Transferases and 6.5% as Hydrolases. Conversely, Oxidoreductases, Transferases and Hydrolases have very small misclassification rates.

The code was written in Matlab language and was performed using High-Performance Computing (HPC) resources from the "mesocentre" computing center of École Centrale de Paris (http://www.mesocentre.ecp.fr) supported by CNRS. Running on 2 Intel X5650 with 4GB RAM, the computational time

Conclusions

The bioinformatics bottleneck is a major problem in the fields of Next Generation Sequencing (NGS) and Drug Design (DD). Data accumulation is becoming a challenge on its own as the handling and analysis of huge datasets is not a trivial task. Therefore there is dear need in the field of bioinformatics to establish and optimize new methodologies that are faster and much more efficient for routine tasks in the aforementioned fields. A major drawback in protein classification is the fact that protein similarity is still judged upon primary sequence comparisons rather than combining structural information too. Using structural information was quite challenging a while ago as significant computing power was required. However, nowadays it is not too difficult to use optimized workstations and supercomputers to analyze all structural information available. Remarkably, the RCSB PDB database has now more than 114,000 entries. In 1990 there were only 507 structures available and in 2000 only 13,591 structures. Quick and reliable classification of NGS generated sequences is of paramount importance in the field of DD, as the problem of pharmacological target identification still holds. Classifying quickly and reliably, the several thousands of proteins that are being identified and sequenced on a daily basis would lead to an optimized pipeline that could yield results of great interest to protein science, DD and NGS related fields such as anticancer and antiviral therapy.

The proposed approach is fully automated, reproducible and computationally very efficient during prediction phase. Also the achieved accuracy (73.5%) by the SVM classifier based on structural information is significantly higher than the reported accuracy (35%) of the SVM classifier by Dobson and Doig [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF] based also on protein structure. We used the torsion angles distribution to represent structure, whereas in [START_REF] Dobson | Predicting Enzyme Class From Protein Structure Without Alignments[END_REF] 55 structural attributes were originally extracted, including residue fractions, surface fractions, secondary structure content, cofactors, metals and general properties. Then attribute subset selection was applied based on backwards elimination.

Furthermore, the weighted combination of classifiers in the proposed scheme led to a significant increase of accuracy (27.1% for the first guess) relatively to the classification performed using only structural information, while the accuracy increase relatively to the AA-based classification was only marginal (0.9%). The trend is similar for the cumulative accuracy with multiple guesses. As can be seen from Fig. 3, the classification fusion performs better in respect to the cumulative accuracy with multiple guesses than the single classifiers.

The two classes that showed the best results after fusion (Transferases and Hydrolases) are the ones which have the largest number of samples in the dataset. This could be related to the selection of α through maximization of overall accuracy which is biased towards the majority classes. It is well known that most machine learning techniques rely on balanced datasets in which each class includes the same number of samples. In the future, we plan to investigate bootstrapping and data aggregation techniques [START_REF] Chawla | Data mining for imbalanced datasets: an overview[END_REF] which provide efficient solutions to unbalanced datasets.

Moreover, in the current study, we investigated two common supervised classification techniques, the nearest neighbor and SVM. The nearest neighbor is a very simple classifier often used as baseline to assess the necessity of more advanced tools. SVM is a very popular algorithm due to its ability to capture complex relationships between the datapoints and its high predictive power. Also the number of required hyper-parameters to be optimized in SVM is small (usually 2, i.e. the parameters controlling the misclassification penalty and smoothness), and thus quite easy to tune even by manual search or grid-search. Ongoing work includes the investigation of different classifiers, in terms of accuracy and performance.

Acknowledgment

This research was partially supported by European Research Council Grant Diocles (ERC-STG-259112).

Fig. 2 .

 2 Fig. 2. Classification accuracy on the validation dataset as a function of the weight α

Fig. 3 .Fig. 4 .

 34 Fig. 3. Comparison of the overall CA between the 3 methods

Fig. 5 .

 5 Fig. 5. Confusion matrix

Table 1 .

 1 Enzyme Classification of the 39,251 enzymes

	ID	EC 1	EC 2	EC 3	EC 4	EC 5	EC 6
	Name	Oxidoreductase Transferase Hydrolase Lyase Isomerase Ligase
	Number	7,256	10,665	15,451	2,694	1,642	1,543

Table 2 .

 2 CA using structural information and amino-acid sequences separately

		Structural information	Amino acid sequence
	Category CA1 CA2 CA3 CA4 CA5 CA1 CA2 CA3 CA4 CA5
	EC 1	0.746 0.884 0.943 0.977 0.992 0.967 0.988 0.996 0.999 1.000
	EC 2	0.762 0.920 0.970 0.990 0.997 0.937 0.964 0.977 0.996 1.000
	EC 3	0.798 0.909 0.961 0.982 0.994 0.920 0.958 0.975 0.992 0.999
	EC 4	0.596 0.685 0.790 0.900 0.950 0.892 0.922 0.944 0.983 0.993
	EC 5	0.547 0.635 0.730 0.827 0.939 0.900 0.954 0.970 0.976 0.979
	EC 6	0.304 0.476 0.605 0.822 0.926 0.796 0.822 0.841 0.871 0.964
	Overall	0.735 0.864 0.924 0.965 0.986 0.934 0.966 0.979 0.993 0.998

Table 3 .

 3 Most representative guesses for each true class

	Guesses