# Hybrid Linear Logic, revisited

Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux

► To cite this version:

Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, In press, 10.1017/S0960129518000439. hal-01968154

HAL Id: hal-01968154

https://inria.hal.science/hal-01968154

Submitted on 2 Jan 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Hybrid Linear Logic, revisited

Kaustuv Chaudhuri

Inria & LIX/École polytechnique, France

Joëlle Despeyroux

Inria and CNRS, I3S, Sophia-Antipolis, France

Carlos Olarte

ECT – Universidade Federal do Rio Grande do Norte. Brazil

Elaine Pimentel

Departamento de Matemática – Universidade Federal do Rio Grande do Norte. Brazil

Accepted to MSCS: November 8, 2018

Abstract

HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgments are labelled by worlds (having a monoidal structure) and hybrid connectives (`at` and `↓`) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the linear logic exponentials (`!`, `?`) are decorated with labels representing *locations*, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL<sup>®</sup> (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (`μHyMALL`), which can be encoded into multiplicative additive linear logic with fixed points (`μMALL`). As an application, we propose encodings of Computational Tree Logic (CTL) into both `μMALL` and `μHyMALL`. In the former, states are represented as atoms in the linear context, hence reflecting a more *operational* view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the *semantics* of CTL.

# 1 Introduction

Logical frameworks are adequate tools for specifying proof systems, since they support levels of abstraction that facilitate writing declarative specifications of object-level logical systems. Thus designing suitable logical frameworks for adequately specifying different proof systems has become one of the main tasks for many logicians working in computer science.

Among the many frameworks that have been used for the specification of proof systems, linear logic [Gir87] (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, [MP13, CP02]). However, since specifications of object-level systems into the logical framework should be natural and direct, there are some features that often cannot be adequately captured in LL, e.g. modalities different from the ones present in LL.

Extensions of LL, or its intuitionistic version ILL [Gir87], have been proposed in order to fill this gap, hence having stronger logical frameworks that preserve the elegant properties of linear logic as the underlying logic. Two of such extensions are HyLL (Hybrid Linear Logic) [DC14], an extension of ILL, and SELL (Subexponential Linear Logic) [DJS93, NM09], an extension of ILL/LL<fnref n="1" />. 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

<footnote n="1">¹Intuitionistic and classical SELL are equally expressive [Cha10].</footnote>
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 [DC14, dMDF14].

In SELL, the LL exponentials (!, ?) are decorated with labels: the formula ?ªA can be interpreted as A holds in a location, modality, or world a. Such labels are organized in a pre-order, so that if A holds in a, then it can be deduced in any location b smaller then a. Moreover, the formula ?ª!ª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 [NOP17]. 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., !ª?c?d). For this, SELL enhances the expressive power of LL as a logical framework.

Since HyLL and SELL share LL/ILL as the base logic, it is reasonable to investigate the relationship between worlds and locations. The first contribution of this work is a careful comparison study of LL, HyLL and SELL. We start by showing a direct encoding of the HyLL's logical rules into LL with the highest level of adequacy, namely, on the level of derivations [NM10]. This means that there is a 1-1 relation between the set of derivations in HyLL with the set of their interpretations in LL.

We then propose an encoding of HyLL into SELL<sup>∞</sup> (SELL with quantification over locations [NOP13, NOP17]) that gives better insights about the meaning of worlds in HyLL. More precisely, we represent HyLL worlds as locations in SELL and encode HyLL into SELL<sup>∞</sup>. 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.

It is worthy noticing that, in HyLL, using judgments that attach formulas to worlds provides a neat tool for specifying systems with modalities (see e.g., the models of biological systems in [dMDF14]). An elegant property of these models is that, in the same logical framework, it is possible to model the system and also the properties of interest. This is done by first specifying in (a fragment of) Computational Tree Logic (CTL) the desired property and then encoding it as a HyLL formula.

The next contribution of this paper is to show that neither the universal CTL path quantifier A (for all paths), nor the temporal CTL formula EGF (there exists a path where F always holds) can be encoded in HyLL. The main reason is that the definition of such formulas is recursive and hence, one needs to use induction, at the meta-level, to accurately capture their behavior. Instead of using meta-reasoning, as done in [dMDF14], we show that CTL formulas can be encoded into multiplicative, additive linear logic with fixed points (µMALL) [Bae12]. For that, we specify the (current) state of the transition system (Kripke structure) as atoms in the linear context and, following the fixed point characterization of CTL [BCM+92], we encode the whole set of CTL formulas. Such encoding gives a sort of *operational* view of the CTL connectives: when a fixed point formula is unfolded, the current state *s* is consumed and the resulting premises in the derivation represent some (or all) the successor states from *s* where the given CTL formula must be proved again. Hence, in order to accurately represent the state transitions as µMALL derivations, the encoding is parametric in the given Kripke structure and it internalizes the accessibility relation as conjunctions/disjunctions on all possible transitions.

In order to give a more loosely coupled encoding with respect to the transition system, we add fixed point operators to multiplicative, additive HyLL (µHyMALL) and present an encoding of CTL into this system. In this case, worlds in HyLL represent states of the transition system and the encoding of CTL connectives quantifies and *moves* formulas on those worlds. Hence, the resulting encoding has a pleasant duality with the semantics of CTL.

The rest of the paper is organized as follows. We briefly recall LL in Section 2.1 and HyLL in Section 2.2. The encoding of HyLL logical rules into LL is discussed in Section 3.1. Section 3.2 presents the encoding of HyLL into SELL<sup>∞</sup>. We also prove that information confinement, a feature in SELL that is needed to specify spatial systems, cannot be captured in HyLL. Section 4 proposes the system µHyMALL, that enhances multiplicative, additive HyLL with fixed points. The encodings of CTL into µMALL and µHyMALL are described in Sections 5.2 and 5.3 respectively. Section 6 concludes the paper.

This paper is an extended version of [DOP17]. In the present paper we not only refine several technical details from that work but we also add the notion of fixed points to HyLL. In [DOP17] we used the well known system µMALL for showing an encoding of CTL into linear logic (with fixed points). Although this entails a correct specification, the encoding is itself complex. Our new encoding of CTL into µHyMALL is not only simpler, but closer to the semantical specification of CTL itself. Moreover, the representation of the transition system is less coupled than the one in [DOP17], thus allowing us to prove meta-theoretical properties of CTL inside the same logical framework.

## 2 Preliminaries

In this section we review some of the basic proof theory for linear logic LL [Gir87] and hybrid linear logic HyLL [DC14].

### 2.1 Linear Logic and Focusing

By the name LL we shall mean the logic that results from merging the logical connectives and proof rules of linear logic [Gir87] with the term and quantificational structure of Church's Simple Theory of Types [Chu40]. More precisely, simple types are either *primitive types*, of which ◦ is a reserved primitive type denoting formulas, or *functional types* that are
written using an infix arrow $\tau \to \tau'$. A type is a *predicate type* if it is of the form $\tau_1 \to \dots \to \tau_n \to \emptyset$, where $n \ge 0$. *Terms* are simply typed $\lambda$-terms and we identify two terms up to the usual $\alpha, \beta$, and $\eta$-conversions. The substitution notation $B[t/x]$ denotes the $\lambda$-normal form of the $\beta$-redex $(\lambda x.B)t$.

The set of linear logic formulas is given by the following grammar:

$$F, G ::= p(\vec{t}) \mid p(\vec{t})^{\perp} \mid 1 \mid \mathbf{0} \mid \top \mid \bot \mid F \otimes G \mid F \not\exists G \mid F \& G \mid F \oplus G \mid \exists_{\tau} x.F \mid \forall_{\tau} x.F \mid ?F \mid !F$$

where atomic propositions are applied to a sequence of terms. The logical connectives for LL can be divided into the following groups: the *multiplicative* version of conjunction, true, disjunction, and false, which are written as $\otimes$, $\oplus$, $\perp$, respectively; and the *additive* version of these connectives, which are written as $\&$, $\top$, $\oplus$, $\mathbf{0}$, respectively; the *exponentials* $!$ and $?$; and the (typed) universal and existential *quantifiers* $\forall_{\tau}$ and $\exists_{\tau}$. In the quantifiers, the syntactic variable $\tau$ can range over all non-predicate types: $\forall_{\tau}$ and $\exists_{\tau}$ both have type $(\tau \to o) \to o$. The expressions $\forall_{\tau}\lambda x.B$ and $\exists_{\tau}\lambda x.B$ are abbreviated as the more usual $\forall_{\tau}x.B$ and $\exists_{\tau}x.B$. From this point on, we will drop the subscript $\tau$ when it is not important or it can be determined from context. Formulas are taken to be in *negation normal form* using the standard classical linear logic dualities, e.g., $(F \otimes G)^{\perp} \equiv F^{\perp} \not\exists G^{\perp}$. Hence negation in LL has only atomic scope.

First proposed by Andreoli [And92] 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: *negative* ($\not\exists$, $\perp$, $\&$, $\top$, $\forall$, $?$) and *positive* ($\otimes$, $1$, $\oplus$, $\mathbf{0}$, $\exists$, $!$). Note that the dual of a negative connective is positive and vice-versa. In general, the introduction rules for negative connectives are all invertible, meaning that the conclusion of any of these introduction rules is equivalent to its premises. The introduction rules for the positive connectives are not necessarily invertible. The notions of negative and positive polarities are extended to formulas in the natural way by considering the outermost connective. Although any bias can be assigned to atomic formulas, this work will consider only *negative* atoms.

The focused system LLF for classical linear logic is presented in Figure 1. There are two kinds of arrows in this proof system: $\downarrow$ and $\uparrow$, and a pair of contexts to the left of the arrows: $\Gamma$ is a set of formulas whose main connective is a question-mark (being hence the unbounded context), while $\Delta$ is a multi-set of linear formulas, behaving as the bounded context. Sequents with the $\downarrow$ arrow belong to the positive phase and introduce the logical connective of the “focused” formula (the one to the right of the arrow). Building proofs of such sequents may require non-invertible proof steps to be taken. Sequents with the $\uparrow$ arrow belong to the negative phase and decompose the multiset of formulas on the right of the arrow in such a way that only inference rules over negative formulas are applied; the others are “stored” in the linear context using the rule $R \uparrow$. The structural rules $D_1, D_2$ and $R \downarrow$ make the transition between negative and positive phases. The *positive phase* begins by choosing a positive formula $F$ on which to focus (using $D_1, D_2$). 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 and the proof switches to the negative phase (using $R \downarrow$).

This change of phases on proof search is particularly interesting when the focused formula is a *bipole* [And92].

**Definition 2.1 (Bipoles).** 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.

Using the linear logic distributive properties, monopoles are equivalent to formulas of the form

$$\forall x_1 \dots \forall x_p [\&_{i=1,\dots,n} \not\exists_{j=1,\dots,m_i} F_{i,j}],$$

where the $F_{i,j}$ are either atoms or the result of applying $?$ to an atomic formula. Similarly, bipoles can be rewritten as formulas of the form

$$\exists x_1 \dots \exists x_p [\bigoplus_{i=1,\dots,n} \otimes_{j=1,\dots,m_i} G_{i,j}],$$

where $G_{i,j}$ are either negated atoms, monopole formulas, or the result of applying $!$ to a monopole formula. Notice that the units $\top$, $\mathbf{0}$, $\perp$, and $1$ are 0-ary versions of $\&$, $\oplus$, $\not\exists$, and $\otimes$, respectively.

Given this normal representation of bipoles and according to the focusing discipline, it turns out that, once introduced, a bipole is completely decomposed into its atomic subformulas, a fact illustrated by the following bipole derivation.

$$\frac{\frac{\frac{\Gamma'; \Delta' \Uparrow \cdot \dots \quad [\not\exists, ?, R \Uparrow]}{\Gamma; \Delta' \Uparrow \not\exists_{j=1,\dots,m_i} ?p_{i,j}} \dots}{\Gamma; \Delta' \Uparrow \forall x_1 \dots \forall x_p [\&_{i=1,\dots,n} \not\exists_{j=1,\dots,m_i} ?p_{i,j}]} [\forall, &]}{\Gamma; \Delta' \Uparrow ! \forall x_1 \dots \forall x_p [\&_{i=1,\dots,n} \not\exists_{j=1,\dots,m_i} ?p_{i,j}]} [!]}{\dots} \frac{\Gamma; \Delta \Downarrow \exists x_1 \dots \exists x_t [\bigoplus_{i=1,\dots,k} \otimes_{j=1,\dots,q_i} G_{i,j}]}{\Gamma; \Delta \Downarrow \exists x_1 \dots \exists x_t [\bigoplus_{i=1,\dots,k} \otimes_{j=1,\dots,q_i} G_{i,j}]} [\exists, \oplus, \otimes]$$

Here $p_{i,j}$ is atomic for all $i, j$. If the connective $!$ is not present, then the rule $!$ is replaced by the rule $R \downarrow$. Notice that the derivation above contains a single positive and a single negative phase. This two phase decomposition will enable us to adequately capture the application of object-level inference rules as will be shown in Section 3.
Judgmental rules

$$ \frac{\Gamma; p(\vec{t}) @ w \vdash p(\vec{t}) @ w}{[init]} \qquad \frac{\Gamma, A @ u; \Delta, A @ u \vdash C @ w}{\Gamma, A @ u; \Delta \vdash C @ w} [copy] $$

Multiplicative rules

$$ \frac{\Gamma; \Delta \vdash A @ w \quad \Gamma; \Delta' \vdash B @ w}{\Gamma; \Delta, \Delta' \vdash A \otimes B @ w} [\otimes R] \qquad \frac{\Gamma; \Delta, A @ u, B @ u \vdash C @ w}{\Gamma; \Delta, A \otimes B @ u \vdash C @ w} [\otimes L] $$

$$ \frac{\Gamma; \cdot \vdash 1 @ w}{[1R]} \qquad \frac{\Gamma; \Delta \vdash C @ w}{\Gamma; \Delta, 1 @ u \vdash C @ w} [1L] $$

$$ \frac{\Gamma; \Delta, A @ w \vdash B @ w}{\Gamma; \Delta \vdash A \neg B @ w} [-\circ R] \qquad \frac{\Gamma; \Delta \vdash A @ u \quad \Gamma; \Delta', B @ u \vdash C @ w}{\Gamma; \Delta, \Delta', A \neg B @ u \vdash C @ w} [-\circ L] $$

Additive rules

$$ \frac{\Gamma; \Delta \vdash \top @ w}{[\top R]} \qquad \frac{\Gamma; \Delta, 0 @ u \vdash C @ w}{[0L]} $$

$$ \frac{\Gamma; \Delta \vdash A @ w \quad \Gamma; \Delta \vdash B @ w}{\Gamma; \Delta \vdash A \& B @ w} [&R] \qquad \frac{\Gamma; \Delta, A_i @ u \vdash C @ w}{\Gamma; \Delta, A_1 \& A_2 @ u \vdash C @ w} [&L_i] $$

$$ \frac{\Gamma; \Delta \vdash A_i @ w}{\Gamma; \Delta \vdash A_1 \oplus A_2 @ w} [\oplus R_i] \qquad \frac{\Gamma; \Delta, A @ u \vdash C @ w \quad \Gamma; \Delta, B @ u \vdash C @ w}{\Gamma; \Delta, A \oplus B @ u \vdash C @ w} [\oplus L] $$

Quantifier rules

$$ \frac{\Gamma; \Delta \vdash A @ w}{\Gamma; \Delta \vdash \forall \alpha. A @ w} [\forall R] \qquad \frac{\Gamma; \Delta, A[\tau/\alpha] @ u \vdash C @ w}{\Gamma; \Delta, \forall \alpha. A @ u \vdash C @ w} [\forall L] $$

$$ \frac{\Gamma; \Delta \vdash A[\tau/\alpha] @ w}{\Gamma; \Delta \vdash \exists \alpha. A @ w} [\exists R] \qquad \frac{\Gamma; \Delta, A @ u \vdash C @ w}{\Gamma; \Delta, \exists \alpha. A @ u \vdash C @ w} [\exists L] $$

In $\forall R$ and $\exists L$, $\alpha$ is assumed to be fresh with respect to $\Gamma$, $\Delta$, and $C$.

In $\exists R$ and $\forall L$, $\tau$ stands for a term or world, as appropriate.

Exponential rules

$$ \frac{\Gamma; \cdot \vdash A @ w}{\Gamma; \cdot \vdash !A @ w} [!R] \qquad \frac{\Gamma, A @ u; \Delta \vdash C @ w}{\Gamma; \Delta, !A @ u \vdash C @ w} [!L] $$

Hybrid connectives

$$ \frac{\Gamma; \Delta \vdash A @ u}{\Gamma; \Delta \vdash (A \ at \ u) @ w} [at R] \qquad \frac{\Gamma; \Delta, A @ u \vdash C @ w}{\Gamma; \Delta, (A \ at \ u) @ v \vdash C @ w} [at L] $$

$$ \frac{\Gamma; \Delta \vdash A[w/u] @ w}{\Gamma; \Delta \vdash \downarrow u.A @ w} [\downarrow R] \qquad \frac{\Gamma; \Delta, A[v/u] @ v \vdash C @ w}{\Gamma; \Delta, \downarrow u.A @ v \vdash C @ w} [\downarrow L] $$

<caption>Figure 2: The sequent calculus for HyLL.</caption>
The inference rules are depicted in Figure 2. Note that (A at u) is a mobile proposition: it carries with it the world at which it is true. Both introduction rules for the other hybrid connective, ↓, bind the current world. Weakening and contraction are admissible rules for the unbounded context.

The most important structural properties are the admissibility of the general identity 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 2.1 (Identity/Cut [DC14]).** 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 5) is not definable in S5.

Finally, we also note that HyLL admits a complete focused proof system. The interested reader can find proofs and further meta-theoretical theorems about HyLL in [DC14].

3 Relative Expressiveness Power of HyLL

Different frameworks can be more or less adequate for specifying different systems. While very specific frameworks often provide better encodings for a small range of systems, general frameworks can handle more systems, sometimes not efficiently or in a natural way. Therefore, finding frameworks that are general enough while still adequate and efficient is a key issue. With that in mind, we will compare HyLL with two other LL based frameworks: LL itself and linear logic with subexponentials (SELL).

We start by proving that HyLL's axioms and rules can be adequately specified in LL. It turns out that any interpretation of a system into another must be *adequate*, in the sense that there must be a 1-1 relation between the sets of interpreted objects with the set of their interpretations. The *level of adequacy* can then determine how tight are those systems. We show that our encoding has the highest possible level of adequacy (on the level of derivations – see [NM10]), so that one step of derivation in HyLL corresponds to one focused step in LL. This means that every proof in HyLL can be exactly mimicked by a derivation in LLF. We note, however, that HyLL enables for more semantical driven specifications when compared to LL, as it will be discussed in Section 5.

Since linear logic with subexponentials (SELL) is a conservative extension of LL, the specification of HyLL into LL trivially implies that HyLL can be similarly encoded in SELL as well. Our approach in Section 3.2, however, will be entirely different: we will interpret worlds as subexponentials, hence having a better meta level understanding of the behavior of worlds in HyLL.

3.1 HyLL and LL

We briefly recapitulate the basic concepts of the specification of sequent-style calculi in LLF (see [MP13] for a more detailed presentation). Let $obj$ be the type of object-level formulas and let $\llbracket \cdot \rrbracket$, $\lfloor \cdot \rfloor$, and $\lceil \cdot \rceil$ be meta-level predicates of type $obj \to \circ$, where $\circ$ is the primitive type denoting formulas. HyLL sequents of the form $\Gamma; \Delta \vdash C$ will be encoded in LL as $?\llbracket \Gamma \rrbracket ?\lceil \Delta \rceil ?\lfloor C \rfloor$ where, if $\Psi = \{F_1, ..., F_n\}$, then $\lfloor \Psi \rfloor = \lfloor F_1 \rfloor ?\dots ?\lceil F_n \rceil$ and $?\llbracket \Psi \rrbracket = ?\llbracket F_1 \rrbracket ?\dots ?\lceil F_n \rceil$. In that way, the $\lfloor \cdot \rfloor$ and $\lceil \cdot \rceil$ predicates identify which object-level formulas appear on which side of the sequent: brackets down for left (useful mnemonic: $\lfloor$ for “left”) and brackets up for right, while the double brackets $\llbracket \cdot \rrbracket$ identify formulas in the (left) unbounded context.

Inference rules are specified as 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 (⊗). As a matter of example, the additive version of the inference rules for conjunction in intuitionistic logic

$$
\frac{\Gamma, A \to C}{\Gamma, A \land B \to C} \wedge_{L1} \frac{\Gamma, B \to C}{\Gamma, A \land B \to C} \wedge_{L2} \frac{\Gamma \to A \quad \Gamma \to B}{\Gamma \to A \land B} \wedge_R
$$

can be specified as the following bipoles:

$$
\wedge_L : \exists A, B. (\lfloor A \wedge B \rfloor^{\perp} \otimes (\lfloor A \rfloor \oplus \lfloor B \rfloor)) \quad \wedge_R : \exists A, B. (\lfloor A \wedge B \rfloor^{\perp} \otimes (\lfloor A \rfloor \& \lfloor B \rfloor))
$$

The following definition shows how to encode HyLL inference rules into LL.

**Definition 3.1 (HyLL rules into LL).** Let w, d, h and ◦ denote, respectively, the types for worlds, (first-order) objects, HyLL formulas and LL formulas. Let $\lceil \cdot \rceil$, $\lfloor \cdot \rfloor$ and $\llbracket \cdot \rrbracket$ be predicates of the type $h \to w \to \circ$ and A, B, C have, respectively, types $w \to h$, $d \to h$ and $h$. The encoding of HyLL inference rules into LL is depicted in Figure 3 (we omit the encoding of most of the linear logic connectives that can be found in [MP13]).
We shall use $a, b, \dots$ to range over elements in $I$ and we will assume that $\leq$ is upwardly closed with respect to $U$, i.e., if $a \in U$ and $a \leq b$, then $b \in 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 subexponentials labeled with $a \in I$

$$ \vdash ?^{a_1} F_1, \dots, ?^{a_n} F_n, G \quad \vdash ?^{a_1} F_1, \dots, ?^{a_n} F_n, !^a G \quad !^a \quad \vdash \Delta, G \quad ?^a $$

where the rule $!^a$ has the side condition that $a \leq a_i$ for all $i$. Moreover, for all indices $a \in U$, we add the usual rules of weakening and contraction to $?^a$.

We can enhance the expressiveness of SELL with the subexponential quantifiers $\oplus$ and $\wp^3$ [NOP17] given by the rules (omitting the subexponential signature)

$$ \vdash \Delta, G[l_e/l_x] \quad \vdash \Delta, \oplus l_x : a.G \quad \oplus \quad \vdash \Delta, \wp l_x : a.G \quad \wp $$

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 \leq a$. We call the resulting system SELL$^\oplus$.

SELL$^\oplus$ admits a cut-free, complete focused proof system (Figure 4). The sequent notation is close to the one for LLF and differs only on the treatment of contexts. SELL$^\oplus$ makes use of indexed contexts $\mathcal{K}$ that maps a subexponential index to multiset of formulas, e.g., if $s$ is a subexponential index, then $\mathcal{K}[s]$ is a multiset of formulas, where intuitively they are all marked with $?^s$. That is, $\mathcal{K}[s] = \{F_1, \dots, F_n\}$ should be interpreted as the multiset of formulas $?^s F_1, \dots, ?^s F_n$. We also make use of the operations on contexts depicted in Figure 5. Most of the operations are straightforward. For instance, $(\mathcal{K}_1 \otimes \mathcal{K}_2)[s]$, used to specify the tensor introduction rule $(\otimes)$, is defined as follows: when $s$ is a bounded subexponential index, $(\mathcal{K}_1 \otimes \mathcal{K}_2)[s]$ is obtained by multiset union of $\mathcal{K}_1[s]$ and $\mathcal{K}_2[s]$; when $s$ is an unbounded subexponential index, then it is $\mathcal{K}_1[s]$.<fnref n="4" /> On the other side, for the promotion rule, we use the operation $\mathcal{K} \leq_l$ that restricts the indexed context $\mathcal{K}$ to the formulas marked with a subexponentials greater than $l$. Hence, $\mathcal{K} \leq_l [s] = \mathcal{K}[s]$ if $l \leq s$ and $\mathcal{K} \leq_l [s] = \emptyset$ otherwise.

By using different prefixes, SELL$^\oplus$ is an adequate framework 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 [NPR11]; to specify systems with temporal, epistemic and spatial modalities [NOP13, OPN15, NOP17] and soft-constraints or preferences [PON14]; to specify Bigraphs [CR15]; and to specify and verify biological [OCFH16] and multimedia interacting systems [ADOR15].

Linear logic allows for the specification of two kinds of context maintenance: both weakening and contraction are available (unbounded 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 unbounded HyLL judgments and the unbounded LL context.

Encoding HyLL into SELL$^\oplus$ allows for a better understanding of worlds in HyLL. More precisely, we use subexponentials to represent worlds, where each world $w$ has its own linear and unbounded contexts, represented as $w$ and $c_w$, respectively. Hence, a HyLL judgment of the shape $F@w$ in the (left) linear context is encoded as the SELL$^\oplus$ formula $?^w \llcorner F@w$. That is, HyLL judgments that hold at world $w$ are stored at the $w$ linear context of SELL$^\oplus$. A judgment of the form $G@w$ in the unbounded HyLL context is encoded as the SELL$^\oplus$ formula $?^{c_w} \llcorner G@w$. Thus the encoding of $G@w$ is stored in the unbounded subexponential context $c_w$.

The next definition introduces the encoding of HyLL inference rules into SELL$^\oplus$. Observe that, surprisingly, the subexponential structure needed is flat on worlds, hence not reflecting their monoidal structure. This is explained by the fact that worlds in HyLL do not control the context on rules as the promotion rule in SELL does.

**Definition 3.2** (HyLL rules into SELL$^\oplus$). Let $w, d, h, [\cdot], [\cdot], \llcorner, \wp$, $A, B, C$ be as in Definition 3.1 and $\circ$ be the type for SELL$^\oplus$ formulas. Given a HyLL constraint domain $W$, consider a subexponential signature $\Sigma = \langle I, \leq, U \rangle$ such that $U = \{c, copy, \infty\} \cup \{c_w \mid w \in W\}$, $I = W \cup U$. For any $w \in W$ we have $w \leq \infty$, $copy \leq c_w \leq \infty$, $copy \leq c$ and, for any other $u, w \in I$, $u \not\leq w$. The encoding of HyLL inference rules into SELL$^\oplus$ is depicted in Figure 6 (we omit the encodings of the other connectives, that follow similarly).

Let us give some intuition on the above defined subexponential structure. The unbounded subexponential $c$ will be used to store the clauses defining the encoding of the rules (see Theorem 3.2). The unbounded subexponential $copy$ is the least of all the unbounded subexponentials. It is a dummy subexponential,<fnref n="5" /> useful to correctly specify $!_R$: when $!^copy$ is introduced, only formulas stored in the unbounded subexponentials can be present (i.e., the theory in $c$ and the atoms of the form $\llcorner \cdot \llcorner$, stored in $c_w$). Moreover, all the linear locations $w$ (not related to $copy$) must be empty. This reflects the fact that the HyLL linear context must be empty when $!$ is introduced. Note also that $w : \infty$ represents

<footnote n="3">³$\oplus$ can be read as “for all locations” while $\wp$ is meant to be “there exists a location”.</footnote>

<footnote n="4">⁴As specified by the side-condition of the $\otimes$ rule in Figure 4, it must be the case that $\mathcal{K}_1[s] = \mathcal{K}_2[s]$ when $s$ is unbounded.</footnote>

<footnote n="5">⁵Subexponentials are often called dummy when they are not inhabited.</footnote>
Negative rules

$$ \frac{\vdash \mathcal{K} : \Delta \Uparrow L}{\vdash \mathcal{K} : \Delta \Uparrow \perp, L} [\perp] \qquad \frac{\vdash \mathcal{K} : \Delta \Uparrow F, G, L}{\vdash \mathcal{K} : \Delta \Uparrow F \not\not\sim G, L} [\not\not\sim] \qquad \frac{\vdash \mathcal{K} +_l F : \Delta \Uparrow L}{\vdash \mathcal{K} : \Delta \Uparrow ?^l F, L} [?^l] $$

$$ \frac{}{\vdash \mathcal{K} : \Delta \Uparrow \top, L} [\top] \qquad \frac{\vdash \mathcal{K} : \Delta \Uparrow F, L}{\vdash \mathcal{K} : \Delta \Uparrow F \& G, L} [\&] $$

$$ \frac{}{\vdash \mathcal{K} : \Delta \Uparrow F[c/x], L} [\top] \qquad \frac{}{\vdash \mathcal{K} : \Delta \Uparrow F[l_e/l_x], L} [\not\not\sim] \qquad \frac{}{\vdash \mathcal{K} : \Delta \Uparrow \emptyset l_x : a.F, L} [\emptyset_R] $$

Positive rules

$$ \frac{}{\vdash \mathcal{K} : \cdot \Downarrow 1} [1] \text{ given } \mathcal{K}[\mathcal{I} \setminus \mathcal{U}] = \emptyset \qquad \frac{\vdash \mathcal{K}_1 : \Delta \Downarrow F}{\vdash \mathcal{K}_1 \otimes \mathcal{K}_2 : \Delta, \Delta \Downarrow F \otimes G} [\otimes] \text{ given } (\mathcal{K}_1 = \mathcal{K}_2)|_{\mathcal{U}} $$

$$ \frac{}{\vdash \mathcal{K} : \Delta \Downarrow F_i}{\vdash \mathcal{K} : \Delta \Downarrow F_1 \oplus F_2} [\oplus_i] \qquad \frac{}{\vdash \mathcal{K} : \Delta \Downarrow F[t/x]}{\vdash \mathcal{K} : \Delta \Downarrow \exists x.F} [\exists] \qquad \frac{}{\vdash \mathcal{K} : \Delta \Downarrow G[l/x]}{\vdash \mathcal{K} : \Delta \Downarrow \mathcal{W} l_x : a.G} [\mathcal{W}_L] $$

$$ \frac{}{\vdash \mathcal{K} \leq_I : \cdot \Uparrow F}{\vdash \mathcal{K} : \cdot \Downarrow!^l F} [l^l] \text{ given } \mathcal{K}[\{x \mid l \not\leq x \wedge x \notin \mathcal{U}\}] = \emptyset $$

Initial, Reaction and Decision Rules

$$ \frac{}{\vdash \mathcal{K} : \Delta \Downarrow p(\bar{t})^{\perp}} [I] \text{ given } p(\bar{t}) \in (\Delta \cup \mathcal{K}[\mathcal{I}]) \text{ and } (\Delta \cup \mathcal{K}[\mathcal{I} \setminus \mathcal{U}]) \subseteq \{p(\bar{t})\} $$

$$ \frac{}{\vdash \mathcal{K} +_l P : \Delta \Downarrow P}{\vdash \mathcal{K} +_l P : \Delta \Uparrow} [D_l], \text{ given } l \in \mathcal{U} \qquad \frac{}{\vdash \mathcal{K} : \Delta \Downarrow P}{\vdash \mathcal{K} +_l P : \Delta \Uparrow} [D_l], \text{ given } l \notin \mathcal{U} $$

$$ \frac{}{\vdash \mathcal{K} : \Delta \Downarrow P}{\vdash \mathcal{K} : \Delta, P \Uparrow L} [D_1] \qquad \frac{}{\vdash \mathcal{K} : \Delta \Uparrow L, P_a}{[R \Uparrow]} \qquad \frac{}{\vdash \mathcal{K} : \Delta \Uparrow N}{[R \Downarrow]} $$

<caption>Figure 4: Focused linear logic system with (quantified) subexponentials. Here, $L$ is a list of formulas, $\Delta$ is a multiset of formulas, $P$ is not an atom, $P_a$ is positive or an atom and $N$ is negative.</caption>

$$ \bullet (\mathcal{K}_1 \otimes \mathcal{K}_2)[i] = \begin{cases} \mathcal{K}_1[i] \cup \mathcal{K}_2[i] & \text{if } i \notin \mathcal{U} \\ \mathcal{K}_1[i] & \text{if } i \in \mathcal{U} \end{cases} \qquad \bullet \mathcal{K}[S] = \bigcup \{\mathcal{K}[i] \mid i \in S\} $$

$$ \bullet (\mathcal{K} +_l A)[i] = \begin{cases} \mathcal{K}[i] \cup \{A\} & \text{if } i = l \\ \mathcal{K}[i] & \text{otherwise} \end{cases} \qquad \bullet \mathcal{K} \leq_i [l] = \begin{cases} \mathcal{K}[l] & \text{if } i \leq l \\ \emptyset & \text{if } i \not\leq l \end{cases} $$

$$ \bullet (\mathcal{K}_1 = \mathcal{K}_2)|_S \text{ is true if and only if } (\mathcal{K}_1[j] = \mathcal{K}_2[j]) \text{ for all } j \in S. $$

<caption>Figure 5: Specification of operations on contexts.</caption>

any subexponential in the ideal of $\infty$ (note that $\infty$ is also a dummy subexponential). This means that, in the formula $\mathcal{W}w : \infty.F$, the subexponential variable $w$ could be substituted, in principle, by any element of $\mathcal{W} \cup \{c_w | w \in \mathcal{W}\}$. That is, the proposed subexponential signature correctly specifies the role of worlds in HyLL, as shown next.

**Theorem 3.2** (Adequacy). Let $\Upsilon$ be the set of formulas resulting from the encoding in Definition 3.2. The sequent $\Gamma; \Delta \vdash F@w$ is provable in HyLL iff the sequent

$$ c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, w : \lfloor F@w \rfloor; \cdot \Uparrow . $$

is provable in SELL$^\emptyset$.<fnref n="6" /> 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$^\emptyset$ formula corresponding to the encoding of $at_L$ (stored in $?^c\Upsilon$), we obtain

$$ \frac{w : [(A \ at \ u)@w] ; \cdot \Uparrow [(A \ at \ u)@w]^{\perp}}{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w : [(A \ at \ u)@w] ; \cdot \Downarrow!^w [(A \ at \ u)@w]^{\perp}} \stackrel{D_l, I}{\longrightarrow} \frac{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, v : [C@v], u : \lfloor A@u \rfloor; \cdot \Uparrow \cdot}{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, v : [C@v] ; \cdot \Downarrow?^u [A@u] \otimes R \Uparrow, ?^u} \longrightarrow \\ \frac{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, w : [(A \ at \ u)@w], v : [C@v] ; \cdot \Downarrow!^w [(A \ at \ u)@w]^{\perp} \otimes ?^u [A@u] \otimes \exists, \mathcal{W} \otimes \exists C, \mathcal{W}u, w. ([!^w [(C \ at \ u)@w]^{\perp} \otimes ?^u [C@u])}{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, w : [(A \ at \ u)@w], v : [C@v] ; \cdot \Downarrow \exists C, \mathcal{W}u, w. ([!^w [(C \ at \ u)@w]^{\perp} \otimes ?^u [C@u])} \longrightarrow \stackrel{D_l}{\longrightarrow} \\ \frac{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, w : [(A \ at \ u)@w], v : [C@v] ; \cdot \Uparrow .}{c : \{\Upsilon\}, c_{w_i} : \llbracket \Gamma \rrbracket, w_i : \lfloor \Delta \rfloor, w : [(A \ at \ u)@w], v : [C@v] ; \cdot \Uparrow .} $$

<footnote n="6">⁶Clarifying some notation: if $\Delta = \{F_1@w_1, \dots, F_n@w_n\}$, then $?w_i[\Delta] = ?w_1[F_1@w_1], \dots, ?w_n[F_n@w_n]$. Observe that, in the negative phase, such formulas will be stored at their respective contexts, that will be represented by $w_i : [\Delta]$. Similarly for $[\cdot, \cdot]$.</footnote>
Defined identity rules

$$ \underline{\Sigma; \mu B\vec{t} @ w \vdash \mu B\vec{t} @ w} \quad [\mu \text{Init}] \qquad \underline{\Sigma; \nu B\vec{t} @ w \vdash \nu B\vec{t} @ w} \quad [\nu \text{Init}] $$

Equality rules

$$ \underline{\Sigma; \vdash t = t @ w} \quad [= R] \qquad \frac{\{ (\Sigma; \Delta \vdash C @ w)\theta : \theta \in \text{csu}(s, t) \}}{\Sigma; \Delta, s = t @ u \vdash C @ w} \quad [= L] $$

Least fixed point rules

$$ \frac{\Sigma; \Delta \vdash B(\mu B)\vec{t} @ w}{\Sigma; \Delta \vdash \mu B\vec{t} @ w} \quad [\mu R] \qquad \frac{\vec{x}; B S \vec{x} @ u \vdash S \vec{x} @ u \quad \Sigma; \Delta, S \vec{t} @ u \vdash C @ w}{\Sigma; \Delta, \mu B \vec{t} @ u \vdash C @ w} \quad [\mu L] $$

Greatest fixed point rules

$$ \frac{\vec{x}; S \vec{x} @ w \vdash B S \vec{x} @ w \quad \Sigma; \Delta \vdash S \vec{t} @ w}{\Sigma; \Delta \vdash \nu B \vec{t} @ w} \quad [\nu R] \qquad \frac{\Sigma; \Delta, B(\nu B)\vec{t} @ u \vdash C @ w}{\Sigma; \Delta, \nu B \vec{t} @ u \vdash C @ w} \quad [\nu L] $$

Figure 7: Rules specific to $\mu$HyMALL. The rules for the HyMALL connectives can be directly adapted from those in Figure 2.

The rule for inequality requires a bit of explanation. There is one premise for each $\theta \in \text{csu}(s, t)$. The instance $(\Sigma; \vdash \Delta)\theta$ of the sequent $\Sigma; \vdash \Delta$ is defined as usual: its eigenvariables are the eigenvariables in the set of terms $\{u\theta : u \in \Sigma\}$, and for each formula $F \in \Delta$ there is the formula $F\theta$ in $\Delta\theta$.

For the fixed points, there is a version of the identity rule that relates the least and greatest fixed points, an unfold rule for least fixed points, and a coinduction rule for greatest fixed points:

$$ \frac{}{\Sigma; \vdash \mu B\vec{t}, \nu B\vec{t}} d\text{Init} \qquad \frac{\Sigma; \vdash \Delta, B(\mu B)\vec{t}}{\Sigma; \vdash \Delta, \mu B\vec{t}} \mu \qquad \frac{\vec{x}; \vdash (S\vec{x})^{\perp}, B S \vec{x}}{\Sigma; \vdash \Delta, \nu B\vec{t}} \nu $$

In the defined identity rule $d\text{Init}$, the notation $\bar{B}$ stands for $\lambda p. \lambda \vec{x}. (B p^{\perp} \vec{x})^{\perp}$. In the coinduction rule $(\nu)$, the predicate $S$ is an invariant. The first premise of the rule shows that it is indeed an invariant of $B$, while the second premise replaces the greatest fixed point $\nu B$ with the invariant. Observe that if we use $B(\nu B)$ itself for the invariant $S$, then we obtain:

$$ \frac{\frac{\frac{\vec{x}; \vdash \bar{B}(\mu \bar{B})\vec{x}, B(B(\nu B))\vec{x}}{\vec{x}; \vdash (B(\nu B)\vec{x})^{\perp}, B(B(\nu B))\vec{x}} \Sigma; \vdash \Delta, B(\nu B)\vec{t}}{\Sigma; \vdash \Delta, \nu B\vec{t}} \nu}{\nu} $$

The left branch is a proof of identity where eventually the defined identity rule $d\text{Init}$ is used to relate $\mu \bar{B}\vec{x}$ and $\nu B\vec{x}$. This branch will therefore always be derivable. Hence, we see that the unfold rule for $\nu$ is derivable in terms of the coinduction rule, and therefore does not need to be given explicitly. The meta-theory of $\mu$MALL, including the important cut-elimination theorem, is pretty standard and exhaustively covered in [Bae12].

Along the same lines as $\mu$MALL, we can extend HyMALL(the multiplicative/additive fragment of HyLL in Figure 2) to $\mu$HyMALL, by adding equality and least and greatest fixed points. In fact, for fixed point predicates built using $\mu$ and $\nu$, we will allow the arguments to contain worlds as well; likewise, we will allow for equality to hold between worlds. However, we retain the restriction from HyMALL that all undefined predicates contain no world arguments.<fnref n="7" /> Like with $\mu$MALL sequents, $\mu$HyMALL sequents will have an explicit context of eigenvariables, so they will be of the form $\Sigma; \Delta \vdash F @ w$, where $\Delta$ is as before. Since we are limiting our attention to $\mu$HyMALL, we dispense with the unbounded context $\Gamma$, which can be added to yield $\mu$HyLL. Most of the rules from Figure 2 can be directly adapted with this additional eigenvariable context. The remaining rules are given in Figure 7.

It may be worthwhile to consider if the $\mu$HyMALL rules can be encoded in $\mu$MALL by means of an extension of Definition 3.1. Indeed, we can simply extend the rules of Figure 3 with new cases for equalities and fixed points. The extension is almost entirely trivial and elided here except for the following sketch: both $[\mu \text{Init}]$ and $[\nu \text{Init}]$ will be captured by means of $d\text{Init}$; $[= R]$ by means of $=; [= L]$ by means of $\ne; [\mu L]$ and $[\nu R]$ by means of $\nu$; and $[\mu R]$ and $[\nu L]$ by means of $\mu$.

<footnote n="7">⁷This restriction can be lifted from HyMALL without any difficulty.</footnote>
# 5 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 shown in [dMDF14], 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 both propositional µMALL and first order µHyMALL. In both cases, we follow the standard interpretation of CTL quantifiers as fixed points.

The first encoding relies on the behavior of the LL connectives to control the use of transition rules during a proof of a CTL formula. More precisely, states in the transition system are represented as atoms (in the linear context) that are consumed and produced by the encoding of transitions. The second encoding uses HyLL's words in order to define states and quantifiers on words to specify path quantifiers. Hence, the encoding resembles the semantics of CTL.

Let us start by recalling the syntax of CTL.

**Definition 5.1 (CTL connectives and path quantifiers).** Given a set of atomic propositions $\mathcal{P}$, formulas in CTL are given by the following grammar

$$F ::= p | \neg F | F \land F | F \lor F | \mathbf{Q}XF | \mathbf{Q}FF | \mathbf{Q}GF | \mathbf{Q}[FUF] \quad p \in \mathcal{P}, Q \in \{A, E\},$$

The temporal connectives are: X (Next) meaning “at the next state”; F (Future) meaning “in some future”; G (Globally) meaning “in all futures”; and, FUG (F until G) meaning “from now, F will be true in every steps until some future point (possibly including now) where G holds”. Temporal connectives must be preceded by a path quantifier: E (Exists) meaning “for some path” or A (All) meaning “for all paths”. The usual dualities apply (e.g., $\neg \mathbf{EXF} = AX\neg F$, $\neg \mathbf{AGF} = EF\neg F$) and negation is involutive i.e., it can be restricted to atoms.

**Transition Systems.** Let $\mathcal{P} = \{p_1, \dots, p_n\}$ be a set of atomic propositions. A Kripke structure over $\mathcal{P}$ is a tuple $\mathcal{K} = \langle S, I, R, L \rangle$ where $S$ is a finite set of states, $I \subseteq S$ is the set of initial states, $R \subseteq S \times S$ is a transition relation and $L: S \to 2^\mathcal{P}$ is a labeling. We assume that given two different states $s, s'$, $L(s) \neq L(s')$. Note that this is not a loss of generality since we can always extend $\mathcal{P}$ with atomic propositions to uniquely identify each state. We shall write $s \to s'$ when $(s, s') \in R$. Observe that, in CTL, $R$ must be serial, i.e., every state has a successor. Finally, we write $s \models_{\mathcal{CTL}} F$ when $F$ holds at state $s$ with the standard meaning (see, e.g., [CE81]). For instance, $s \models_{\mathcal{CTL}}^{\mathcal{K}} EGF$ iff there exists a path $\pi = \langle s_1 \cdot s_2 \cdot s_3 \dots \rangle$ starting at $s$ (i.e. $s = s_1$) such that for all $i \ge 1$, $s_i \models_{\mathcal{CTL}}^{\mathcal{K}} F$.

## 5.1 Transition Systems and HyLL

In order to specify reachability properties in transition systems, some modal connectives can be defined in HyLL [DC14]:

$$ \begin{array}{l@{\qquad}l} \Box A & \stackrel{\text{def}}{=} \downarrow u. \forall w. (A \text{ at } u.w) \\ \delta_v A & \stackrel{\text{def}}{=} \downarrow u. (A \text{ at } u.v) \end{array} \qquad \begin{array}{l} \diamond A \stackrel{\text{def}}{=} \downarrow u. \exists w. (A \text{ at } u.w) \\ \phantom{\delta_v A \stackrel{\text{def}}{=} \downarrow u.} \end{array} $$

$\Box A$ (resp. $\diamond A$) represents all (resp. some) state(s) satisfying $A$ and reachable in some path from now. The connective $\delta$ represents a form of delay: $\delta_v A$ stands for an intermediate state in a transition to $A$. Informally it can be thought to be “v before $A$”.

We may use such modal operators in order to encode some features of transition systems as HyLL formulas. To each $p \in \mathcal{P}$, we associate two HyLL atomic formulas: $p$ and $p^\perp$ (abusing the notation), where by $p^\perp$ we denote the atomic HyLL proposition interpreting the CTL formula $\neg p$. Then states and transitions can be encoded as follows:

$$ [[s]]_{\mathcal{K}} = \bigotimes_{p \in \mathcal{P}} v(s, p) \qquad [[s \to s')]_{\mathcal{K}} = \forall w. (([[s]]_{\mathcal{K}} \text{ at } w) \neg \delta_1([[s']]_{\mathcal{K}}) \text{ at } w) $$

where $v(s, p) = p$ if $p \in L(s)$ and $v(s, p) = p^\perp$ otherwise. Given a transition relation $R = \{r_1, \dots, r_m\}$, we use $[[R]]_{\mathcal{K}}@w$ to denote the set $\{[[r_1]]_{\mathcal{K}}@w, \dots, [[r_m]]_{\mathcal{K}}@w\}$.

We can encode in HyLL a restricted fragment of CTL, namely, formulas built using only the temporal connectives EX, EF:

$$ \begin{array}{lclcl} [[p]]_{\mathcal{K}} & = & p \otimes \top & [[\neg p]]_{\mathcal{K}} & = & p^{\perp} \otimes \top \\ [[F \land G]]_{\mathcal{K}} & = & \mathbf{d}^{+}([[F]]_{\mathcal{K}} \& [[G]]_{\mathcal{K}}) & [[F \lor G]]_{\mathcal{K}} & = & \mathbf{d}^{-}([[[F]]_{\mathcal{K}}) \oplus \mathbf{d}^{-}([[[G]]_{\mathcal{K}}) \\ [[\mathbf{EXF}]]_{\mathcal{K}} & = & \mathbf{d}^{+}(\delta_1 [[F]]_{\mathcal{K}}) & [[\mathbf{EFF}]]_{\mathcal{K}} & = & \diamond [[F]]_{\mathcal{K}} \end{array} $$

where $\mathbf{d}^{+}(F) = F \otimes 1$ and $\mathbf{d}^{-}(F) = 1 \neg F$ are positive and negative delays respectively. Observe that $\mathbf{d}^{+}(F) \equiv \mathbf{d}^{-}(F) \equiv F$. Delays are added for adequacy results.

**Proposition 5.1 (Adequacy).** Let $\mathcal{K} = \langle S, I, R, L \rangle$ be a Kripke structure on a set of atomic propositions $\mathcal{P}$. Let $F$ be a CTL formula built from the CTL fragment $\land, \lor, \mathbf{EX}, \mathbf{EF}$. Then, $s \models_{\mathcal{CTL}}^{\mathcal{K}} F$ iff $[[R]]_{\mathcal{K}}@0; [[s]]_{\mathcal{K}}@w \vdash [[F]]_{\mathcal{K}}@w$ is provable in HyLL.
Proof. We will reason on the focused version of HyLL and we will assume that atoms have positive bias. Assume that $s \to s'$. If we decide to focus on the encoding of $(s, s') \in R$, we necessarily obtain a derivation of the shape

$$ \frac{[R]_K @0; [s']_K @w.1 \vdash G}{[R]_K @0; [s]_K @w \vdash G} \qquad (1) $$

where all atoms from $[s]_K @w$ are consumed and the formula $[s']_K @w.1$ is added into the context. This mimics exactly the transition $s \to s'$.

The ($\Rightarrow$) side proceeds by induction on the structure of $F$. For the base case, if $s \models_{CTL}^K p$, it is easy to show that the sequent $[R]_K @0; [s]_K @u \vdash (p \otimes \top)@u$ is provable in HyLL (similarly for $\neg p$). If $s \models_{CTL}^K EF F$, then there exists a path $\langle s_1 \cdot s_2 \cdots \rangle$ starting at $s$ s.t. there exists $i \ge 1$ s.t. $s_i \models_{CTL}^K F$. By repetitively applying (1), we have a derivation that consumes $[s_1]_K$ to produce $[s_i]_K$ and the result follows by induction. The case for $EF F$ follows similarly. Finally, the cases for $\wedge$ and $\vee$ follow immediately by induction.

($\Leftarrow$) We shall show that each focused step corresponds exactly to a “step” in the deduction of $s \models_{CTL}^K F$. Consider the sequent $[R]_K @0; [s]_K @w \vdash [F]_K @w$. We have two choices: (i) focus on $[s \to s']_K$ and, from (1), we transform the state $s$ into the state $s'$; or (ii) focus on the formula on the right. In the first case, we already showed that this action mimics exactly the transition $s \to s'$. In the second case, the focused formula $F$ must be of the form

$$ F ::= p \otimes \top | p^{\perp} \otimes \top | 1 \otimes (F \& F) | F \oplus F | \downarrow u (F \ at \ u.1) | \downarrow u (\exists w. F \ at \ u.w) $$

representing the encoding of atoms, conjunction, disjunction, $EF F$ and $EF F$ respectively. In a negative phase, the only connectives we can introduce, if any, are the hybrid ones ($\downarrow$ and $\atop$). This is a bureaucratic step allowing us to fix the formulas at the “current” world as in

$$ \frac{\Gamma; \Delta \vdash F[x/w]@y}{\Gamma; \Delta \vdash \downarrow x(F \ at \ y)@w} \ at_R, \downarrow_R $$

Hence, when focusing on $F$ we fall in one of the following cases.

* $F = p \otimes \top$ (or $p^{\perp} \otimes \top$): the context must already have $p$ (or $p^{\perp}$), at the right world, to prove $p$ (or $p^{\perp}$). This corresponds to proving that the state $s$ satisfies (or not) $p$.

* $F = 1 \otimes (F_1 \& F_2)$: $1$ is proved with empty context and focus is lost in $F_1 \& F_2$. Hence, after a negative phase, we have a derivation proving $F_1$ and another proving $F_2$. This corresponds exactly to the step of proving a conjunction in CTL.

* $F = F_1 \oplus F_2$: chose one of the branches and focus is lost due to the negative delay in the encodings. This corresponds to proving a disjunction in CTL.

* $F = d^+(\delta_1 F)$: focus is lost obtaining, on the right, $F$ fixed at the world $w+1$. This mimics the step of proving $F$ in the next time-unit ($EF F$).

* $F = \exists w. F \ at \ u.w$: a world $w$ is chosen and focus is lost (due to $\atop$). This corresponds in CTL to proving $EF F$ by showing that there exists a future world $(u+w)$ where $F$ holds.

□

Observe that our encoding cannot be extended to consider formulas of the shape $EGF$. In fact, the natural choice would be $[EGF]_K = \Box[F]_K$, but this encoding would not be adequate. Consider, for instance, a system with a unique state $s$ and a unique (looping) transition $s \to s$. Assuming that $p \in L(s)$, clearly $s$ satisfies the formula $EGp$. Now, consider the HyLL sequent $[s \to s]_K @0; [s]_K @w \vdash \Box[s]_K @w$. Introducing the connectives on the right we obtain

$$ \frac{[s \to s]_K @0; [s]_K @w \vdash [s]_K @w.v}{[s \to s]_K @0; [s]_K @w \vdash \Box[s]_K @w} \downarrow_R, \forall_R, \atop R $$

where $v$ is fresh. Then focusing on the encoding of $s \to s'$:

$$ \frac{[s \to s]_K @0; [s]_K @ (w+1) \vdash G}{[s \to s]_K @0; [s]_K @w \vdash G} \ copy, \forall_L, \neg_L $$

Therefore the left and right worlds in the sequent will never match, and this sequent is not provable. In other words: 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, i.e., fixed points.
$$ [[AXF]]_{\kappa} = \bigoplus_{(s,s') \in R} (\text{neg}(s) \oplus (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][F]_{\kappa}))) $$

$$ [[EXF]]_{\kappa} = \bigoplus_{(s,s') \in R} (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][F]_{\kappa})) $$

$$ [[AFF]]_{\kappa} = \mu Y. [[F]]_{\kappa} \oplus \bigoplus_{(s,s') \in R} (\text{neg}(s) \oplus (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) $$

$$ [[EFF]]_{\kappa} = \mu Y. [[F]]_{\kappa} \oplus \bigoplus_{(s,s') \in R} (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) $$

$$ [[AGF]]_{\kappa} = \nu Y. [[F]]_{\kappa} \& \bigoplus_{(s,s') \in R} (\text{neg}(s) \oplus (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) $$

$$ [[EGF]]_{\kappa} = \nu Y. [[F]]_{\kappa} \& \bigoplus_{(s,s') \in R} (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) $$

$$ [[A[F \cup G]]_{\kappa} = \mu Y. [[G]]_{\kappa} \oplus \left( [[F]]_{\kappa} \& \bigoplus_{(s,s') \in R} (\text{neg}(s) \oplus (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) \right) $$

$$ [[E[F \cup G]]_{\kappa} = \mu Y. [[G]]_{\kappa} \oplus \left( [[F]]_{\kappa} \& \bigoplus_{(s,s') \in R} (\text{pos}(s) \otimes ([[s']_{\kappa} \mathcal{Y}][Y])) \right) $$

<caption>Figure 8: Encoding of CTL into propositional μMALL (see Definition 5.2).</caption>

## 5.2 Encoding E and A quantifiers in propositional μMALL

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 whether AFF holds for all successors of s. Hence, CTL quantifiers are usually characterized as fixed points (see e.g., [BCM$^{+92}$]).

$$ \mathbf{EFF} = \mu Y.F \lor \mathbf{EXY} $$

$$ \mathbf{EGF} = \nu Y.F \land \mathbf{EXY} $$

$$ \mathbf{E}[F \cup G] = \mu Y.G \lor (F \land \mathbf{EXY}) $$

$$ \mathbf{AFF} = \mu Y.F \lor \mathbf{AXY} $$

$$ \mathbf{AGF} = \nu Y.F \land \mathbf{AXY} $$

$$ \mathbf{A}[F \cup G] = \mu Y.G \lor (F \land \mathbf{AXY}) $$

**Definition 5.2 (CTL into propositional μMALL).** Let $\mathcal{K} = \langle S, I, R, L \rangle$ be a Kripke structure on a set of atomic propositions $\mathcal{P}$. We define

$$ - [[s]]_{\mathcal{K}} = (\bigotimes_{p \in \mathcal{P}} v(s, p))^{\perp} \text{ where } v(s, p) = p \text{ if } p \in L(s) \text{ and } v(s, p) = p^{\perp} \text{ otherwise.} $$

$$ - pos(s) = [[s]]_{\mathcal{K}}^{\perp} $$

$$ - neg(s) = \bigoplus_{p \in \mathcal{P}} (v(s, p))^{\perp} \otimes \top. $$

The encodings of $QX$, $QF$, $QG$ and $QU$, for $Q \in \{A, E\}$ are in Figure 8. The encoding of the rest of the formulas is as in the case for HyLL.

The encoding relies on the following principles. Let $r = (s, s') \in R$. The formula $pos(s)$ (resp. $neg(s)$) tests if $r$ can (resp. cannot) be fired at the current state. If it can be fired, then the current state is transformed into the new state. Hence, the encoding of $A$ (resp. $E$) test all (resp. at least one) of the fireable rules. This explains the use of $\&$ (resp. $\oplus$). Finally, the use of least or greatest fixed points reflects the fixed point characterization of CTL connectives given above.

**Remark 5.1.** Observe that, in all the clauses in Figure 8, the formula $pos(s) \otimes ([[s']_{\kappa} \mathcal{Y}][B])$, is present. We could have written instead $[r]_{\kappa} \to B$, which reads closer to what we expect: "assuming that $r$ is fired, $B$ holds". The formulas $(L \to R) \to B$ and $L \otimes (R \to B)$ are not logically equivalent. In fact, the first formula is equivalent to $(L \otimes R^{\perp}) \mathcal{Y}B$ while the second is equivalent to $L \otimes (R^{\perp} \mathcal{Y}B)$. The first is stronger, 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$. We chose the second since it describes better the desired behavior, thus easing the proof of the following adequacy result.

**Theorem 5.1 (Adequacy).** Let $\mathcal{K} = \langle S, I, R, L \rangle$ be a Kripke structure on a set of atomic propositions $\mathcal{P}$, $s \in S$ be a state and $F$ be a CTL formula. Then, $s \models_{\mathcal{K}}^L F$ iff the sequent $\vdash [[s]]_{\mathcal{K}}, [[F]]_{\mathcal{K}}$ is provable in μMALL.

*Proof.* As done for HyLL, we will consider the focused version of μMALL and we will assume that atoms have positive bias.

(⇒) We proceed by induction on the structure of the formula. The base cases for atomic formulas ($p$ and $\neg p$) are trivial and the cases for $\land$ and $\lor$ are easy consequences from the inductive hypothesis.

**Cases AX and EX.** Note that given two different states $s$ and $s'$ (thus $L(s) \neq L(s')$):

* the sequents $\vdash [[s]]_{\mathcal{K}}, pos(s)$ and $\vdash [[s]]_{\mathcal{K}}, neg(s')$ are both provable.

* the sequents $\vdash [[s]]_{\mathcal{K}}, neg(s)$ and $\vdash [[s]]_{\mathcal{K}}, pos(s')$ are both not provable.

This means that, in a context containing the formula $[[s]]_{\mathcal{K}}$, we can always prove if a given transition rule $r \in R$ is fireable or not.
Consider the case AXF. The derivation necessarily starts with the negative phase

$$ \frac{\Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{neg}(s_1) \oplus (\mathrm{pos}(s_1) \otimes ([[s'_i]]_{\mathcal{K}} \mathring{\otimes} [[F]]_{\mathcal{K}}) \dots \Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{neg}(s_m) \oplus (\mathrm{pos}(s_m) \otimes ([[s'_m]]_{\mathcal{K}} \mathring{\otimes} [[F]]_{\mathcal{K}}) \& \\ \Sigma; \vdash [[s]]_{\mathcal{K}}, \mathcal{\&} \quad (\mathrm{neg}(s) \oplus (\mathrm{pos}(s) \otimes ([[s']_{\mathcal{K}} \mathring{\otimes} [[F]]_{\mathcal{K}})))}{(s,s') \in R} $$

Then, for every premise, a positive phase starts, choosing 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 have

$$ \frac{\Sigma; \vdash [[s'_i]]_{\mathcal{K}}, [[F]]_{\mathcal{K}}}{\Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{pos}(s_i) \otimes ([[s'_i]]_{\mathcal{K}} \mathring{\otimes} [[F]]_{\mathcal{K}})} \otimes, \mathring{\otimes} $$

and the positive phase ends. By inductive hypothesis, the sequent $\Sigma; \vdash [[s'_i]]_{\mathcal{K}}, [[F]]_{\mathcal{K}}$ 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 at s'. Let $s = s_1 \rightarrow \dots \rightarrow s_n = s'$ be one of such paths and consider the following derivation:

$$ \frac{\Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{neg}(s_1) \oplus (\mathrm{pos}(s_1) \otimes ([[s'_1]]_{\mathcal{K}} \mathring{\otimes} \mu B) \dots \Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{neg}(s_m) \oplus (\mathrm{pos}(s_m) \otimes ([[s'_m]]_{\mathcal{K}} \mathring{\otimes} \mu B)}{\Sigma; \vdash [[s]]_{\mathcal{K}}, \mu B} \quad \mu, \oplus, \& $$

The premises correspond to proving whether a transition $r \in R$ is fireable or not. If $r$ is fireable, we observe a derivation of the shape

$$ \frac{\Sigma; \vdash [[s'_i]]_{\mathcal{K}}, \mu B}{\Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{pos}(s_i) \otimes ([[s'_i]]_{\mathcal{K}} \mathring{\otimes} \mu B)} \otimes, \mathring{\otimes} \\ \Sigma; \vdash [[s]]_{\mathcal{K}}, \mathrm{neg}(s_i) \oplus (\mathrm{pos}(s_i) \otimes ([[s'_i]]_{\mathcal{K}} \mathring{\otimes} \mu B)) \oplus $$

where s becomes $s'_i$ and, from that state, $\mu B$ must be proved. Hence, we can show that $[[s_n]]_{\mathcal{K}}$ will be eventually added to the context. By inductive hypothesis, the sequent $\Sigma; \vdash [[s_n]]_{\mathcal{K}}, [[F]]_{\mathcal{K}}$ is provable and hence $\Sigma; \vdash [[s_n]]_{\mathcal{K}}, \mu B$ is provable (by unfolding and then choosing $[[F]]_{\mathcal{K}}$ in the disjunction $[[AFF]]_{\mathcal{K}} = \mu Y. [[F]]_{\mathcal{K}} \oplus \Psi$).

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 reachable states from s must also satisfy AGF. Let

$$ S = \{s \in S \mid s \models_{CTL} F \text{ and, for all } s', \text{ if } s \rightarrow s', \text{ then } s' \in 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, \dots, s_n\}$ and $I = [[s_1]]_{\mathcal{K}}^{\perp} \oplus \dots \oplus [[s_n]]_{\mathcal{K}}^{\perp}$. We shall show that, for any $s \in S$, the sequent $\Sigma; \vdash [[s]]_{\mathcal{K}}, [[AGF]]_{\mathcal{K}}$ is provable using $I$ as inductive invariant.

Once the rule $\nu$ is applied, we have to prove two premises:

1. **Premise** $\Sigma; \vdash [[s]]_{\mathcal{K}}, I$. This sequent is easy by choosing $[[s]]_{\mathcal{K}}^{\perp}$ from $I$.

2. **Premise** $\Sigma; \vdash BI, I^{\perp}$. The $\mathcal{\&} [[s]]_{\mathcal{K}}$ formula in $I^{\perp}$ forces us to prove several cases. More precisely, for each $s \in S$, we have to prove $\Sigma; \vdash BI, [[s]]_{\mathcal{K}}$. Consider the following derivation

$$ \frac{\Sigma; \vdash [[F]]_{\mathcal{K}}, [[s]]_{\mathcal{K}} \quad \Sigma; \vdash R_1, [[s]]_{\mathcal{K}} \quad \dots \quad \Sigma; \vdash R_n, [[s]]_{\mathcal{K}}}{\Sigma; \vdash [[F]]_{\mathcal{K}} \& R_1 \& \dots \& R_n, [[s]]_{\mathcal{K}}} \& $$

where $R_i = \mathrm{neg}(s_i) \oplus (\mathrm{pos}(s_i) \otimes ([[s'_i]]_{\mathcal{K}} \mathring{\otimes} I))$. Again we have several cases to prove.

The first sequent $\Sigma; \vdash F, [[s]]_{\mathcal{K}}$ follows from inductive hypothesis.

If the rule $r_i$ is not fireable at state s, then the sequent $\Sigma; \vdash [[s]]_{\mathcal{K}}, R_i$ is provable (by choosing neg($s_i$)). On the other hand, if $r_i$ is fireable at state s, we then have

$$ \frac{\Sigma; \vdash [[s']_{\mathcal{K}}, I]}{\Sigma; \vdash R_i, [[s]]_{\mathcal{K}}} \oplus, \otimes, \& $$

Since $S$ is closed under $\rightarrow$, it must be the case that $s' \in S$ and hence the sequent $\Sigma; \vdash [[s']_{\mathcal{K}}, I$ is provable (as in **Premise 1** above).

The case EG is similar.

($\Leftarrow$) Due to focusing, we can show that the derivations in the $\Rightarrow$ part are the only way to proceed during a proof in (focused) $\mu$MALL. Hence, we match exactly a “step” in the deduction of $s \models_{CTL} F$. Hence, the only interesting case
$$
\begin{align*}
\llbracket AXF \rrbracket &= \downarrow u. \forall w. \text{trans } u w \otimes (\llbracket F \rrbracket \text{ at } w) \\
\llbracket EXF \rrbracket &= \downarrow u. \exists w. \text{trans } u w \otimes (\llbracket F \rrbracket \text{ at } w) \\
\llbracket AFF \rrbracket &= \mu(\lambda R. \llbracket F \rrbracket \oplus \downarrow u. \forall w. \text{trans } u w \otimes (R \text{ at } w)) \\
\llbracket EFF \rrbracket &= \mu(\lambda R. \llbracket F \rrbracket \oplus \downarrow u. \exists w. \text{trans } u w \otimes (R \text{ at } w)) \\
\llbracket AGF \rrbracket &= \nu(\lambda R. \llbracket F \rrbracket \& \downarrow u. \forall w. \text{trans } u w \otimes (R \text{ at } w)) \\
\llbracket EGF \rrbracket &= \nu(\lambda R. \llbracket F \rrbracket \& \downarrow u. \exists w. \text{trans } u w \otimes (R \text{ at } w)) \\
\llbracket A[F \cup G] \rrbracket &= \mu(\lambda R. \llbracket G \rrbracket \oplus (\llbracket F \rrbracket \& \downarrow u. \forall w. \text{trans } u w \otimes (R \text{ at } w))) \\
\llbracket E[F \cup G] \rrbracket &= \mu(\lambda R. \llbracket G \rrbracket \oplus (\llbracket F \rrbracket \& \downarrow u. \exists w. \text{trans } u w \otimes (R \text{ at } w)))
\end{align*}
$$

<caption>Figure 9: Encoding of CTL into µHyMALL (See Definition 5.3)</caption>

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]]<sub>K</sub>, νB with invariant I<sub>x</sub>. This means that we have a proof of the sequent Σ; ⊢ [[s]]<sub>K</sub>, I<sub>x</sub>. Moreover, due to the shape of B, we must also have a proof of Σ; ⊢ [[s<sup>s</sup>]]<sub>K</sub>, I<sub>x</sub> for any reachable state s'. Then, we can show that there is a proof of Σ; ⊢ I<sub>x</sub>, &<sub>s∈S</sub> [[s]]<sub>K</sub>. Let I be the invariant in the proof of the ⇒ part. Note that I<sup>⊥</sup> = &<sub>s∈S</sub> [[s]]<sub>K</sub> and hence Σ; ⊢ I<sub>x</sub>, I<sup>⊥</sup> (i.e., Σ; ⊢ I ⊢ I<sub>x</sub>) is provable. This shows that I is greater than I<sub>x</sub>, thus we also have a proof of Σ; ⊢ [[s]]<sub>K</sub>, νB using I. The result follows from a derivation similar to the one used in the proof of the ⇒ part. □

Finally, it is worth noticing that, in Definition 5.2, we do not encode the transition rules as a theory (as we did in Section 5.1). In fact, consider the following: (1) the presence of a formula of the shape [[s → s']<sub>K</sub> in the context allows us to move from the current state to a successor one; (2) fixed points operators must be applied in order to go through paths, checking properties on them. Now, actions (1) and (2) should be coordinated, otherwise one would lose adequacy in the encodings. More precisely, by focusing on [[s → s']<sub>K</sub>, we may “jump” a state without checking the needed property in that state. For avoiding these problems, we internalized the transition rules directly into the encoding.

## 5.3 CTL in µHyMALL

The encoding on µMALL in the previous section is heavy in two specific ways: (1) the current state of the automaton is managed by means of the neg and pos predicates, and (2) the encoding of formulas is not compositional as it is sensitive to the transition system R. These aspects limit us from even stating and proving properties of the encoding that are independent of the transition system. For instance, it is obvious from the semantics that AGF implies EGF regardless of what F or R are, and this can even be seen as a direct consequence of (A & B) ⊢ (A ⊕ B) being true in linear logic, but we are prevented from writing that implication generically for any R. These issues can be addressed by means of an encoding using µHyMALL instead of µMALL.

The key difference in the encoding in µHyMALL is that we can encode the transition system directly by means of a non-recursive least fixed point expression, i.e., a table. We write this as the predicate trans that can be derived from a set of transition rules R as follows:

$$ \mathbf{trans} \triangleq \mu \left( \lambda T. \lambda u. \lambda v. \bigoplus_{(s,s') \in R} (s = u \otimes s' = v) \right). $$

From the definition of trans, we have that, for any given s, s':

- trans s s' → trans s s' ⊗ trans s s' and

- trans s s' → 1.

These statements are easy to prove, starting with [¬R] and then using [µL] (with any invariant since trans is not recursive). Note that for any t, t = t is logically equivalent to 1. Moreover, if t and t' are different terms, then csu(t, t') is empty and a formula t = t' on the left of the sequent finishes any derivation (using [=L]).

**Definition 5.3. (CTL into µHyMALL)** Let K = ⟨S, I, R, L⟩ be a Kripke structure on a set of atomic propositions P. Let trans be the predicated defined as above on R. The encoding [[·]] of CTL temporal formulas, i.e., of QX, QF, QG and QU, for Q ∈ {A, E} into µHyMALL is in Figure 9.

**Theorem 5.2 (Adequacy).** Let K = ⟨S, I, R, L⟩ be a Kripke structure on a set of atomic propositions P, s ∈ S be a state and F be a CTL formula. Then, the µHyMALL sequent: ·; · ⊢ [[F]] @ s is derivable if and only if s |=<sub>CTL</sub> F.

*Proof.* The proof follows the same argument in the proof of Theorem 5.1. □

Observe that in this encoding, the task of establishing the successor state is delegated to the multiplicative subformula trans uv in each case. The multiplicative split guarantees that it cannot consume any other linear assumptions. However, since trans unfolds into a disjunction of equations, there is no possible way for it to consume any linear resources
in the first place. Note also that this predicate is the only one in the encoding that needs to quantify over worlds. This is
typical of encodings in $\mu$HyMALL (or $\mu$HyLL): any inductive reachability relation that needs to be encoded on worlds
can be represented as a least fixed point predicate.

As mentioned at the start of this subsection, the encoding in $\mu$HyMALL allows us to prove meta-theoretic properties of
CTL such as, for any $F, \cdot; [AGF] @ s \vdash [AFF] @ s$. This proof does not require examining the *trans* definition at all.
In fact, all the characteristic properties of CTL given at the start of Section 5.2 can be proved as theorems in $\mu$HyMALL.

# 6 Concluding Remarks and Future Work

We compared the expressiveness, as logical frameworks, of two extensions of linear logic (LL). We showed that it is
possible to adequately encode HyLL's logical rules into LL. In order to better analyze the meaning of worlds in HyLL,
we showed that a flat subexponential structure (for worlds) suffices to encode HyLL into $SELL^\emptyset$. We also showed 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 [Ree06]. Being a logic in the
LF family, HLF is based on natural deduction, hence having a complex notion of $(\beta\eta)$ 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 several systems. This work
indicates that SELL is a broader framework for handling such systems, since it can encode HyLL's rules and worlds
naturally and directly. However, the simplicity of HyLL may be of interest for specific purposes, such as building tools
for diagnosis in biomedicine. Moreover, as shown in Section 5.3, HyLL offers an elegant way of specifying transitions
systems and their properties (written in CTL).

Formal proofs in HyLL were implemented in [dMDF14], in the Coq proof assistant. It would be interesting to extend
the implementations of HyLL given there to $\mu$HyMALL. Such an interactive proof environment would enable both formal
studies of encoded systems in $\mu$HyMALL and formal meta-theoretical study of $\mu$HyMALL itself.

**Acknowledgments.** We would like to thank Dale Miller for being such a good mentor and colleague. We also thank the anonymous reviewers for their valuable comments on an earlier draft of this paper.

# References

[ADOR15] Jaime Arias, Myriam Desainte-Catherine, Carlos Olarte, and Camilo Rueda. Foundations for reliable and flexible interactive multimedia scores. In Tom Collins, David Meredith, and Anja Volk, editors, *MCM 2015*, volume 9110 of LNCS, pages 29–41. Springer, 2015.

[And92] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *J. Log. Comput.*, 2(3):297–347, 1992.

[Bae12] David Baelde. Least and greatest fixed points in linear logic. *ACM Trans. Comput. Log.*, 13(1):2, 2012.

[BCM+92] Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^20 states and beyond. *Inf. Comput.*, 98(2):142–170, 1992.

[CE81] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, *Logics of Programs, Workshop, Yorktown Heights, New York, May 1981*, volume 131 of LNCS, pages 52–71. Springer, 1981.

[Cha10] Kaustuv Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In Anuj Dawar and Helmut Veith, editors, *CSL 2010*, volume 6247 of LNCS, pages 185–199. Springer, 2010.

[Chu40] Alonzo Church. A formulation of the simple theory of types. *The Journal of Symbolic Logic*, 5:56–68, 1940.

[CP02] Iliano Cervesato and Frank Pfenning. A Linear Logical Framework. *Inf. & Comp.*, 179(1):19–75, 2002.

[CPT16] Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. *Mathematical Structures in Computer Science*, 26(3):367–423, 2016.
[CR15] Kaustuv Chaudhuri and Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, *LPAR-20 2015*, volume 9450 of LNCS, pages 146–161. Springer, 2015.

[DC14] Joëlle Despeyroux and Kaustuv Chaudhuri. A hybrid linear logic for constrained transition systems. In *Post-Proc. of TYPES 2013*, volume 26 of *Leibniz Intl. Proceedings in Informatics*, pages 150–168. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2014.

[DJS93] Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, *Kurt Gödel Colloquium*, volume 713 of LNCS, pages 159–171. Springer, 1993.

[dMDF14] Elisabetta de Maria, Joëlle Despeyroux, and Amy Felty. A logical framework for systems biology. In *Proceedings of the 1st Intl. Conference on Formal Methods in Macro-Biology (FMMB)*, volume 8738 of LNCS, pages 136–155. Springer, 2014.

[DOP17] Joëlle Despeyroux, Carlos Olarte, and Elaine Pimentel. Hybrid and subexponential linear logics. *Electr. Notes Theor. Comput. Sci.*, 332:95–111, 2017.

[Gir87] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987.

[Mil92] Dale Miller. Unification under a mixed prefix. *Journal of Symbolic Computation*, 14(4):321–358, 1992.

[MP13] Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. *Theor. Comput. Sci.*, 474:98–116, 2013.

[Nig14] Vivek Nigam. A framework for linear authorization logics. *Theor. Comput. Sci.*, 536:21–41, 2014.

[NM09] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, *PPDP*, pages 129–140. ACM, 2009.

[NM10] Vivek Nigam and Dale Miller. A framework for proof systems. *J. Autom. Reasoning*, 45(2):157–188, 2010.

[NOP13] Vivek Nigam, Carlos Olarte, and Elaine Pimentel. A general proof system for modalities in concurrent constraint programing. In *CONCUR*, volume 8052 of LNCS, pages 410–424. Springer Verlag, 2013.

[NOP17] Vivek Nigam, Carlos Olarte, and Elaine Pimentel. On subexponentials, focusing and modalities in concurrent systems. *Theor. Comput. Sci.*, 693:35–58, 2017.

[NPR11] Vivek Nigam, Elaine Pimentel, and Giselle Reis. Specifying proof systems in linear logic with subexponentials. *Electr. Notes Theor. Comput. Sci.*, 269:109–123, 2011.

[NPR16] Vivek Nigam, Elaine Pimentel, and Giselle Reis. An extended framework for specifying and reasoning about proof systems. *J. Log. Comput.*, 26(2):539–576, 2016.

[OCFH16] Carlos Olarte, Davide Chiarugi, Moreno Falaschi, and Diana Hermith. A proof theoretic view of spatial and temporal dependencies in biochemical systems. *Theoretical Computer Science*, 641:25–42, 2016.

[OPN15] Carlos Olarte, Elaine Pimentel, and Vivek Nigam. Subexponential concurrent constraint programming. *Theoretical Computer Science*, 606:98–120, 2015.

[OPR18] Carlos Olarte, Elaine Pimentel, and Camilo Rueda. A concurrent constraint programming interpretation of access permissions. *TPLP*, 18(2):252–295, 2018.

[PON14] Elaine Pimentel, Carlos Olarte, and Vivek Nigam. A proof theoretic study of soft concurrent constraint programming. *Theory and Practice of Logic Programming*, 14:475–308, 2014.

[Ree06] Jason Reed. Hybridizing a logical framework. In *International Workshop on Hybrid Logic (HyLo)*, Electronic Notes in Theoretical Computer Science, pages 135–148, Seattle, USA, August 2006. Elsevier.