Note that if *C* ⦂ T and T T then *C* ⦂ T- , so typing is a well-defined relation from configurations to equivalence classes of configuration types.

#### **Proposition 4.** (Compλμ ⦂ Tyλμ2) *satisfies the subject reduction property.*

*Proof.* For the observable transitions, this is a straightforward observation that the typing relation is preserved. For internal transitions (specifically, β reductions), we use the corresponding subject reduction property for λμ2 substitutions — i.e. if Θ; Ξ; Γ K[λx.ts] : ⊥; Δ then Θ; Ξ; Γ K[t[s/x]] : ⊥; Δ and if Θ; Ξ; Γ K[μα.t] : ⊥; Δ then Θ; Ξ; Γ t[K/α] : ⊥; Δ.

Figure 2 gives an example illustrating the role of types in constraining behaviour: a trace of the value λf.f v ⦂ ∃X.X, where v is an arbitrary typable value (recall that ∃X.X - ∀Y.(∀X.X → Y ) → Y ). Observe that there are no transitions from the the final state — a call to γ is not possible because −Y, +X −(Y - = X- ) is not negatively satisfiable. In fact, the tree of transitions of ∃X.X branches only on negative transitions (i.e. Opponent moves). It follows that any configuration of this type will have the same set of transitions, and that therefore λf.f λxy.x ∼∃X.X λf.f λxy.y as proposed in the introduction.

### **4.2 A Second-Order Typed Interaction Structure**

It remains to prove that Tyλμ2 is a well-defined typing system for the interaction structure on Compλμ, and that typed bisimulation is therefore a congruence. We need to establish that the pointwise extension of the arrow relation (Definition 16) to second-order configuration types (i.e. T1 T2 T3 if Θ1 Θ2 Θ3, Ξ1 Ξ2 Ξ3, Γ1 Γ2 Γ3, Δ1 Δ2 Δ3, and pτ1 pτ2 pτ3) satisfies the conditions of Definition 5 — that if *C*1 = (E1; A1) ⦂ T1 and *C*2 = (E2; A2) ⦂ T2, where T1 T2 T3 and

( ; λf.f v) ⦂ ( ; ; −(∀X.X → Y ) → Y ; ) −g,α ↓ ( ; [α]g v) ⦂ (−Y - ; ; −g : ∀X.X → Y - +⊥; −α : Y - ) +gβ ↓ ((β → [α] • v); •) ⦂ (−Y - ; ; −g : ∀X.X → Y - −⊥; −α : Y - , +β : ∀X.X → Y - −β ↓ ((β → [α] • v); [α] • v) ⦂ (−Y - ; ; −g : ∀X.X → Y - +∀X.X → Y - ; −α : Y - ) +z,γ ↓ ((β → [α] • v), (z → v), (γ → [α]•); •) ⦂ (−Y - , +X- ; ; −g : ∀X.X → Y - , +z : X- −⊥; −α : Y - , +γ : Y - ) −zδ ↓ ((β → [α] • v), (z → v), (γ → [α]•); [δ]v) ⦂ (−Y - , +X- ; ; −g : ∀X.X → Y - , +z : X- +⊥; −α : Y - , +γ : Y - , −δ : X- ) +δ ↓ ((β → [α] • v), (z → v), (γ → [α]•); v) ⦂ (−Y - , +X- ; ; −g : ∀X.X → Y - , +z : X- −X- ; −α : Y - , +γ : Y - )

Fig. 2: Trace of λf.f v : ∃X.X

sup(*C*1)∩sup(*C*2) ⊆ sup(T1), then C1|C2 is well-defined, has type T3 and satisfies the interaction conditions.

By Proposition 2, *C*1|*C*2 = (E1 ∪ E2; A1|A2) is a well-defined configuration, and E - E1 ∪ E2 is a pre-valuation for Γ3 ∪ Δ3. By the assumption that *C*1 ⦂ T1 and *C*2 ⦂T2, there are valuations V1 *C*1 ⦂T1 and V2 *C*2 ⦂T2. Then V - V1∪V2 is a pre-valuation for Θ3. To show that V∗ *C*1|*C*2 ⦂ T3, we need to verify that:

**Lemma 3.** V *positively satisfies* Ξ3*.*

*Proof.* Let W be a pre-valuation for Θ3. The first formula in Ξ2 (if any) which is not satisfied by V∪W = V1 ∪ V2 ∪ W cannnot be positive in Ξ1 (positively satisfied by V1) nor in Ξ2 (positively satisfied by V2), and so must be a negative formula in Ξ3.

**Lemma 4.** Θ− 3 ; V∗(Ξ3); V∗(Γ − 3 ) E∗(A1|A2) : V(τ ); V∗(Δ− 3 )

*Proof.* Observe that E∗ = (E∗ 1 · E∗ 1 )i and V = (V2 · V1)i for some i ≤ n. Hence, it suffices to prove by induction on i that Θ2; (V2 · V1)i (Ξ2); (V2 · V1)i (Γ − 2 ) (E∗ 2 · E∗ 1 )i (A1|A2); (V2 · V1)i (Δ− 2 ).

Similarly, each term and continuation assigned to an output variable is welltyped under closure by V∗ and E∗ and thus:

**Proposition 5.** *C*1|*C*2 ⦂ T3*.*

It remains to show that the interaction conditions of Definition 5 are satisfied. The key is establishing condition 1 — that if *C*1 pl −→ *C* - 1 and *C*2 pl −→ *C* - 2 then T1 pl → T- 1 and T2 pl → T- 2 such that T- 1 T- 2 T3. This requires some further investigation of configuration types.

The interesting cases are those where A1 ≡ λx.t and A2 ≡ K[•s] (or viceversa) and so they can perform the complementary actions − y, α and + y, α. We need to show that |Θ1|; |Ξ1| τ is *non-atomic* — that is, |Θ1|; |Ξ1| τ = ∀X1 ...Xm.ρ → σ — for some ρ, σ. Observe that this implies that |Θ2|; |Ξ2| τ is also non-atomic (since Ξ2 contains the equations in Ξ1) so that T1 and T2 can perform the complementary actions − y, α and + y, α.

Since any derivation of a typing judgement for λx.t or K[•s] must conclude with →-introduction followed by applications of the type-equality rule we have:

**Lemma 5.** *If* Θ; Ξ; Γ λx.t : τ ; Δ *or* Θ; Ξ; Γ K[•s] : τ ; Δ *then* Θ; Ξ τ *is non-atomic.*

Hence, by the assumption that (E1; λx.t)⦂(Θ1; Ξ2; Γ1 −τ ; Δ1) and (E2; K[•t])⦂ (Θ2; Ξ2; Γ2 +τ ; Δ) we know that Θ1; V1(Ξ1) V1(τ ) and Θ2; V∗ 2 (Ξ2) V∗ 2 (τ ) are non-atomic. From the latter we may infer that Θ1; V∗ 2 (Ξ1) V∗ 2 (τ ) is nonatomic, since Θ2 and Ξ2 are interleavings of Θ1 and Ξ1 with the disjoint contexts Θ3 and Ξ3.

So to show that |Θ1|; |Ξ1| τ is non-atomic is it is sufficient to prove the contrapositive.

**Lemma 6.** *Suppose* V+ Θ Ξ *and* V− Θ Ξ*, where* |Θ|; |Ξ| τ *is atomic. Then either* Θ−; V+(Ξ) V+(τ ) *or* Θ+; V−(Ξ) V−(τ ) *is atomic.*

*Proof.* We extend the grammar of types with an unbounded set of "neutral atoms" A, B, C, . . ., which are equal only if syntactically identical, and prove the lemma for this extended set of types by an outer induction on the size of Θ, and an inner induction on the sum of the lengths of the types in Ξ.

At least one of V+(τ ) and V−(τ ) must be atomic and so if Ξ is empty then the hypothesis holds. Otherwise, Ξ ≡ p(σ = σ- ), Ξ for some types σ, σ and equational context Ξover Θ, and polarity p ∈ {+, −}.

If σ and σ are both non-atomic, then by satisfiability σ ≡ ∀X1 ...Xn.ρ1 → ρ2 and σ ≡ ∀X1 ...Xn.ρ- 1 → ρ- 2 for some ρ1, ρ2, ρ- 1, ρ- 2. Letting A1,...,An be fresh, distinct atomic types, define ρ = ρ[A1/X1,...,An/Xn]. The equational context Ξ-- = p(ρ1 = ρ1 - ), p(ρ2 = ρ2 - ), Ξ is equivalent to (satisfied by the same valuations as) Ξ, and so Θ; Ξ-- τ is atomic, and positively and negatively satisfied by V+ and V−. Hence, by inner induction hypothesis, one of Θ−; V+(Ξ--) V+(τ ) or Θ+; V−(Ξ--) V−(τ ) is atomic.

Otherwise at least one of σ and σ is atomic. If σ ≡ σ- , then we may discard the tautology σ = σ and apply the (inner) inductive hypothesis to Θ; Ξ- τ . Otherwise at least one of σ, σ must be a type-variable with polarity p in Θ (none of the other cases are p-satisfiable). So assume without loss of generality that Θ ≡ Θ- , pX, Θ- and Ξ ≡ p(σ = X), Ξ- . We may show that:

**–** Θ- , Θ--; Ξ- [σ/X] τ [σ/X] is atomic.

**–** Θ, Θ-- Ξ- [σ/X] is positively satisfied by V+ and negatively satisfied by V−.

So by the outer inductive hypothesis, either (Θ- , Θ--)−; V+(Ξ[σ/X]) V+(τ ) or (Θ, Θ--)+; V−(Ξ[σ/X]) V−(τ ) is atomic, and hence either Θ−; V+(Ξ) V+(τ ) or Θ+; V−(Ξ) V−(τ ) is atomic.

We have shown that the arrow relation satisfies the first interaction condition. 2 and 3 are straightforward to verify, establishing that (Compλμ2 ⦂ Tyλμ2) is a well-defined typed interaction structure. Therefore, by Proposition 1, typed bisimulation is preserved by parallel composition plus hiding, and thus:

**Theorem 1.** *Typed bisimulation is a congruence for the* λμ2*-calculus.*

## **5 Conclusions and Further Directions**

We have described a "Curry-style" approach to game semantics, and used it to give new models of polymorphism. Various existing models may also be framed as typed interaction systems, such as the semantics of call-by-value in [12]. Nor are instances restricted to operational game semantics: for example we can present linear combinatory algebras of games and strategies in this way, and potentially other models of concurrent interaction. Unlike basic Church-style game semantics, these models give the opportunity to make finer distinctions between programs based on internal behaviour, which we have not explored here.

The notion of typed interaction structure reflects only limited structure of our models, but may be developed further. Having characterized parallel composition plus hiding within this setting, a natural next step would be a notion of copycat strategy, leading to structure for sharing and discarding information. One goal for such a development would be to put the generalization of congruence from configurations to terms on a systematic footing.

In another direction, our models of polymorphism may be developed further. In particular combining and fully exploiting generic and abstract data types often requires *higher-order* polymorphism, in which quantifiers range over *type operators* (functions which take types as arguments and return them as values). Whereas this is difficult to represent in game semantics, our model readily extends to a typing system based on System Fω, which allows quantification over type-operators: the price to pay is that satisfiability of configuration types (and thus effective presentation of the states of our LTS) requires the solution of higher-order unification problems, which are undecidable, in general.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/ 4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### **An Axiomatic Approach to Reversible Computation***-*

Ivan Lanese1 ( ), Iain Phillips2 , and Irek Ulidowski3

1 Focus Team, University of Bologna/INRIA, Italy<EMAIL_ADDRESS>
2 Imperial College London, England<EMAIL_ADDRESS>
3 University of Leicester, England<EMAIL_ADDRESS>
**Abstract.** Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.

**Keywords:** Reversible Computation, Labelled Transition System with Independence, Causal Safety, Causal Liveness

## **1 Introduction**

Reversible computing studies computations which can proceed both in the standard, forward direction, and backward, going back to past states. Reversible computation has attracted interest due to its applications in areas as different as low-power computing [15], simulation [4], robotics [21], biological modelling [31] and debugging [23].

c The Author(s) 2020

- This work has been partially supported by COST Action IC1405 on Reversible Computation - Extending Horizons of Computing. The first author has also been partially supported by French ANR project DCore ANR-18-CE25-0007 and by INdAM as a member of GNCS (Gruppo Nazionale per il Calcolo Scientifico).

J. Goubault-Larrecq and B. K¨onig (Eds.): FOSSACS 2020, LNCS 12077, pp. 442–461, 2020. https://doi.org/10.1007/978-3-030-45231-5\_23

There is widespread agreement in the literature about what properties characterise reversible computation in the sequential setting. Thus in reversible finite state automata [32], reversible cellular automata [13], reversible Turing machines [2] and reversible programming languages such as Janus [35] the main point is that the mapping from inputs to outputs is injective, and the reverse computation is deterministic.

Matters are less clear when it comes to reversible computation in the concurrent setting. Indeed, various reversible concurrent models have been studied, most notably in the areas of process calculi [6,29,18], event structures [34], Petri nets [1,25] and programming languages such as Erlang [20].

A main result of this line of research is that the notion of reversibility most suited for concurrent systems is *causal-consistent reversibility* (other notions are also used, e.g., to model biological systems [31]). According to an informal account of causal-consistent reversibility, any action can be undone provided that its consequences, if any, are undone beforehand. Following [6] this account is formalised using the notion of causal equivalent traces: two traces are causal equivalent if and only if they only differ for swapping independent actions, and inserting or removing pairs of an action and its reverse. According to [6, Section 3]

Backtracking an event is possible when and only when a causally equivalent trace would have brought this event as the last one

which is then formalised as the so called causal consistency (CC) [6, Theorem 1], stating that coinitial computations are causal equivalent if and only if they are cofinal. Our new proof of CC (Proposition 3.6) shows that it holds in essentially any reversible formalism satisfying the Loop Lemma and the Parabolic Lemma, and we believe that CC is insufficient on its own to capture the informal notion.

A formalisation closer to the informal statement above is provided in [20, Corollary 22], stating that a forward transition t can be undone after a derivation iff all its consequences, if any, are undone beforehand. We are not aware of other discussions trying to formalise such a notion, except for [30], in the setting of reversible event structures. In [30], a reversible event structure is *cause-respecting* if an event cannot be reversed until all events it has caused have also been reversed; it is *causal* if it is cause-respecting and a reversible event can be reversed if all events it has caused have been reversed [30, Definition 3.34].

We provide (Section 4) a novel definition of the idea above, composed by:

We shall see that CC does not capture the same property as CS+CL (Examples 4.15, 4.37), and that there are slightly different versions of CS and CL, which can all be proved under a small set of reasonable assumptions.

The main aim of this paper is to take an abstract model, namely labelled transition systems with independence equipped with reverse transitions (Section 2), and to show that the properties above (as well as others) can be derived

**Table 1.** Axioms and properties for causal reversibility.

from a small set of simple axioms (Sections 3, 4, 5). This is in sharp contrast with the large part of works in the literature, which consider specific frameworks such as CCS [6], CCS with broadcast [26], CCB [14], π-calculus [5], higher-order π [18], Klaim [11], Petri nets [25], μOz [22] and Erlang [20], and all give similar but formally unrelated proofs of the same main results. Such proofs will become instances of our general results. More precisely, our axioms will:

Thus, when defining a new reversible formalism, one just has to check whether the axioms hold, and get for free the proofs of the most relevant properties. Notably, the axioms are normally easier to prove than the properties, hence the assessment of a reversible calculus gets much simpler.

As a reference, Table 1 lists the axioms and properties used in this paper.

In order to understand which kinds of behaviours are incompatible with a causal-consistent reversible setting, consider the following LTSs in CCS:

a.**0** a → **0,** b.**0** b → **0:** from state **0** one does not know whether to go back to a.**0** or to b.**0**;

We remark that all such behaviours are perfectly reasonable in CCS, and they are dealt with in the reversible setting by adding history information about past actions. For example, in the first case one could remember the initial state, in the second case both the initial state and the action taken, and in the last case the number of iterations that have been performed.

Due to space constraints, some proofs and additional results can only be found in the companion technical report [16].

## **2 Labelled Transition Systems with Independence**

We want to study reversibility in a setting as general as possible. Thus, we base on the core of the notion of *labelled transition system with independence* (LTSI) [33, Definition 3.7]. However, while [33] requires a number of axioms on LTSI, we take the basic definition and explore what can be done by adding or not adding various axioms. Also, we extend LTSI with reverse transitions, since we study reversible systems. We define first labelled transition systems (LTSs).

We consider the LTS of the entire set of processes in a calculus, rather than the transition graph of a particular process and its derivatives, hence we do not fix an initial state.

**Definition 2.1.** *A* labelled transition system (LTS) *is a structure* (Proc, Lab,)*, where* Proc *is the set of states (or processes),* Lab *is the set of action labels and* ⊆ Proc × Lab × Proc *is a* transition relation*.*

We let P, Q, . . . range over processes, a, b, c, . . . range over labels, and t, u, v, . . . range over transitions. We can write t : P a → Q to denote that t = (P, a, Q). We call a-transition a transition with label a.

**Definition 2.2 (LTS with independence).** *We say that* (Proc, Lab,→, ι) *is an* LTS with independence *(LTSI) if* (Proc, Lab,→) *is an LTS and* ι *is an irreflexive symmetric binary relation on transitions.*

In many cases (see Section 6), the notion of independence coincides with the notion of concurrency. However, this is not always the case. Indeed, concurrency implies that transitions are independent since they happen in different processses, but transitions taken by the same process can be independent as well. Think, for instance, of a reactive process that may react in any order to two events arriving at the same time, and the final result does not depend on the order of reactions.

We shall assume that all transitions are reversible, so that the Loop Lemma [6, Lemma 6] holds. This does not hold in models of reversibility with control mechanisms such as irreversible actions [6,7] or a rollback operator [17]. Nevertheless,

when showing properties of models with controlled reversibility it has proved sensible to first consider the underlying models where all transitions are reversible, and then study how control mechanisms change the picture [11,20]. The present work helps with the first step.

**Definition 2.3.** *Given* (Proc, Lab,)*, let the* reverse LTS *be* (Proc, Lab,-)*, where* P a - Q *iff* Q a P*. It is convenient to combine the two LTSs (forward and reverse): let the reverse labels be* Lab = {a : a ∈ Lab}*, and define the combined LTS to be* → ⊆ Proc × (Lab ∪ Lab) × Proc *by* P a → Q *iff* P a Q *and* P a → Q *iff* P a -Q*.*

We stipulate that the union Lab∪Lab is disjoint. We let α, . . . range over Lab∪Lab. For α ∈ Lab ∪ Lab, the *underlying* action label und(α) is defined as und(a) = a and und(a) = a. Let a = a for a ∈ Lab. Given t : P α → Q, let t : Q α → P be the transition which reverses t.

We let ρ, σ, . . . range over finite sequences α1 ...αn, with εP representing the empty sequence starting and ending at P. We shall write ε when P is understood. Given an LTS, a *path* is a sequence of forward or reverse transitions of the form P0 → α1 P1 ··· α →n Pn. We let r, s, . . . range over paths. We may write r : P ρ →∗ Q where the intermediate states are understood. On occasion we may refer to a path simply by its sequence of labels ρ. Given a path r : P ρ →∗ Q, the inverse path is r : Q ρ →∗ P where ε = ε and αρ = ρ α. The length of a path r (notated |r|) is the number of transitions in the path. Paths r : P ρ →∗ Q and R σ →∗ S are *coinitial* if P = R and *cofinal* if Q = S. We say that a path is *forward-only* if it contains no reverse transitions.

Let (Proc, Lab,→) be an LTS. The irreversible processes in (Proc, Lab,→) are Irr = {P ∈ Proc : P -}.

In the following we will consider LTSIs obtained by adding a notion of independence to combined LTSs as above. We will call the result a *combined LTSI*.

## **3 Basic Properties**

In this section we show that most of the properties in the reversibility literature (see, e.g., [6,29,18,20]), in particular the parabolic lemma and causal consistency, can be proved under minimal assumptions on the combined LTSI under analysis.

We formalise the minimal assumptions using three axioms, described below.

**Definition 3.1 (Basic axioms).** *Let* L = (Proc, Lab,→, ι) *be a combined LTSI. We say* L *satisfies:*

**Square Property (SP)** if whenever t : P α → Q, u : P β → R with tιu then *there are cofinal transitions* u- : Q β → S and t - : R α → S;

**Backward Transitions are Independent (BTI)** if whenever t : P a - Q and t - : P b - Q and t -= t then tιt- ;

**Well-Foundedness (WF)** *if there is no infinite reverse computation, i.e. we do not have* Pi *(not necessarily distinct) such that* Pi+1 → ai Pi *for all* i = 0, 1,...*.*

WF can alternatively be formulated using backward transitions, but the current formulation makes sense also in non-reversible calculi (e.g., CCS), which can be used as a comparison. Let us discuss the intuition behind these axioms. SP takes its name from the Square Lemma, where it is proved for concrete calculi and languages in [6,18,20], and captures the idea that independent transitions can be executed in any order, that is they form commuting diamonds. SP can be seen as a sanity check on the chosen notion of independence. BTI generalises the key notion of backward determinism used in sequential reversibility (see, e.g., [32] for finite state automata and [35] for the imperative language Janus) to a concurrent setting. Backward determinism can be spelled as "two coinitial backward transitions do coincide". This can be generalised to "two coinitial backward transitions are independent". Finally, WF means that we consider systems which have a finite past. That is, we consider systems starting from some initial state and then moving forward and back.

Axioms SP and BTI are related to properties which are part of the definition of (occurrence) transition systems with independence in [33, Definitions 3.7, 4.1]. WF was used as an axiom in [28].

Using the minimal assumptions above we can prove relevant results from the literature. We first define causal equivalence, equating computations differing only for swaps of independent transitions and simplification of a transition with its reverse.

**Definition 3.2 (cf. [6]).** *Let* (Proc, Lab,→, ι) *be an LTSI satisfying SP. Let* ≈ *be the smallest equivalence relation on paths closed under composition and satisfying:*

We first consider the Parabolic Lemma ([6, Lemma 10]), which states that each path is causal equivalent to a backward path followed by a forward path.

**Definition 3.3. Parabolic Lemma (PL)***: for any path* r *there are forwardonly paths* s, s *such that* r ≈ ss *and* |s| + |s |≤|r|*.*

**Proposition 3.4.** *Suppose an LTSI satisfies BTI and SP. Then PL holds.*

The proof of Proposition 3.4 (available in [16]) is very similar to that of [6, Lemma 10] except that in the latter BTI is shown directly as part of the proof.

A corollary of PL is that if a process is reachable from an irreversible process, then it is also forwards reachable from it. In other words, making a system reversible does not introduce new reachable states but only allows one to explore differently forwards reachable states. This is relevant in reversible debugging of concurrent systems [10,20], where one wants to find bugs that actually occur in forward-only computations. See the companion technical report [16, Corollary A.1]. We now move to causal consistency [6, Theorem 1].

## **Definition 3.5. Causal Consistency (CC)***: if* r *and* s *are coinitial and cofinal then* r ≈ s*.*

Essentially, causal consistency states that history information allows one to distinguish computations which are not causal equivalent, indeed, if two computations are cofinal, that is they reach the same final state (which includes the stored history information) then they need to be causal equivalent.

Causal consistency frequently includes the other direction, namely that coinitial causal equivalent computations are cofinal, meaning that there is no way to distinguish causal equivalent computations. This second direction follows easily from the definition of causal equivalence.

Notably, our proof of CC below is very much shorter than existing proofs.

**Proposition 3.6.** *Suppose an LTSI satisfies WF and PL. Then CC holds.*

*Proof.* Let r : P ρ →∗ Q and r : P ρ- →∗ Q. Using WF, let I,s be such that s : I σ →∗ P, I ∈ Irr. Now srsr is a path from I to I, and so by PL there are r1, r2 forward-only such that r1r2 ≈ srsr . But I ∈ Irr and so r1 = ε and r2 = ε. Thus ε ≈ srsr , so that sr ≈ sr and r ≈ r as required.

Causal consistency implies the unique transition property.

**Definition 3.7.** *An LTSI* (Proc, Lab,→, ι) *satisfies Unique Transition (UT) if* P a → Q *and* P b → Q *imply* a = b*.*

#### **Corollary 3.8.** *If an LTSI satisfies CC then it satisfies UT.*

UT was shown in the forward-only setting of occurrence TSIs in [33, Corollary 4.4]; it was taken as an axiom in [28].

*Example 3.9 (PL alone does not imply WF or CC).* Consider the LTSI with states Pi for i = 0, 1,... and transitions ti : Pi+1 a → Pi, ui : Pi+1 b → Pi with a = b and ti ι ui. BTI and SP hold. Hence PL holds by Proposition 3.4. However clearly WF fails. Also ti and ui are coinitial and cofinal, and a = b, so that UT fails, and hence CC fails using Corollary 3.8. Note that the ab diamonds here have the same side states so are degenerate (cf. Lemma 4.4).

## **4 Causal Safety and Causal Liveness**

In the literature, causal consistent reversibility is frequently informally described by saying that "a transition can be undone if and only if each of its consequences, if any, has been undone". In this section we study this property, where the two implications will be referred to as causal safety and causal liveness. We provide three different versions of such properties, based on independence of transitions (Section 4.2), ordering of events (Section 4.3), and independence of events (Section 4.4), and study their relationships. In order to define such properties we need the concept of event.

#### **4.1 Events**

**Definition 4.1 (Event, general definition).** *Let* (Proc, Lab,→, ι) *be an LTSI.  The equivalence classes of forward transitions, written* [P, a, Q]*, are the* events*. The equivalence classes of reverse transitions, written* [P, a, Q]*, are the* reverse events*. Define a labelling function from* → / ∼ *to* Lab *by setting* ([P, α, Q]) = α*.*

Events are introduced as a derived notion in an LTS with independence in [33], in the context of forward-only computation. We have changed their definition by using coinitial independence at all corners of the diamond, yielding rotational symmetry. This reflects our view that forward and backward transitions have equal status.

Our definition can be simplified if the LTSI, and independence in particular, are well-behaved. Thus, we now add a further axiom related to independence.

CPI states that independence is a property of commuting diamonds more than of their specific pairs of edges. Indeed, it allows independence to propagate around a commuting diamond.

**Definition 4.3.** *If a combined LTSI satisfies axioms SP, BTI, WF and CPI, we say that it is* pre-reversible*.*

The name 'pre-reversible' indicates that we expect to require further axioms, but the present four are enough to ensure that LTSIs are well-behaved, with events compatible with causal equivalence. Pre-reversible axioms are separated from further axioms by a dashed line in Table 1.

The following non-degeneracy property was shown for occurrence transition systems with independence in [33, page 312], which have forward transitions only. We have to cope with backwards as well as forward transitions.

**Lemma 4.4.** *Suppose that an LTSI is pre-reversible. If we have a diamond* t : P α → Q*,* u : P β → R *with* tιu *together with cofinal transitions* u : Q β → S *and* t : R α → S*, then the diamond is* non-degenerate*, meaning that* P, Q, R, S *are distinct states.*

If an LTSI is pre-reversible then by Lemma 4.4 and the use of CPI we can simplify the statement of Definition 4.1 to:

**Definition 4.5 (Event, simplified definition).** *Let* (Proc, Lab,→, ι) *be a prereversible LTSI. Let* ∼ *be the smallest equivalence relation satisfying: if* t : P α → Q*,* u : P β → R*,* u : Q β → S*,* t : R α → S*, and* tιu*, then* t ∼ t *.*

We are now able to show independence of diamonds (ID), which can be seen as dual of SP.

**Definition 4.6 (Independence of Diamonds (ID)).** *An LTSI satisfies the Independence of Diamonds property (ID) if whenever we have a diamond* t : P α → Q*,* u : P β → R*,* u : Q β → S *and* t : R α → S*, with*

**–** Q = R *if* α *and* β *are both forwards or both backwards;* **–** P = S *otherwise;*

*then* tιu*.*

**Proposition 4.7.** *If an LTSI satisfies BTI and CPI then it satisfies ID.*

We now consider the interaction between events and causal equivalence. We need some notation first.

**Definition 4.8.** *Let* r *be a path in an LTSI* L *and let* e *be an event of* L*. Let* (r, e) *be the number of occurrences of transitions* t *in* r *such that* t ∈ e*, minus the number of occurrences of transitions* t *in* r *such that* t ∈ e*.*

We now show that (r, e) is invariant under causal equivalent traces.

**Lemma 4.9.** *Let* L *be a pre-reversible LTSI. Let* r ≈ s*. Then for each event* e *we have that* (r, e) = (s, e)*.*

Lemma 4.9 generalises what was shown for the forward-only setting in [33, Corollary 4.3].

**Proposition 4.10.** *If an LTSI is pre-reversible, then for any rooted path* r *and any forward event* e *we have* (r, e) ≥ 0*.*

#### **4.2 CS and CL via Independence of Transitions**

We first define causal safety and liveness using the independence relation.

**Definition 4.11.** *Let* L = (Proc, Lab,→, ι) *be a pre-reversible LTSI.*

**Fig. 1.**

We may wish to close the independence relation over this axiom:

**Definition 4.12 (Independence Respects Events (IRE)).** *Whenever* t ∼ t ι u *we have* tιu*.*

IRE is one of the conditions in the definition of transition systems with independence [33, Definition 3.7]. Together with the axioms for pre-reversibility, it is enough to show both causal safety and causal liveness.

**Theorem 4.13.** *Let a pre-reversible LTSI satisfy IRE. Then it satisfies CS.*

#### **Theorem 4.14.** *Let a pre-reversible LTSI satisfy IRE. Then it satisfies CL.*

CS and CL are not derivable from CC; we give an example LTSI which satisfies CC but not CS and not CL.

*Example 4.15.* Consider the LTS in Figure 1. Independence is mostly coinitial and given by closing under BTI and CPI. Additionally we make the leftmost atransition independent with all b-transitions. Note that all a-transitions belong to the same event, and all b-transitions belong to the same event. Also SP and WF hold, so that the LTSI is pre-reversible, and CC holds. However IRE does not hold. Furthermore CS fails using Definition 4.11. Indeed, consider any path bab →∗ from the start. CS would imply that the first b is independent with the a but this is not the case (we do have b ι a).

Also CL fails using Definition 4.11. Indeed, consider any path abb →∗ from the start. Since the leftmost a-transition is independent with all b-transitions, we should be able to reverse a at the end of the path, but this is not possible.

The next axiom states that independence is fully determined by its restriction to coinitial transitions. This is related to axiom (E) of [33, page 325], but here we allow reverse as well as forward transitions.

*then there are* t 1 ∼ t1*,* t 2 ∼ t2 *such that* t 1 *and* t 2 *are coinitial and* t 1 ι t 2*.* **Definition 4.16 (Independence of Events is Coinitial (IEC)).** If t1 ι t2

Thanks to previous axioms, independence behaves well w.r.t. reversing.

**Definition 4.17 (Reversing Preserves Independence (RPI)).** If tιt- then t ι t- .

**Proposition 4.18.** *If an LTSI satisfies SP, CPI, IRE, IEC then it also satisfies RPI.*

All the axioms that we have introduced are independent, i.e. none is derivable from the remaining axioms.

**Proposition 4.19.** *SP, BTI, WF, CPI, IRE, IEC are independent of each other.*

## **4.3 CS and CL via Ordering of Events**

To define CS and CL via ordering of events, we define the causality relation ≤ on events.

**Definition 4.20.** *Let* L = (Proc, Lab,→, ι) *be an LTSI. Let* e, e *be events of* L*. Let* e ≤ e *iff for all rooted paths* r*, if* (r, e ) > 0 *then* (r, e) > 0*. As usual* e<e *means* e ≤ e *and* e = e *. If* e<e *we say that* e *is a* cause *of* e *.*

**Lemma 4.21.** *If an LTSI satisfies SP, BTI, WF and CPI then* ≤ *is a partial ordering on events.*

Previously, orderings on events have been defined using forward-only rooted paths; in fact, the definitions coincide for pre-reversible LTSIs.

**Definition 4.22 ([12,28]).** *Let* L = (Proc, Lab,→, ι) *be an LTSI. Let* e, e *be events of* L*. Let* e ≤f e *iff for all rooted forward-only paths* r*, if* r *contains a representative of* e *then* r *also contains a representative of* e*.*

**Lemma 4.23.** *For any LTSI,* e ≤ e *implies* e ≤f e *. If an LTSI satisfies SP, BTI, WF and CPI then* e ≤f e *implies* e ≤ e *.*

*Proof.* Straightforward using PL and Lemma 4.9.

We now give definitions of causal safety and causal liveness using ordering on events.

**Definition 4.24.** *Let* L = (Proc, Lab,→, ι) *be an LTSI.*

We postpone giving proofs of CS< and CL< until we have introduced a further definition of causal safety and liveness using independence of events.

#### **4.4 CS and CL via Independent Events**

We now introduce a third version of causal safety and liveness, which uses independence like CS and CL, but on events rather than on transitions. First we lift independence from transitions to events.

**Definition 4.25 (Coinitially independent events).** *Let events* e, e *be* (coinitially) independent*, written* e ci e *, iff there are coinitial transitions* t, t *such that* [t] = e*,* [t ] = e *and* tιt *.*

**Lemma 4.26.** *If an LTSI is pre-reversible, then if* e ci e *we have also* e ci e *.*

Thus in pre-reversible LTSIs, ci is fully determined just considering forward events. By Lemma 4.26, if we know e ci e then we know und(e) ci und(e ).

We can give a third formulation of causal safety and liveness using ci:

**Definition 4.27.** *Let* L = (Proc, Lab,→, ι) *be a pre-reversible LTSI.*

Note that in Definition 4.27 we operate at the level of events, rather than at the level of transitions as in Definition 4.11.

**Theorem 4.28.** *If an LTSI is pre-reversible then it satisfies CS*ci*.*

We now introduce a weaker version of axiom IRE (Definition 4.12).

**Definition 4.29 (Coinitial IRE (CIRE)).** *If* [t] ci [u] *and* t, u *are coinitial then* tιu*.*

**Theorem 4.30.** *If a pre-reversible LTSI satisfies CIRE then it satisfies CL*ci*.*

We next give an example where CC holds but not CSci (and not CPI).

*Example 4.31.* Consider the cube with transitions a, b, c on the left in Figure 2, where the forward direction is from left to right. We add independence as given by BTI. So SP, BTI, WF hold, but not CPI. From the start we have an atransition followed by a path r = bc followed by a. For CSci to hold, we want a to be the reverse of the same event as the first a. They are connected by a ladder with sides cb. We add independence for all corners on the two faces of the ladder (ab and ac). Then we get bc ≈ cb (independence at a single corner is enough). However the bs are not the same event since the bc face does not have independence at each corner. Therefore we do not get [a] ci [b], and CSci fails.

We next give an example where CSci and CLci hold but not CC.

**Fig. 2.**

*Example 4.32.* Consider the LTSI with Qi b → Pi, Pi+1 c → Pi, Qi+1 c → Qi, Pi+1 a → Qi for i = 0, 1,.... This is shown on the right in Figure 2. Clearly WF does not hold. We add coinitial independence to make BTI and CPI hold. Then also SP and CIRE hold. However, CC fails since, for example P1 a → Q0 b → P0 and P1 c → P0 are coinitial and cofinal but not causally equivalent. Note that there are just three events a, b, c with a ci c, b ci c but not a ci b. CSci and CLci hold. Indeed, c is independent from every other action, and it can always be undone, while a and b are independent from c only and they can be undone after any path composed by c and no others.

### **4.5 Polychotomy**

In this section we relate our three versions of causal safety and liveness, with the help of what we call *polychotomy*, which states that if events do not cause each other and are not in conflict, then they must be independent. We start by defining a conflict relation on events.

**Definition 4.33.** *Two forward events* e, e *are in* conflict*, written* e # e *, if there is no rooted path* r *such that* (r, e) > 0 *and* (r, e ) > 0*.*

Much as for orderings, conflict on events has been defined previously using forward-only rooted paths [12,28]; in fact, the definitions coincide for pre-reversible LTSIs. We omit the details.

**Definition 4.34 (Polychotomy).** *Let* L *be a pre-reversible LTSI. We say that* L *satisfies* polychotomy *if whenever* e, e *are* forward *events, then exactly one of the following holds: 1.* e = e *; 2.* e<e *; 3.* e < e*; 4.* e # e *; or 5.* e ci e *.*

Property NRE below is related to polychotomy.

*any forward event* e *we have* (r, e) ≤ 1*.* **Definition 4.35 (No Repeated Events (NRE)).** In any rooted path r, for

**Lemma 4.36 (Polychotomy).** *Suppose that a pre-reversible LTSI satisfies NRE. Then polychotomy holds.*

**Fig. 3.**

*Example 4.37.* Consider the LTSI in Figure 3. We add independence to make BTI and CPI hold. Both SP and WF hold. Hence, CC holds as well. There are three events, labelled with a, b, c. Clearly NRE fails for both a and b. We see that a<c but also a ci c, so that polychotomy fails. CSci holds by Theorem 4.28. However CS< fails: consider the transition P a → Q together with the path r : Q bc →∗ R and S a → R, and note that a<c.

The next lemma allows us to connect ordered safety and liveness with coinitial safety and liveness.

**Lemma 4.38.** *Suppose that a pre-reversible LTSI satisfies NRE. Suppose* P a → Q*,* e = [P, a, Q]*,* r : Q ρ →∗ R *and* (r, e ) > 0 *where* e *is a forward event. Then exactly one of* e ci e *and* e<e *holds.*

**Proposition 4.39.** *Suppose that a pre-reversible LTSI* L *satisfies NRE. Then*

Property RED below is also related to NRE and polychotomy.

**Definition 4.40.** *An LTSI satisfies Reverse Event Determinism (RED) if whenever* t, t *are backward coinitial transitions and* t ∼ t *then* t = t *.*

**Proposition 4.41.** *If a LTSI* L *is pre-reversible then the following are equivalent: 1.* L *satisfies NRE; 2.* L *satisfies RED; 3. independence* ci *is irreflexive on events; and 4. polychotomy holds.*

**Proposition 4.42.** *Suppose that a pre-reversible LTSI satisfies CIRE. Then it also satisfies NRE.*

NRE was shown in the forward-only setting of occurrence transition systems with independence in [33, Corollary 4.6]. It was also shown in the reversible setting without independence in [28, Proposition 2.10].

*Example 4.43.* Consider the LTSI in Figure 4. Independence is given by closing under BTI and CPI. There are three events, labelled a, b, c, which are all independent of each other. We see that NRE holds but not CIRE. Also CLci and CL< fail: consider P a → Q b → R, where a cannot be reversed at R.

**Fig. 4.**

**Proposition 4.44.** *Let* L *be a pre-reversible LTSI.*

## **5 Coinitial Independence**

In this section we consider coinitial LTSIs, defined as follows, and their relationship with LTSIs in general.

**Definition 5.1.** *Let* L = (Proc, Lab,→, ι) *be a combined LTSI. Then* ι *is* coinitial *if for all transitions* t, u*, if* tιu *then* t *and* u *are coinitial. We say that* L *is coinitial if* ι *is coinitial.*

We define a mapping c restricting general independence to coinitial transitions and a mapping g extending independence along events.

 Furthermore, define* t c(ι) u *iff* tιu *and* t, u *are coinitial.*

**Proposition 5.3.** *Let* L = (Proc, Lab,→, ι) *be a pre-reversible LTSI.*

Thanks to Proposition 5.3, we can extend a coinitial pre-reversible LTSI satisfying CIRE in a canonical way to a pre-reversible LTSI satisfying IRE and IEC.

In some reversible calculi (such as RCCS) independence of coinitial transitions is defined purely by reference to the labels. If this is the case it is a simple matter to verify the axioms CPI and CIRE.

**Proposition 5.4.** *Let* L = (Proc, Lab,→, ι) *be a coinitial combined LTSI.  Then* L *satisfies CPI and CIRE.*

*Proof.* Straightforward, noting that labels on opposite sides of a diamond of transitions must be equal.

Note that I must be irreflexive, since ι is irreflexive.

If we have a coinitial pre-reversible LTSI satisfying CIRE then CS< and CL< hold (using Proposition 4.42 and Proposition 4.39). Applying mapping g we get a general pre-reversible LTSI satisfying IRE and IEC by Proposition 5.3. This will satisfy CS and CL as a result of applying Theorem 4.13 and Theorem 4.14 respectively. It will also satisfy CS< and CL<. Conversely, if we have a general pre-reversible LTSI satisfying IRE then CS and CL hold by Theorem 4.13 and Theorem 4.14 respectively. Applying mapping c we get a coinitial pre-reversible LTSI satisfying CIRE. This will satisfy CS< and CL< .

## **6 Case Studies**

We look at whether our axioms hold in various reversible formalisms. Remarkably, all the works below provide proofs of the Loop Lemma.

**RCCS** We consider here the semantics of RCCS in [6], and restrict the attention to coherent processes [6, Definition 2]. In RCCS, transitions P μ:ζ → Q and P μ- :ζ- → Q are concurrent if μ∩μ = ∅ [6, Definition 7]. This allows us to define coinitial independence as tιu iff t and u are concurrent. We now argue that the resulting coinitial LTSI is pre-reversible and also satisfies CIRE. SP was shown in [6, Lemma 8]. BTI was shown in the proof of [6, Lemma 10]. WF is straightforward, noting that backward transitions decrease memory size. Hence, we obtain a very much simplified proof of CC. For CPI and CIRE we note that independence is defined on the underlying labels and thus Proposition 5.4 applies. Therefore CS< and CL< hold. Using Proposition 5.3, we can get an LTSI with general independence satisfying IRE and IEC, and therefore CS and CL. This is the first time these causal properties have been proved for RCCS.

**HO***π* We consider here the uncontrolled reversible semantics for HOπ [18]. We restrict our attention to reachable processes, called there consistent. The semantics is a reduction semantics; hence there are no labels (or, equivalently, all the labels coincide). To have more informative labels we can consider the transitions defined in [18, Section 3.1], where labels are composed of memory information and a flag denoting whether the transition is forward or backward. The notion of independence would be given by the concurrency relation on coinitial transitions [18, Definition 9]. All pre-reversible LTSI axioms hold, as well as CIRE which is needed for causal safety and liveness. Specifically, SP is proved in [18, Lemma 9]. BTI holds since distinct memories have disjoint sets of keys [18, Definition 3 and Lemma 3] and by the definition of concurrency [18, Definition 9]. WF holds as each backward step consumes a memory, which is finite to start with. Finally, CPI and CIRE are valid since the notion of concurrency is defined on the annotated labels and using our Proposition 5.4.

As a result we obtain a very much simplified proof of CC. Moreover, using CPI and CIRE, we get the CS< and CL< safety and liveness properties and, applying mapping g from Section 5, we get a general pre-reversible LTSI satisfying IRE and IEC, hence CS and CL are satisfied. This is the first time that causal properties have been shown for HOπ.

**R***π* We consider the (uncontrolled) reversible semantics for π-calculus defined in [5]. We restrict the attention to reachable processes. The semantics is an LTS semantics. Independence is given as concurrency which is defined for consecutive transitions [5, Definition 4.1]. CC holds [5, Theorem 4.5].

Our results are not directly applicable to Rπ, since SP holds up to label equivalence of transitions on opposite sides of the diamond, rather than equality of labels as in our approach. We would need to extend axiom SP and the definition of causal equivalence to allow for label equivalence in order to handle Rπ using our axiomatic method.

**Erlang** We consider the uncontrolled reversible (reduction) semantics for Erlang in [20]. We restrict our attention to reachable processes. In order to have more informative labels we can consider the annotations defined in [20, Section 4.1]. We then can define coinitial transitions to be independent if they are concurrent [20, Definition 12].

We next discuss the validity of our axioms in reversible Erlang. SP is proved in [20, Lemma 13] and BTI is trivial from the definition of concurrency [20, Definition 12]. WF holds since the pairs of integers (total number of elements in memories, total number of messages queued) ordered under lexicographic order are always positive and decrease at each backward step. Intuitively, each step but the ones derived using the rule for reverse sched (see [20, Figure 11]) consumes an item of memory, and each step derived using rule reverse sched removes a message from a process queue. Finally, CPI and CIRE hold since the notion of concurrency is defined on the annotated labels, and by Proposition 5.4.

Since this the setting is very similar to the one of HOπ (both calculi have a reduction semantics and a coinitial notion of independence defined on enriched labels), we get the same results as for HOπ, including CC, and CS and CL.

**Reversible occurrence nets** Reversible occurrence nets [25,24] are traditional occurrence nets (safe and with no backward conflicts) extended with a reverse transition for each forward transition. They give rise to an LTS where states are pairis (N,m) with N a net and m a marking. A computation that represents firing a transition t in (N,m) and resulting in (N,m ) is given by a firing relation (N,m) t → (N,m ). The notion of independence is the concurrency relation [25, Section 3] which is defined between arbitrary firings (transitions). Hence, we get a general LTSI. The CC property is shown by following the traditional approach in [6]. SP and PL are shown as well. PL and CC require several pages of proofs [24]. The causal safety and causal liveness properties are not considered in [25,24].

We can obtain CC, and additionally CS and CL, as follows. SP and BTI are proved for reversible occurrence nets in [24] as Lemma 4.3 and Lemma 3.3 respectively. WF holds because there are no forward cycles of firings in occurrence nets, hence no infinite reverse paths. In order to have CS and CL, we need to show CPI and IRE. Lemma 3.4 in [24] gives CPI. Events can be defined on firings as in our Definition 4.5, and then IRE holds as the concurrency relation preserves such events.

## **7 Conclusion, Related and Future Work**

The literature on causal-consistent reversibility (see, for example the early survey [19]) has a number of proofs of results such as the parabolic lemma (PL) and the causal consistency property (CC), all of which are instantiated to a specific calculus, language or formalism. We have taken here a complementary approach, analysing the properties of interest in an abstract and language-independent setting. In particular, we have shown how to prove the most relevant of these properties from a small number of axioms.

Our approach builds upon [28], where a set of axioms for reverse LTSs was given and several interesting properties were shown. While the idea is similar, the development is rather different since we consider more basic axioms (we only share WF, while many of the axioms in [28], such as UT, follow from ours), and since the two papers focus on different properties. We focus on CC and various forms of CS and CL, while [28] considers correspondence with prime event structures and reversible bisimulations. Moreover, LTSs in [28] do not have a notion of independence.

In other related work, we may particularly mention [8], which like ours takes an abstract view, though based on category theory. However, its results concern irreversible actions, and do not provide insights in our setting, where all actions are reversible. The only other work which takes a general perspective is [3], which concentrates on how to derive a reversible extension of a given formalism. However, proofs concern a limited number of properties (essentially our CC), and hold only for extensions built using the technique proposed there. Also [27,29] are general, since they propose how to reverse a calculus that can be defined in a general format of SOS rules. However, the format has its syntactic constraints while our approach abstracts from them. Finally, [9] presents a number of properties such as, for example, backward confluence, which arise in the context of reversing of steps of executed transitions in Place/Transition nets.

The approach proposed in this paper opens a number of new possibilities. Firstly, when devising a new reversible formalism, our results provide a rich toolbox to prove (or disprove) relevant properties in a simple way. This is particularly relevant since causal-consistent reversibility is getting applied to more and more complex languages, such as Erlang [20], where direct proofs become cumbersome and error-prone. Secondly, our abstract proofs are relatively easy to formalise in a proof-assistant, which is even more relevant given that this will certify the correctness of the results for many possible instances. Another possible extension of our work concerns integrating into our framework irreversible actions [7]. In order to do that we could take inspiration from the above-mentioned [8].

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **An Auxiliary Logic on Trees: on the Tower-hardness of logics featuring reachability and submodel reasoning**

Alessio Mansutti(-)

LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay<EMAIL_ADDRESS>
**Abstract.** We describe a set of simple features that are sufficient in order to make the satisfiability problem of logics interpreted on trees TOWER-hard. We exhibit these features through an *Auxiliary Logic on Trees* (ALT), a modal logic that essentially deals with reachability of a fixed node inside a forest and features modalities from sabotage modal logic to reason on submodels. After showing that ALT admits a TOWER-complete satisfiability problem, we prove that this logic is captured by four other logics that were independently found to be TOWER-complete: twovariables separation logic, quantified computation tree logic, modal logic of heaps and modal separation logic. As a by-product of establishing these connections, we discover strict fragments of these logics that are still non-elementary.

## **1 Introduction**

In mathematical logic there is a well-known trade-off between expressive power and complexity, where weaker languages cannot capture interesting properties of complex systems, whereas finding solutions of a given problem is infeasible for richer languages. For instance, many verification tasks, such as reachability and homomorphisms queries, happen to be expressible in monadic second-order logic (MSO) [15]. This logic is however not usable in practice, as its satisfiability problem SAT(MSO) is undecidable in general and was famously proved by Rabin [36] to be decidable but non-elementary when the logic is interpreted on trees or on one unary function. A more recent analysis that uses the hierarchy of non-elementary ranking functions [38] classifies SAT(MSO) on these two structures as TOWER-complete, i.e. complete for the class of problems of time complexity bounded by a tower of exponentials, whose height is an elementary function of the input.

In order to bypass these problems, a general approach is to design restrictions of MSO that can solve complex reasoning tasks while being more appealing complexity-wise. An example of this is given by the framework of temporal logics, formalisms that describe the evolution of reactive systems [24]. Among the various temporal logics, from the classical linear temporal logic (LTL) [39] and computation tree logic (CTL) [13], as well as their fragments [2,33], to the more recently developed interval temporal logics [7,8], the main common feature of this framework is perhaps the ability to check whether the system can evolve to a certain configuration, i.e. a *reachability* query. In this context, we recall the landmark result on the satisfiability of CTL, shown EXPTIME-complete by Fisher and Ladner [23]. Another possibility to deal with the complexity of MSO is to restrict the second-order quantifications to specific *submodels*. This is the idea behind ambient logic [16], separation logic [37] and more generally bunched logics [35]

c The Author(s) 2020

and graphs logics [1]. These logics provide primitives for reasoning about resource composition, mainly by adding a *spatial conjunction* ∗ which requires to split a model into two disjoint pieces, one satisfying and the other satisfying . Similar ideas are developed in sabotage modal logics, where the formula ⧫ , headed by the *sabotage* modality ⧫, states that must hold in a graph obtained by removing one edge from the current model [4,21]. Within these logics, we highlight the quantifier-free fragment of separation logic restricted to the ∗ operator, denoted here with (∗) and whose satisfiability problem is proved to be PSPACE-complete in [12].

Once a framework provides a solid foundation for reasoning tasks, a natural step is to extend its expressiveness while keeping its complexity in check. Sometimes the additional capabilities do not change the complexity of the logic, as for example (∗) extended with reachability predicates, whose satisfiability problem is still PSPACE-complete [20]. However, it often happens that the new features make the problem jump to higher complexity classes and, sometimes, reach MSO. We pinpoint two instances of this:

Consequently, it is natural to ask ourselves why the additional features made the problem harder. Answering this question requires to study the interplays between the various operators of the logic, searching for a sufficient set of conditions explaining its complexity.

Our motivation. Second-order features often lead to logics with TOWER-hard satisfiability problems, as illustrated above for first-order (∗) and *T*. A good amount of research has been done independently on these logics [5,9,17,28], culminating with the TOWER-hardness of (∗) with two quantified variables [17] and the TOWER-hardness of *T* with just one temporal operator between *exists-finally* and *exists-next* [5] (see Section 4 for the definitions). Connections between these two formalisms have not been explicitly developed so far, perhaps because of the quite different logics: *T* is built on top of propositional calculus and it is interpreted on infinite trees, whereas (∗) does not feature propositional symbols and it is essentially interpreted on finite structures. Nevertheless, we argue that these and other logics are related not only as they are fragments of MSO, but also as they share a form of reachability and an ability of reasoning on submodels which is sufficient to obtain TOWER-hard logics.

Our contribution. We explicit these common features that lead to TOWER-hard logics by relying on an *Auxiliary Logic on Trees* (ALT), introduced in Section 2. ALT reasons about reachability of a fixed *target node* inside a finite forest and features modalities from sabotage logics to reason on submodels. Here, reachability should be understood as the ability to reach the target node in at least one step, starting from a "current" node which can be updated thanks to the existential modality *somewhere* ⟨U⟩ [26]. In Section 3, we take a look at the expressive power of ALT and show that SAT(ALT) is TOWER-hard. In Section 4, we then display how ALT is captured by first-order (∗) and *T*, as well as modal logic of heaps (MLH) and modal separation logics (MSL), two other logics introduced in [17] and [18], respectively. In this context, beside exposing that all these logics are TOWER-hard because of the way they reason about reachability and submodels, we discover interesting sublogics that are still TOWER-complete:

## **2 The definition of an Auxiliary Logic on Trees**

We introduce an Auxiliary Logic on Trees (ALT). Its formulae are from the grammar:

∶= *⊤* ∣ ∧ ∣ ¬ ∣ ∣ ∣ ⟨U⟩ ∣ ⧫ ∣ ⧫∗

As we will soon clarify, the symbol ⟨U⟩ is borrowed from Goranko and Passy paper on modal logic with universal modality [26]. Similarly, readers who are familiar with sabotage modal logics will recognise in ⧫ the sabotage modality [4], and in ⧫∗its Kleene closure (i.e. ⧫ applied an arbitrary number of times). These two operators modify the model during the evaluation of a formula, making ALT a *relation-changing* modal logic (following the terminology used in [3]). However, contrary to most modal logics, ALT does not feature classical propositional symbols. Instead, this logic only features two interpreted atomic propositions and . Roughly speaking, stands for "the target node is reachable" whereas stands for "the target node is not reachable". The formal definitions will be given soon in order to clarify these two sentences.

Let be countably infinite set of *nodes*. A *(finite) forest* ∶→ is a partial function (encoding the standard parent relation) that

Here, denotes ≥ 0 *functional composition(s)* of . Albeit non-standard, our definition of finite forests over an infinite set of nodes simplifies the forthcoming definitions. Besides, in Section 3.2 we show how restricting to a finite set does not change the expressive power nor the complexity of ALT.

We denote the image of as ran() ={′ ∣ () = ′ for some ∈ dom()}. Given a finite set , we denote with || its cardinality. Let *,* ′ be two nodes. As usual, is a *-descendant* of ′ (alternatively, ′ is an *-ancestor* of ) whenever () = ′ for some ≥ 1. In this case, if = 1 then is a *-child* of ′ (alternatively, ′ is the *-parent* of ). We drop the prefix - from these terms when it is clear from the context. Given two forests *,* ′ , we say that ′ is a *subforest* of , written ′ *⊑* , whenever () = ′ () for every ∈ dom(′ ). Figure 1 intuitively represents two forests (every " " represents a node), the one on the left being a subforest of the one on the right.

ALT is interpreted on *pointed forests* (*, ,* ), where is a forest and *,* ∈ are respectively called the *target node* and the *current evaluation node*. The satisfaction relation *⊧* is defined (throughout the paper, we omit standard clauses for *⊤,* ∧*,* ¬) as:

(*, ,* ) *⊧* ⇔ is a -descendant of . (*, ,* ) *⊧* ⇔ ∈ dom() and (*, ,* ) ̸*⊧* . (*, ,* ) *⊧* ⟨U⟩ ⇔ there is ′ ∈ s.t. (*, ,* ′ ) *⊧* . (*, ,* ) *⊧* ⧫ ⇔ there is ′ s.t. ′ *⊑* , |dom(′ )|+1 = |dom()|, (′ *, ,* ) *⊧* . (*, ,* ) *⊧* ⧫∗ ⇔ there is ′ s.t. ′ *⊑* and (′ *, ,* ) *⊧* .

**Fig. 1.** Subforest relation

We denote with ⟂ the contradiction ¬*⊤*. The standard connectives ∨ and ⇒ are defined as usual. The semantics of and is pretty straightforward. As a visual aid, the nodes in Figure 1 satisfying are the ones in the dark grey area, whereas the ones in the light grey area satisfy . As stated before, the semantics given to ⟨U⟩ is the one of the existential modality *somewhere* [26], stating that there is a way to change the current evaluation node so that becomes true. Its dual operator [U] =¬ ⟨U⟩ ¬ is the universal modality *everywhere*. The semantics given to ⧫ is the one of the *sabotage* modality from [4], which requires to find one edge of the forest that, when removed, makes the model satisfy . Lastly, the ⧫∗modality, here called *repeated sabotage* operator, can be seen as the operator obtained by applying ⧫ an arbitrary number of times. Indeed, by inductively defining ⧫ ( ∈ ℕ) as the formula for = 0 and otherwise ( ≥ 1) as ⧫ ⧫−1 , it is easy to see that (*, ,* ) *⊧* ⧫∗ is equivalent to ∃ ∈ ℕ*.* (*, ,* ) *⊧* ⧫ .

Given a pointed forest (*, ,* ), we denote with () the set of its *garbage nodes*: the set of elements in dom() that are not descendants of , i.e. () = { ∈ dom() ∣ ∀ ≥ 1*,* () ≠ }. Then, () is equivalent to { ∈ ∣ (*, ,* ) *⊧* }. We omit the subscript from () when it is clear from the context. We augment the standard precedence rules of propositional logic so that the modalities ⟨U⟩, ⧫ and ⧫∗ have the same precedence as ¬. For instance, the formula ⟨U⟩ ∧ should be read as (⟨U⟩ ) ∧ .

Satisfiability problem. As usual, given a logic and one of its interpretations *⊧* on a class of structures ℭ, the satisfiability problem of , denoted with SAT() when the interpretation is clear from the context, takes as input a formula of and asks whether there is a structure ∈ ℭ such that *⊧* . If the answer is positive, then is *satisfiable*.

Where does ALT come from? A preliminary definition of ALT was introduced in [31] to reason on the complexity of separation logic. As such, in [31] ALT features the separating conjunction ∗ from separation logic, stating that the forest can be partitioned into two disjoint subforests, one satisfying and one satisfying . This binary operator generalises both ⧫ and ⧫∗operators (we show how in Section 4). Hence, the TOWER-hardness of the satisfiability problem for the logic defined here cannot be inherited from [31] and must be proved (Section 3). Unfortunately, the proof does not give any indication on whether or not the two versions of ALT have the same expressive power. What is clear is that the two logics analyse the model in a different way: the ∗ operator is able to reason on the model in a "concurrent" way, whereas ⧫ and ⧫∗do it in a "sequential" one. Let us draw an example of this. Let (*, ,* ) be a pointed forest. We aim at defining a formula # ≥2 stating that the target node has at least two children. First, we define # ≥1 (the formula for just one child) as ⟨U⟩( ∧ ¬ ⧫ ). Intuitively, # ≥ 2

can then be defined with the ∗ operator simply as the formula # ≥1∗# ≥1, stating that it is possible to partition the forest into two subforests having both at least one child of . With the ⧫ operator, this property is instead defined as

$$\#\mathsf{ch}\_{\mathsf{trg}} \ge 2 \overset{\text{def}}{=} \langle \mathsf{U} \rangle \left( \mathbb{T} \land \neg \blacktriangleright \mathsf{G} \land \blacktriangleright (\neg \text{ inDom} \land \#\mathsf{ch}\_{\mathsf{trg}} \ge 1) \right) . \rangle .$$

where =∨ states that the current evaluation node is in the domain of the forest. This definition of # ≥2 requires to find one child of (as encoded by the "⟨U⟩(∧¬ ⧫ ∧···" part of the formula) and remove it from the model (as expressed by the "⧫(¬ ∧· · ·" part). Only afterwards we check for the existence of a second child of . This form of "sequential reasoning" (that can be often avoided when using the ∗ operator), is used in almost all the formulae of the next sections: we first find a node satisfying a certain property, we remove it from the structure, and only afterwards we check if the model satisfy a second property. This principle only works well for monotonic properties: with respect to the definition of # ≥2, the set of children of monotonically decreases when considering subforests. Thus, finding a child of in the subforest, implies finding a child of in the original forest.

## **3 On the complexity and expressive power of** ALT

In this section, we show that SAT(ALT) is TOWER-hard by reduction from the satisfiability problem of Propositional Interval Temporal Logic on finite words (Section 3.3). The proof adapts the arguments used in [31] for the version of ALT featuring the separating conjunction ∗. The reduction is somewhat non-intuitive and in [31] it is given without explaining why more direct ways fail. Here, we clarify this issue which is related to the fact that ALT cannot deduce any property of the portion of a pointed forest (*, ,* ) corresponding to the nodes in (), except for the size of () and the query ∈ (). This is done in Section 3.2, by relying on a notion of Ehrenfeucht-Frassé games for ¨ ALT.

## **3.1 Towards the TOWER-hardness of** SAT(ALT)**: how to encode finite words.**

As a first step, we define a correspondence between finite words and specific pointed forests. As usual, we define the set of finite words on a finite alphabet as the closure under Kleene star ∗. To ease our modelling, we suppose = [1*,* ] to be the alphabet of natural numbers between 1 and . Let = 1··· be a -symbols word in ∗ and = {1*,*···*,* } be a set of nodes. Let ( ∈ [1*,* ]) be a set of + 1 nodes different from 1*,*···*,* and so that for each distinct *,*  ∈ [1*,* ], ∩ = ∅. Lastly, let be a node not in ∪ ⋃ ∈[1*,*] . A pointed forest (*, ,* ) encodes w.r.t. the sets *,*1*,*···*,* iff (**I**) () = , (**II**) for all ∈ [1*,*  − 1] () = +1, (**III**) for all ∈ [1*,* ] and ′∈, (′ ) = and (**IV**) every -descendant of belongs to a set among *,*1*,*···*,*.

We call the path from 1 to , the *main path* of . The nodes of this path are the ones in , and can be characterised as being the only descendants of with at least one child. Moreover, 1 is the only node of the main path having the same number of descendants and children. We say that a node ∈ dom() *encodes* the symbol ∈ if it is a descendant of and it has exactly + 1 children that are not in . Then, the nodes in are the only ones encoding symbols, where encodes for any ∈ [1*,* ]. For instance, Figure 2 shows an encoding of the word 1121.

In order to characterise the class of pointed forests encoding finite words, we adapt the formulae of [31] shown in Table 1 (where their semantics is described). Let (*, ,* ) be a pointed forest and let ∈ ℕ. The formula () ≥ is inductively defined as: () ≥ 0 = *⊤,* () ≥ +1 = ⟨U⟩ ( ∧ ⧫(¬ ∧ () ≥ ) ) *.*

Notice how, in the definition of () ≥ +1, we use the same principle used to encode # ≥2 at the end of Section 2: we first find a node in (), remove it from the model, and then find other elements of (). The formulae # ≥ and # ≥ (again, we refer to Table 1 for their semantics) are instead defined as:

# ≥ = ⧫∗( [U] ¬ *⏟⏟⏟* () is empty. ∧ ∧ ⧫(¬ ∧ () ≥ ) *⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟* Removing lead to a set of garbage nodes of size at least . ) # ≥ 0 = *,* # ≥ +1 = # ≥ +1 ∧ ¬ ⧫ ( ∧¬# ≥ 1) *⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟ .*

Whenever nodes of dom() are removed, if still reaches then it has at least one descendant.

Given ∈ {()*,* #*,* #*,* #}, we write = for ≥ ∧ ¬ ≥ +1. For instance, # = is the formula that checks whether has *exactly* children and it is a descendant of . We can now conclude the encoding of finite words.

Let (*, ,* ) be a pointed forest encoding ∈ ∗ and let be the set of nodes in its main path. Let us recall two properties of our encoding: (I) a node ′ encodes a symbol of iff ′ ∈ , and (II) the node encoding the first symbol of is the only node in with the same number of descendants and children. To reflect (I) we denote with the formula # ≥ 1. For (II), given *⊆* , we introduce the formula that checks if the current evaluation node corresponds to the first node of the main path and encodes a symbol in . It is defined as ⋁ ∈(# = +1∧# = + 1). The following statement formalises the connection between this formula and property (II) stated above.

**Lemma 1.** *Let* ∈ +*. Let* (*, ,* ) *be a pointed forest encoding . Let* 1 *be the first node in the main path of . For every ⊆ ,* (*, ,* ) *⊧* ⟨U⟩ *iff* (*, ,* 1) *⊧ .*

We are finally ready to define the formula , characterising the class of forests that encodes words in ∗. It is proved correct by Lemma 2, and it is defined as follows

The target node has no descendants, or has a descendant that encodes a symbol.

$$\begin{array}{l} \mathsf{word}\_{\Sigma} \stackrel{\mathsf{def}}{=} \overbrace{(\mathsf{U} \mathsf{J} \,\,\mathsf{T} \Rightarrow \langle \mathsf{U} \rangle \,\mathsf{symb})}^{} \wedge \neg \mathsf{#} \mathsf{ch}\_{\mathsf{trg}} \geq 2 \wedge \\ \mathsf{[U]} (\mathsf{symb} \Rightarrow \mathsf{1st}\_{\Sigma} \vee \underbrace{(\neg \mathsf{1st}\_{\{n+1\}} \wedge \mathsf{\Phi} \,\mathsf{1st}\_{\Sigma})}\_{}) .\end{array}$$

The current node encodes a symbol in [1*,* ] and exactly one of its children encodes a symbol.

**Lemma 2.** *A pointed forest* (*, ,* ) *is an encoding of a word in* ∗ *iff* (*, ,* ) *⊧ .*

**game played on** ((1*,* 1*,* 1)*,* (2*,* 2*,* 2)*,* (*,,* ))

**if** there is ∈ {*,* } s.t. not ((1*,* 1*,* 1) *⊧*  iff (2*,* 2*,* 2) *⊧* ) **then** the spoiler wins, **otherwise** the spoiler chooses ∈ {1*,* 2} and plays on (*, ,* ). The duplicator replies on (*, ,* ) where ∈ {1*,* 2}⧵{}. The spoiler **must** choose one of the following moves (else the duplicator wins).

⟨U⟩ **move**: if ≥ 1 then the spoiler **can** choose to play a ⟨U⟩ move. It selects a node ′ ∈ .

	- a finite forest ′ such that ′ *⊑* and |dom(′ )| = |dom()| − 1.
	- **–** The duplicator **must** reply with some ′ *⊑* s.t. |dom(′ )| = |dom()| − 1.
	- **–** The game continues on ((′ 1*,* 1*,* 1)*,* (′ 2*,* 2*,* 2)*,* (*,*−1*,* )).

⧫∗ **move**: if ≥ 1 then the spoiler **can** choose to play a ⧫∗move. It selects a forest ′ *⊑* .

**Fig. 3.** Ehrenfeucht-Fraïssé games for ALT

#### **3.2 Inexpressibility results via the Ehrenfeucht-Fraïssé games for** ALT

Now that we are more familiar with the logic, before completing the TOWER-hardness proof of SAT(ALT) we show some properties that ALT cannot express. Notably, these properties explain why the TOWER-hardness proof of the next section cannot be easily simplified. Moreover, inexpressibility results effectively reduce the set of forests that must be considered in order to solve SAT(ALT). This in turn makes reductions from SAT(ALT) to other logics more immediate, as we show throughout Section 4.

A standard way of proving inexpressibility results for logics interpreted on finite models is by adaptation of the Ehrenfeucht-Fraïssé games [29], as done for other relationchanging logics such as context logic for trees [10] and ambient logic [16].

We define the *rank* of a formula as the triple (*,,* ) ∈ ℕ3 where the *modal rank* is the greatest nesting depth of the modal operator ⟨U⟩ in , whereas the *sabotage rank* (resp. *repeated sabotage rank* ) is the greatest nesting depth of the ⧫ (resp. ⧫∗) operator in . We denote with ALT() the set of formulae with rank ∈ ℕ3.

The Ehrenfeucht-Fraïssé games (EF-games) for ALT are formally defined in Figure 3. A game is played by two players: the *spoiler* and the *duplicator*. A game state ((1*,* 1*,* 1)*,* (2*,* 2*,* 2)*,*) is a triple made of a rank and two pointed forests(1*,* 1*,* 1) and (2*,* 2*,* 2). The goal of the spoiler is to show that the two structures are different. The goal of the duplicator is to counter the spoiler and show that the two structures are similar. Let us make clear what we mean by two models being different: both players can only play following the rules of the logical formalism (in our case, ALT). Then, two models are different if and only if there is a formula ∈ ALT() that it is satisfied by only one of the two models. This correspondence between the game and the logic is expressed by an adequacy result, formalised below in Lemma 3.

A player has a *winning strategy* if it can play in a way that guarantees it the victory, regardless what the other player does. We write (1*,* 1*,* 1) ≈ (2*,* 2*,* 2) whenever the duplicator has a winning strategy for the game ((1*,* 1*,* 1)*,* (2*,* 2*,* 2)*,*). By Martin's Theorem [32] our games are determined: if the duplicator does not have a winning

strategy then spoiler has one, and vice-versa. Hence, (1*,* 1*,* 1) ̸≈ (2*,* 2*,* 2) refers to the fact that the spoiler has a winning strategy.

**Lemma 3.** (1*,* 1*,* 1) ̸≈(2*,* 2*,* 2) *iff* ∃∈ALT()*,* (1*,* 1*,* 1)*⊧ and* (2*,* 2*,* 2)̸*⊧.* The left-to-right direction is proved by induction on the rank and by cases on the first move that the spoiler makes in his winning strategy. The other direction is proved by structural induction on . We start to use the EF-games to derive three easy results.

## **Lemma 4.** *Let be a formula.*

*Proof (sketch).* We sketch the proof of (1) to show how EF-games are used. Let us consider a pointed forest (*, ,* ) such that (*, ,* ) *⊧* . We take a node ′ ∉ dom() ∪ ran() and define the forest ′ (′ ) = **if** (′ ) = **then** ′ **else** (′ ). Notice that ′ ∉ dom(′ ). We then prove ∀ ∈ ℕ3 (*, ,* ) ≈ (′ *,* ′ *,* ) by induction on , leading to (1) directly by Lemma 3. The proof of (3) essentially follows from (2). *⊓⊔*

Interestingly enough, the third statement of Lemma 4 fundamentally implies that enforcing to be finite, instead of infinite as we do throughout this work, does not change the expressive power nor the complexity of ALT.

Let (*, ,* ) be a pointed forest. We now show that ALT has a very limited expressive power with respect to the garbage nodes. In particular, it can only check for the membership of in () (with the formula ) and for the size of () (with the formula ()≥). We formalise this inexpressibility result as follows.

**Lemma 5.** *Let* = (*,,* )*. Let ,* 1 *and* 2 *be three forests and let ,* ∈ *, such that for every* ∈ {1*,* 2}*, ⊑ and* () = dom() ⧵ dom()*. If we have*

 ∈ 1() *iff* ∈ 2() *and* min(|1()|*,* + + ) = min(|2()|*,* + + ) *then* (1*, ,* ) ≈ (2*, ,* )*.*

Let us informally explain Lemma 5, whose proof is by induction on and by cases on the moves of the spoiler. Let (1*, ,* ) be a pointed forest and suppose (ad absurdum) that it satisfies a formula of rank that express a property of the garbage nodes that is different form the ones cited above. For example, let us assume that characterise the set of pointed forests having a garbage node with at least two children. Consider the subforest *⊑* 1 whose domain corresponds to the set of 1-descendants of . In particular, 1() = dom(1) ⧵ dom(). We extend to a forest 2 by (re)defining it on the nodes in 1() so that 2() = 1() and none of these nodes has more than one 2-child (this construction can always be done). This last equality implies that ∈ 1() ⇔ ∈ 2() and min(|1()|*,* + + ) = min(|2()|*,* + + ). By Lemma 5 (1*, ,* ) ≈ (2*, ,* ), which implies (2*, ,* ) *⊧*  by Lemma 3. However, (2*, ,* ) is defined so that every node in 2() has at most one child. Thus, cannot characterise the set of models having a garbage node with at least two children.

As shown in the next section, the inexpressibility result in Lemma 5 plays a central role in the development of the reduction that leads to the TOWER-hardness of SAT(ALT).

## **3.3** PITL **on marked words and the TOWER-hardness of** SAT**(**ALT**)**

We are now ready to show the non-elementarity of SAT(ALT). The proof is by reduction from the satisfiability problem of Propositional Interval Temporal Logic (PITL) under locality principle [34,25], which in turn is shown TOWER-hard by reduction from the nonemptiness problem of star-free regular languages (see [38] for the TOWER characterisation of this problem). PITL is a well-known logic that was introduced by Moszkowski in [34] for the verification of hardware components. It is interpreted on non-empty finite words over a finite alphabet of unary symbols . Its formulae are from the grammar:

$$\varphi \colon= \begin{array}{c} \varphi \land \varphi \mid \ \neg \varphi \mid \ \mathsf{a} \mid \ 1 \mid \ \varphi \mid \varphi \mid \end{array}$$

where ∈ . Under the *locality principle* interpretation, a word = 1··· ∈ + satisfies whenever 1 = . Moreover, satisfies if it is a word of length one (i.e. ∈ ). The main feature of this logic is its *chop* operator " ". Intuitively, is satisfied by words that can be "chopped" into a prefix and a suffix sharing one symbol, so that the prefix satisfies and the suffix satisfies . Formally,

$$\{\mathfrak{a}\_1\cdots\mathfrak{a}\_k \models \varphi\}\!\!/\psi\quad\stackrel{\text{at}}{\Leftrightarrow} \text{ there is } i \in \{1, k\} \text{ such that } \mathfrak{a}\_1\cdots\mathfrak{a}\_i \models \varphi \text{ and } \mathfrak{a}\_i\cdots\mathfrak{a}\_k \models \varphi\dots$$

Translating in ALT is not easy. Indeed, given the encoding of words proposed in Section 3.1, chopping in two pieces means splitting in some way the main path 1*,*···*,* of a forest (*, ,* ) encoding to then check that the word encoded by 1*,*···*,* satisfies and the one encoded by *,*···*,* satisfies . However, by doing this the elements 1*,*···*,* become garbage nodes. Thus, as a consequence of Lemma 5, ALT cannot check in any way what is the word encoded by these nodes. Easy translations from PITL to ALT seem therefore impossible and, as done in [31], we are required to go through an alternative interpretation of PITL based on *marking symbols* instead of chopping words.

A *marking* of an alphabet is a bijection (*.*) ∶ → , relating a symbol ∈ to its *marked variant* ∈ . We denote with ⅀ the extended alphabet *⊎* . A word is *marked* if it has some symbols from . We introduce the satisfaction relation *⊧*∙ on a marked word ∈ ⅀+. It is defined as usual for Boolean connectives.  The definition of is more involved. Let ′ ∈ ∗, ∈ and ′′ ∈ ⅀∗ be such that = ′ ′′, so that is the first marked symbol occurring in (this decomposition is uniquely defined). Then, ′ ′′ *⊧*∙ holds if and only if there is there is ∈ s.t.

On this semantics, the satisfaction of a formula only depends on the prefix 1···−1 of that ends with the first marked symbol. To check whether *⊧*∙ we search for a position ∈ [1*,* ] inside this prefix so that is satisfied by the word obtained from by marking the -th symbol, whereas is satisfied by the suffix of starting in . In the definition above, this idea is split into four cases (a)–(d), depending on truthiness of = 1 and = . This is done as it better reflects the encoding of PITL in ALT. The semantics on marked words is related to the standard semantics of PITL as follows.

**Proposition 1 (from [31]).** *Let* ∈ ∗*,* ∈ *and* ′ ∈ ⅀∗*. Let be a formula in* PITL*. satisfies under the standard interpretation of* PITL *if and only if* ′ *⊧*∙ *.*

The alternative interpretation of PITL allows us to reduce SAT(PITL) to SAT(ALT) in a neat way. Let = [1*,* ], ⅀ = ∪ and let ∶ ⅀ → [1*,* 2] be the bijection () = 2 for ∈ and () = 2 − 1 for ∈ . (1···) denotes the word (1)· · ·(). maps ⅀ into the alphabet [1*,* 2], whose words can be encoded into trees (as in Section 3.1). In these trees each symbol ∈ (resp. ∈ ) corresponds to a node in the main path having 2 + 1 (resp. 2) children not in this path. Therefore, given a node encoding a symbol in , removing exactly one children of that is not in the main path is equivalent to marking the symbol encodes. Based on this description, we can check if the current evaluation node encodes a marked symbol from with the following formula:

$$\mathsf{mark}\_{\Sigma} \overset{\mathsf{def}}{=} \bigvee\_{\mathsf{a} \in \Sigma} \Big( (\mathsf{\#chi1d} = \mathsf{2a} \land \mathsf{1st}\_{[1,2\mathsf{a}]}) \lor (\mathsf{\#chi1d} = \mathsf{2a} + 1 \land \neg \mathsf{1st}\_{[1,2\mathsf{a}]}) \Big)$$

As already stated, *⊧*∙ examines the prefix of that ends with the first marked symbol. In pointed forests (*, ,* ) encoding , this prefix corresponds to the subtree whose root encodes a marked symbol and is a -descendant of every other node encoding marked symbols. Therefore, to characterise this tree we need to track the number of nodes encoding marked symbols. We first define a formula ≥ stating that the forest has at least ∈ ℕ nodes encoding marked symbols. It is defined as *⊤* for = 0, and otherwise ( ≥ 1) as ⟨U⟩ ( ∧ ⧫(¬ ∧ ≥ −1)) . Again, this formula uses the same principle introduced in Section 2 for # ≥2: we search for a node encoding a marked symbol, remove it from the structure and then search for −1 other such nodes. Similarly, we introduce # ≥ = ∧ ⧫(¬ ∧ ≥ ), the formula stating that the current evaluation node encodes a symbol and has at least ancestors that encode marked symbols.

At last, for a formula in PITL having symbols from = [1*,* ], we introduce its translation ∇ () in ALT, where ≥ 1 tracks the number of nodes encoding marked symbols. It is homomorphic for Boolean connectives: ∇ (¬) =¬∇ () and ∇ (∧) =∇ ()∧∇ (). For ∈ and , it faithfully represent the *⊧*∙ relation: ∇ () = ⟨U⟩ [2−1*,*2] and ∇ () = ⟨U⟩([1*,*2] ∧ ). Lastly, the formula ∇ ( ) is defined as

$$\begin{split} & \left( \mathsf{T}(\mathsf{U}) \Big( (\mathsf{1s}\mathsf{T}\_{\{1,2\}} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \wedge \nabla\_{\beta}(\varphi) \wedge \nabla\_{\beta}(\varphi)) \vee \\ & (\mathsf{1s}\mathsf{t}\_{\{1,2\}} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \wedge \mathsf{Φ}(\mathsf{mark}\mathsf{x}\_{\Sigma} \wedge \nabla\_{\beta+1}(\varphi)) \wedge \nabla\_{\beta}(\varphi)) \vee \\ & (\mathsf{-1s}\mathsf{t}\_{\{1,2\}} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \geq \beta - 1 \wedge \nabla\_{\beta}(\varphi) \wedge \mathsf{Φ}(\mathsf{1s}\mathsf{t}\_{\{1,2\}} \wedge \nabla\_{\beta}(\varphi))) \vee \\ & (\mathsf{-1s}\mathsf{t}\_{\{1,2\}} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \wedge \mathsf{mark}\mathsf{x}\_{\Sigma} \geq \beta \wedge \mathsf{obl}(\mathsf{mark}\_{\Sigma} \wedge \nabla\_{\beta+1}(\varphi)) \wedge \mathsf{@}(\mathsf{1s}\mathsf{t}\_{\{1,2\}} \wedge \nabla\_{\beta}(\varphi)))) \rfloor. \end{split}$$

Notice how ∇ ( ) follows closely the *⊧*∙ relation: it is split into four disjuncts, one for each case in the definition of . For example, the second disjunct of ∇ ( ) encodes the case (b) in the definition of ′ ′′ *⊧*∙ , as schematised below:

$$\begin{array}{c|c} \mathsf{P} \mathsf{ITL} & \mathsf{\exists} \mathsf{b} \in \Sigma \dots & \mathsf{\exists} \mathsf{w}\_{2} \in \Sigma^{\*} \text{ s.t. } \mathsf{w}' = \mathsf{b} \mathsf{tw}\_{2} \text{ and } \mathsf{\overline{b}} \mathsf{tw}\_{2} \mathsf{\exists} \mathsf{w}'' \models \varphi & \text{and } \mathsf{b} \mathsf{tw}\_{2} \mathsf{\exists} \mathsf{w}'' \models \varphi\\ \hline \mathsf{A} \mathsf{L} \mathsf{T} & \langle \mathsf{U} \rangle (\mathsf{symb} \dots \mathsf{1} \mathsf{st}\_{\{1,2\mathsf{n}\}} \wedge \neg \mathsf{mark} \mathsf{x}\_{\mathsf{\Sigma}} & \wedge \mathsf{\mathsf{d}} (\mathsf{mark} \mathsf{x}\_{\mathsf{\Sigma}} \wedge \nabla\_{\beta+1} (\varphi)) & \wedge \nabla\_{\beta} (\mathsf{y}) \end{array}$$

The translation is proved correct (by induction on the structure of ) in the next lemma.

**Lemma 6.** *Let* = [1*,* ] *and* ⅀ = ∪ *. Let* ∈ ⅀+ *with* ≥ 1 *marked symbols. Let* (*, ,* ) *be an encoding of* ()*. For every in* PITL*, ⊧*∙ *iff* (*, ,* ) *⊧* ∇ ()*.*

Then, the reduction from SAT(PITL) on standard semantics follows as we are able to characterise the set of pointed forests encoding words in ∗ (first three conjuncts in the formula of Lemma 7). To conclude, we simply apply Lemma 6 and Proposition 1.

**Lemma 7.** *Every in* PITL *written with symbols from* = [1*,* ] *is satisfiable under the standard interpretation of* PITL *if and only if the following formula in* ALT *is satisfiable*

> [1*,*2] ∧ ⟨U⟩ ∧ [U]( ⇔ ∧ ¬ ⧫()) ∧ ∇1()*.*

*⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏞⏟* The forest encodes a non-empty word. The only node encoding a marked symbol is the child of the target node.

Because of the case distinction in the formula ∇ ( ), the formula obtained via ∇ is exponential (hence elementary) in the number of symbols used to write . Therefore, from the TOWER-hardness of SAT(PITL) we conclude that SAT(ALT) is TOWER-hard.

## **4 Revisiting TOWER-hard logics with** ALT

We now display the usefulness of ALT as a tool for proving the TOWER-hardness of logics interpreted on tree-like structures. In particular, we provide semantically faithful reductions from SAT(ALT) to the satisfiability problem of four logics that were independently found to be TOWER-complete: first-order separation logic [9], quantified CTL on trees [28], modal logic of heaps [17] and modal separation logic [18]. Our reduction only use strict fragments of these formalisms, allowing us to draw some new results on these logics. Most notably, this section shows that all these logics are TOWER-hard because they fundamentally provide the reachability and submodel reasoning given by ALT.

## **4.1 From** ALT **to First-Order Separation Logic**

Separation logic () [37] is an assertion logic used in state-of-the-art tools [6,11] for Hoare-style verification of heap-manipulating programs. As already stated, a preliminary definition of ALT was defined in [31] to reason on the complexity of separation logic. Hence, here we briefly revisit the relation between ALT and .

Let and be two countably infinite sets of program variables and locations, respectively. Separation logic is interpreted on *memory states*: pairs (*, ℎ*) consisting of a function (the *store*) ∶→ and a partial function with finite domain (the *heap*) *ℎ*∶→. Since and are both countably infinite sets, w.l.o.g. we assume = . We extend the notation of domain, image and function composition to stores and heaps. Two heaps *ℎ*1 and *ℎ*2 are said to be disjoint, written *ℎ*1*⊥ℎ*2, whenever dom(*ℎ*1) ∩ dom(*ℎ*2)=∅, and when this holds the union *ℎ*1 + *ℎ*2 of *ℎ*1 and *ℎ*2 is defined as the standard sum of functions (*ℎ*1 + *ℎ*2)() = **if** ∈ dom(*ℎ*1) **then** *ℎ*1() **else** *ℎ*2(). Let ∈ be a *fixed variable* that is reserved for quantification (quantification over other variables is not possible). We consider the separation logic (∗*, ,* ↪+), whose formulae are built from the following grammar (as in [31]):

∶= *⊤* ∣ ∧ ∣ ¬ ∣ ∣ = ∣ ↪ ∣ () ∣ ↪+ ∣ ∗ ∣ ∃

where *,* ∈ . As shown below, the *reachability predicate* ↪+ can be seen as the transitive closure of the standard *points-to* predicate ↪ of separation logic. For a memory state (*, ℎ*), the satisfaction relation *⊧* is defined as follows:

(*, ℎ*) *⊧* ⇔ dom(*ℎ*)=∅. (*, ℎ*) *⊧* ↪ ⇔ *ℎ*(()) = (). (*, ℎ*) *⊧* = ⇔ () = (). (*, ℎ*) *⊧* () ⇔ () ∈ dom(*ℎ*). (*, ℎ*) *⊧* ↪+ ⇔ there is ∃ ≥ 1 such that *ℎ*(()) = (). (*, ℎ*) *⊧*  ∗ ⇔ ∃*ℎ*1*, ℎ*2 s.t. *ℎ*1*⊥ℎ*2, *ℎ*1 + *ℎ*2 = *ℎ*, (*, ℎ*1) *⊧*  and (*, ℎ*2) *⊧* . (*, ℎ*) *⊧* ∃ ⇔ there is a location ′ ∈ such that ([←′ ]*, ℎ*) *⊧* ,

where [←′ ] is the store updated from by only changing the evaluation of from () to ′ , i.e. for every ∈ , [←′ ]() = **if** = (syntactically) **then** ′ **else** (). The main ingredient of separation logic is the *separating conjunction* ∗ , that is satisfied whether *ℎ* can be partitioned into *ℎ*1 and *ℎ*2 so that (*, ℎ*1) *⊧*  whereas (*, ℎ*2) *⊧* . The ∗ operator captures the ⧫ and ⧫∗ operators as follows. Consider the formula = 1 =¬∧ ¬(¬ ∗ ¬), which is satisfied whenever |dom(*ℎ*)| = 1. We define ⧫SL = ( = 1) ∗ and ⧫∗ SL = *⊤* ∗ . The semantics of these formulae is related to the analogous operators of ALT as follows:

$$\begin{aligned} &(s,h) \models \blacktriangleright \spadesuit \varphi \iff \exists h\_1, h\_2 \text{ s.t. } h\_1 \bot h\_2, \, h\_1 + h\_2 = h, \, |\text{dom}(h\_1)| = 1 \text{ and } (s, h\_2) \models \varphi. \\ &(s, h) \models \blacktriangleright \spadesuit \varphi \iff \exists h\_1, h\_2 \text{ s.t. } h\_1 \bot h\_2, \, h\_1 + h\_2 = h \text{ and } (s, h\_2) \models \varphi. \end{aligned}$$

In order to perform the reduction from SAT(ALT) to SAT((∗*, ,* ↪+)), we fix a variable ∈ that is syntactically different from and that plays the role of the target node. Then, the translation () of a formula in ALT is straightforward:

() = ↪+ . (⧫ ) = ⧫SL (). (*⊤*) = *⊤*. () = ()∧¬ (). (⧫∗) = ⧫∗ SL (). (¬) = ¬ (). (⟨U⟩ ) = ∃ (). ( ∧ ) = () ∧ ().

Given a pointed forest (*, ,* ) and a store such that () = and () = , by structural induction on we can easily show that (*, ,* ) *⊧*  ⇔ (*,* ) *⊧* (). This, together with the fact that ∀ ¬(↪+ ) characterises the class of acyclic heaps (which correspond to the forests of ALT), directly implies the following result.

## **Lemma 8.** *Let* ∈⧵{}*. in* ALT *and* ()∧∀ ¬( ↪+ ) *are equisatisfiable.*

This lemma reproves that both (∗*, ,* ↪+) and first order separation logic with two quantified variables (denoted as (∗)) admit a TOWER-hard satisfiability problem. (∗), as introduced in [17], can be defined from (∗*, ,* ↪+) by removing and ↪+ from the syntax and allowing a second variable, different from , to be quantified. However, in [17] the authors show that both and ↪+ are expressible in (∗), and with some very minor modification to their formulae we can show that both predicates are definable using ⧫ and ⧫∗instead of ∗ and . Moreover, these logics are in TOWER by Rabin's Theorem [36], leading to the TOWER-completeness of SAT(ALT).

**Theorem 1.** SAT((∗)) *and* SAT((∗*, ,* ↪+)) *are* TOWER*-complete even when and* ∗ *are replaced with* ⧫SL *and* ⧫∗ SL *.* SAT(ALT) *is* TOWER*-complete.*

#### **4.2 From** ALT **to Quantified Computation Tree Logic**

We now consider Computation Tree Logic (CTL), a well-known logic for branching time model checking [14,13]. Among its extensions, in [5,22,28] the addition of propositional quantification is considered. The satisfiability problem of the resulting logic is undecidable on Kripke structures, and TOWER-complete on trees [28]. In [5], the authors show that the problem is TOWER-hard even when considering just one operator among *exists-next* or *exists-finally* (the definitions are below). Here, we reprove the result for by first tackling the TOWER-hardness of the logic with the *exists-until* ( ), and then show that this operator can be defined using . Differently from [5] and thanks to the properties of ALT, our reduction does not imbricate until operators, showing that this extension of CTL remains TOWER-hard even when ( ) is restricted so that and are Boolean combinations of propositional symbols.

Let us first recall the standard definition of Kripke structure [27]. Let = {*, ,*· · ·} be a countable set of *propositional symbols*. A *Kripke structure* is a triple (*, ,* ) where is a countable set of *worlds*, *⊆* × is a left-total *accessibility relation* (left-total means that for each world ∈ there is ′ ∈ s.t. (*,* ′ ) ∈ ) and ∶ → 2 is a *labelling function*. We define () ={′ ∈ ∣ (*,* ′ ) ∈ } as the set of worlds accessible from ∈ . Let *⊆* × be an arbitrary relation on worlds (not necessarily left-total). A *path* starting in is a sequence of worlds (0*,* 1*,*· · ·) such that 0 = and (*,* +1) ∈ for every two successive elements *,* +1 of the sequence. The path is said to be *maximal* whenever it is not a strict prefix of any other path. We denote with Π() the set of *maximal paths* starting in . If is left-total then Π() is the set of all infinite paths starting in . Lastly, ∗() denotes the set of worlds reachable from , i.e. those worlds belonging to a path in Π().

We consider Quantified Computational Tree Logic interpreted under tree semantics (*T*) and refer the reader to [28] for a complete description of the logic. The formulae of *T* are built from the following grammar:

$$\varphi \colon = \top \mid \varphi \land \varphi \mid \neg \varphi \mid p \mid \mathsf{EX} \varphi \mid \mathsf{E}(\varphi \mathsf{U} \varphi) \mid \mathsf{A}(\varphi \mathsf{U} \varphi) \mid \exists p \, \varphi$$

where ∈ . All temporal modalities of *T* are from CTL: is the *exists-next* modality, ( ) is the *exists-until* modality and ( ) is the *all-until* modality.

*T* is interpreted on Kripke trees. Formally, a Kripke structure (*, ,* ) is a *(finitely-branching) Kripke tree* if (I) −1 is functional and acyclic, (II) for every world ∈ , () is finite and (III) it has a *root*, i.e. ∗() = for some ∈ . Given ∈ , the worlds in ∗() ⧵ {} are said to be *descendants* of . As Kripke structures are left-total, Kripke trees can be seen as finitely-branching infinite trees. This leads to SAT(*T*) being in TOWER by reduction to MSO on trees [28]. Let = (*, ,* ) be a Kripke tree and ∈ . The satisfaction relation *⊧* of *T* is defined as:

$$\begin{array}{lll} (\mathcal{K}, \mathbf{w}) \models p & \stackrel{\scriptstyle{\text{def}}}{\Leftrightarrow} \mathbf{w} \in \mathcal{V}(p). \\ (\mathcal{K}, \mathbf{w}) \models \mathsf{EX} \, \uprho & \stackrel{\scriptstyle{\text{def}}}{\Leftrightarrow} \exists \mathbf{w}' \in \mathcal{R}(\mathbf{w}) \, \text{s.t.} (\mathcal{K}, \mathbf{w}') \models \rho. \\ (\mathcal{K}, \mathbf{w}) \models \mathsf{E}(\boldsymbol{\varrho} \cup \boldsymbol{\upmu}) & \stackrel{\scriptstyle{\text{def}}}{\Leftrightarrow} \, \text{there are } (\mathsf{w}\_{0}, \mathbf{w}\_{1}, \cdot) \in \Pi\_{R}(\mathbf{w}) \, \text{and } j \in \mathbb{N} \text{ such that} \\ & (\mathcal{K}, \mathbf{w}\_{j}) \models \boldsymbol{\upmu} \, \text{and for every } i < j, (\mathcal{K}, \mathbf{w}\_{i}) \models \rho. \\ (\mathcal{K}, \mathbf{w}) \models \mathsf{A}(\boldsymbol{\varrho} \cup \boldsymbol{\upmu}) & \stackrel{\scriptstyle{\text{def}}}{\Leftrightarrow} \, \text{for all } (\mathsf{w}\_{0}, \mathbf{w}\_{1}, \cdot) \in \Pi\_{R}(\mathbf{w}), \, \exists j \in \mathbb{N} \text{ such that} \\ & (\mathcal{K}, \mathbf{w}\_{j}) \models \boldsymbol{\upmu} \, \text{and for every } i < j, (\mathcal{K}, \mathbf{w}\_{i}) \models \rho. \\ (\mathcal{K}, \mathbf{w}) \models \exists p \, \boldsymbol{\upmu} \, \text{ } \text{there is } \mathcal{W}' \subseteq \mathcal{W} \, \text{ such that } (\mathcal{W}, \mathcal{R}, \mathcal{V}[p \leftarrow \mathcal{W}']) \models \rho. \end{array}$$

where, similarly to the store update [←′ ] of the previous section, [←′ ] stands for the function obtained from by updating the evaluation of from () to ′ .

The formula ∃ requires to update the satisfaction of in a way such that is satisfied. This should already give a good clue on how to reduce ALT to *T*: we represent the nodes of a forest as the set of worlds satisfying a propositional symbol D . Then, for instance, the repeated sabotage operator ⧫∗is encoded by using an existential ∃E that changes the evaluation of a propositional symbol E so that it only holds in worlds where D holds. In this way, the set of worlds satisfying E represents a subforest of the original one. The universal quantification ∀ and the connectives ⇒ and ∨ are defined as usual. So are the classical temporal operators from [14], *exists-finally* = (*⊤* ), *all-generally* = ¬ ¬, *all-finally* = (*⊤* ), *exists-generally* = ¬ ¬, and *exists-strong-release* ( ) = ( ∧ ).

We now work towards a formal encoding of a pointed forest (*, ,* ) into a *pointed model* (*,* ), where = (*, ,* ) is a Kripke tree and is one of its worlds. We use to play the role of the target node . To encode the forest and the current evaluation node we use the worlds appearing in ∗() and three propositional symbols: D , end and n . The intended use of D is to state which elements of ∗() encode nodes in dom(). We need to be careful here, as ∗() is an infinite set whereas dom() is finite. We use the propositional symbol end to solve this inconsistency: we constraint to satisfy the formula (end ) stating that every maximal path (0*,* 1*,*· · ·) ∈ Π() has a finite prefix (0*,*···*,* −1) ( ∈ ℕ) of worlds not satisfying end , whereas ∈ (end ). Then, a world in encodes an element in dom() whenever it satisfies D and it belongs to one of these prefixes. We use the propositional symbol n to encode the current evaluation node. During the translation we require n to be satisfied by exactly one descendant of , so that the modality ⟨U⟩ roughly becomes a quantification over n . From [28], checking whether a formula holds in exactly one descendant of can be done with the formula () = ()∧∀ ( ( ∧ ) ⇒ ( ⇒ )) where ∈ does not appear in . For technical reasons, we treat in a similar way the world , which encodes the target node, and require it to be the only world (among the ones in ∗()) satisfying the auxiliary propositional symbol t . Lastly, we use an additional propositional symbol E in order to encode subforests and deal with the encoding of ⧫ and ⧫∗(as stated above).

We now formalise the encoding. For the remaining of this section, we fix a tuple = (end *,* n *,* t ) of three different propositional symbols. Let D be an additional symbol not in , and let (*, ,* ) be a pointed forest s.t. ∉ dom() (by Lemma 4(1) it is sufficient to consider this class of structures in order to decide satisfiability of a formula in ALT). A pointed model ( = (*, ,* )*,* ), is an (*,* D )*-encoding* of (*, ,* ), or simply *encoding* when (*,* D ) is clear from the context, if there is an injection ∶→∗() s.t.

	- **–** ∀ ∈ [0*,*  − 1], ∉ (end ) and ( ∈ (D ) ⇔ ∃′ ∈ dom() (′ ) = );
	- **–** for every ≥ and every node ′ ∈ dom(), (′ ) ≠ .

It is easy to show that such an encoding always exists. Informally, the first property states that encodes and is the only world in ∗() satisfying t . Similarly, the world () encoding is the only world in ∗() that satisfies n . The second property states that the forest must be correctly encoded in the Kripke structure. In particular, notice that the parent relation of the finite forest is inverted so that it becomes the child relation in the

**Fig. 4.** A pointed forest (left) and one of its encoding as a finitely-branching Kripke tree (right).

Kripke structure (as shown in Figure 4). As is an injection, the encoding does not merge together trees that are disconnected in the forest. Lastly, the third property of states that the elements in dom() must be encoded by nodes in ∗() that precede every world satisfying end . Moreover, among all the descendants of preceding end , the worlds encoding dom() are the only ones satisfying D . This implies that does not satisfy D (as ∉ dom()). Figure 4 shows a pointed forest and one of its possible encodings.

We now formalise the translation. Fix two different symbols D *,* E not in . In order to alternate between D and E , we define D = E and E = D . The translation u() of a formula in ALT, implicitly parametrised by and where u ∈ {D *,* E }, is homomorphic for *⊤* and Boolean connectives (as in , see Section 4.1), and otherwise it is defined as

$$\begin{array}{ll} \tau\_{\mathsf{u}}(\mathsf{T}) & \stackrel{\scriptstyle \mathsf{id}}{=} \mathsf{E}((\mathsf{u}\vee t\,)\wedge\neg end)\,\mathsf{M}\,(\mathsf{u}\wedge n\,)). & \tau\_{\mathsf{u}}(\mathsf{U}\,\mathsf{U}\,\varphi) \stackrel{\scriptstyle \mathsf{id}}{=} \exists\mathsf{n}\,\,(\mathsf{un}\,\mathsf{iq}(n)\wedge\tau\_{\mathsf{u}}(\mathsf{op})).\\ \tau\_{\mathsf{u}}(\mathsf{G}) & \stackrel{\scriptstyle \mathsf{id}}{=} \mathsf{E}(\negend\,\,\mathsf{M}\,(\mathsf{u}\wedge n\,))\wedge\neg\tau\_{\mathsf{u}}(\mathsf{T}). & \tau\_{\mathsf{u}}(\mathsf{\mathsf{A}}^{\&}\,\varphi) \stackrel{\scriptstyle \mathsf{id}}{=} \exists\mathsf{\overline{u}}\,(\mathsf{AG}\,(\overline{\mathsf{u}}\Rightarrow\mathsf{u})\wedge\tau\_{\mathsf{u}}(\mathsf{op})).\\ \tau\_{\mathsf{u}}(\mathsf{\mathsf{A}}\,\varphi) \stackrel{\scriptstyle \mathsf{id}}{=} \exists\mathsf{\overline{u}}\,(\mathsf{AG}\,(\overline{\mathsf{u}}\Rightarrow\mathsf{u})\wedge\operatorname{un\mathsf{im}}\,\mathsf{q}(\mathsf{u}\wedge\neg\overline{\mathsf{u}})\wedge\operatorname{\mathsf{E}}(\negend\,\,\mathsf{M}\,(\mathsf{u}\wedge\neg\overline{\mathsf{u}}))\wedge\tau\_{\mathsf{u}}(\mathsf{op}). \end{array}$$

Let (*, ,* ) be a pointed forest s.t. ∉ dom() and let ((*, ,* )*,* ) be one of its (*,* u)-encodings w.r.t. the injection . For instance, u() requires that there is a path (*,* 1*,*···*,* ) starting in () = and whose worlds do not satisfy end and must satisfy u or t . Moreover, the last world must satisfy u and n . From property (1) of the definition of , the only element satisfying t is , which does not satisfy u (as ∉ dom()). Then, this path of worlds encodes a path in the pointed forest, from the current evaluation node (which is encoded by the only world satisfying n ) to the target node . The translation is shown correct (by structural induction on ) for pointed forests that admit an encoding.

**Lemma 9.** *Let* (*, ,* ) *be a pointed forest s.t.* ∉ dom()*, and let* (*,* ) *be a* (*,* u) *encoding of* (*, ,* )*. Given a formula in* ALT*,* (*, ,* ) *⊧ if and only if* (*,* ) *⊧* u()*.*

Then, to conclude the reduction we just need to characterise the set of models encoding a pointed forest. The formula =¬D ∧t ∧ (t ) ∧ (n ) ∧(end ) does the job.

**Lemma 10.** *in* ALT *and* ∧ D() *in T are equisatisfiable.*

We now take a closer look to the translation. Given a temporal modality and ∈ ℕ∪{}, *T*( ) denotes the fragment of *T* restricted to formulae where the only temporal modality allowed is , which can be nested at most times ( stands for an arbitrary number of imbrications). For instance, *T*( ) denotes the set of formulae restricted to the operator , which can be nested at most times. This fragment of *T* is shown to be -NEXPTIME-hard in [5], which directly leads to the TOWER-hardness of *T*( ) and *T*(). By analysing our translation it is easy to show that *T*(0), i.e. *T* restricted to the only modality ( ) where and are Boolean combination of propositional symbols, and *T*(1) are already TOWERhard. First of all, the formula ( ) in *T*(0) is equivalent to the following formula in *T*(1): ∃ ( (¬∧¬ ⇒ )∧( ⇒ )∧ ( ∧¬) ) , where does not appear in or . Then, we just need to prove the result for *T*(0).

Clearly, the translation u is defined so that the resulting formula is in *T*(0). However, we need to deal with the occurrence of (end ) used inside the formula . Let us first consider the formula ( ⇒ ) which is satisfied by models where once is found to hold in a certain world , then is satisfied in every world of ∗(). Despite not being in *T*(0), the formula ( ⇒ ) is equivalent to the following formula: ∀∀ ( () ∧() ∧ (∧) ∧ ( ∧ ¬) ⇒ (¬ ) ) , where and do not appear in or . We then define a formula () that only uses modalities and is equivalent to , so that then ¬ (¬) is equivalent to :

$$\begin{aligned} \chi\_{\mathsf{EG}}(\mathsf{q}) \stackrel{\text{def}}{=} & \exists p \Big( \neg p \land \mathsf{AG} \,(\neg q \Rightarrow p) \land \mathsf{AG} \,(p \Rightarrow \mathsf{AG} \, p) \land \\ & \forall q \Big( \text{uni} \, \mathsf{q}(q) \land \mathsf{EF} \,(q \land \neg p) \Rightarrow \mathsf{EF} \,(q \land \mathsf{EF} \,(\neg q \land \neg p)) \Big) \Big) \Big) \end{aligned}$$

where does not appear in . This formula is expressible in *T*(0), as every subformula that is not in this fragment is an instance of ( ⇒ ). Then, we conclude that (end ) is expressible in *T*(0), leading to the following result.

**Theorem 2.** *The satisfiability problems of T*(0) *and T*(1) *are* TOWER*-c.*

## **4.3 From** ALT **to Modal Logic of Heaps and Modal Separation Logic**

In [17] and later in [18] two families of logics are presented, respectively called *modal logic of heaps* (MLH) and *modal separation logic* (MSL). At their core, both logics can be seen as modal logics extended with separating connectives, hence mixing separation logic (Section 4.1) with temporal aspects as in quantified CTL (Section 4.2). As we already shown how ALT is captured by these two latter logics, it is natural to ask ourselves if the same holds for MLH and MSL. In this section, we show that this is indeed the case and, as for the previous two sections, ALT allows us to refine the analysis on these logics. Both MLH and MSL are interpreted on finite Kripke functions. A *finite Kripke function* is a Kripke structure (*, ,* ) (see Section 4.2 for its definition) where is infinite and , instead of being left-total, is finite and weakly functional, i.e. || ∈ ℕ and for every *,* ′ *,* ′′ ∈ , if (*,* ′ ) ∈ and (*,* ′′) ∈ then ′ = ′′. As and are both countably infinite sets, without loss of generality we assume = . Two Kripke structures 1 = (*,* 1*,* ) and 2 = (*,* 2*,* ) are disjoint if 1 ∩ 2 = ∅. When this holds, 1 + 2 denotes the model (*,* 1 ∪ 2*,* ). To shorten the presentation, in the following diagram we introduce a language having the operators from MSL and MLH, and summarise known and new results on these logics (where ∈ ):

 ∶= ∣ ⟨≠⟩ ∣ *⊤* ∣ ∧ ∣ ¬ ∣ ◊ ∣ ∗ ∣ ⟨U⟩ ∣ ◊−1 MSL: TOWER-complete from [18]. MLH: TOWER-complete from [17].

As defined below, ◊ is the standard alethic modality from modal logic, ◊−1 is its converse modality, and ⟨≠⟩ is the *elsewhere* modality that generalises the somewhere modality ⟨U⟩ as ⟨U⟩ = ∨ ⟨≠⟩ . For a *pointed model* (*,* ), where = (*, ,* ) is a finite Kripke function and ∈ , the satisfaction relation *⊧* is defined as follows:

By looking at the diagram above, compared to the work in [18], ALT allows us to show that propositional symbols and the elsewhere modality can be removed from MSL without changing the complexity status of its satisfiability problem. Similarly, ALT allows us to refine the analysis on the complexity of SAT(MLH) by showing that the ◊−1 modality is not needed in order to achieve non-elementary complexities.

Let (*, ,* ) be a pointed forest and let (*,* ) be a pointed model where = (*, ,* ). For the reduction, we use to encode the current node . Encoding is not so immediate, as MLH does not have propositional symbols. A possible solution is to encode it as a self-loop, so that the formula is translated to a query stating that reaches the self-loop. As done in Section 4.1 we define the formula =1 = ⟨U⟩ ◊*⊤* ∧ ¬(⟨U⟩ ◊*⊤* ∗ ⟨U⟩ ◊*⊤*), that is satisfied whenever ||=1. We also define the modalities ⧫ and ⧫∗in MLH: ⧫ML = (=1) ∗ and ⧫∗ ML =*⊤* ∗ . Lastly, we introduce the formula = ⧫∗ ML(◊◊*⊤* ∧ ¬⧫ML⧫ML*⊤*) that is satisfied by (*,* ) if (*,* ) ∈ . Suppose for a moment that we are able to use this formula to characterise the class of of every finite Kripke function (*, ,* ) where there is exactly one cycle, and this cycle is a self-loop on a world . Then, we use to encode the target node of a finite forest (*, ,* ) while being careful that the ⧫ and ⧫∗ operators of ALT are translated in such a way that the self-loop on is preserved. Because of the specific treatment of , it is convenient to assume that the current evaluation node is encoded by a world different from , which reflects on the translation of ⟨U⟩. The admissibility of this assumption follows by Lemma 4.

We encode pointed forests as finite Kripke functions. Let (*, ,* ) be a pointed forest s.t. ∉ dom() and ≠ . A finite Kripke function ((*, ,* )*,* ) (recall, = ) is an *encoding* of (*, ,* ) iff for every ′ *,* ′′ ∈ we have (′ *,* ′′) ∈ ⇔ ((′ ) = ′′ or ′ = ′′ = ). Notice how is essentially defined from by adding the self-loop (*,* ). The translation () in MLH of a formula in ALT is homomorphic for *⊤* and Boolean connectives (as is the case for in Section 4.1), and otherwise it is defined as

$$\begin{array}{lll}\tau(\mathsf{T}) & \stackrel{\scriptstyle\mathsf{id}^{\mathsf{e}}}{\stackrel{\scriptstyle\mathsf{e}}{\longrightarrow}}\mathsf{\mathsf{Q}}\_{\mathsf{m}}^{\mathsf{e}}(\bigotimes\mathsf{T}\wedge[\mathsf{U}](\bigotimes\mathsf{T}\Rightarrow\mathsf{Q}\bigotimes\mathsf{T})). & \tau(\mathsf{\mathsf{A}}\,\varphi)\stackrel{\scriptstyle\mathsf{d}\mathsf{e}}{\stackrel{\scriptstyle\mathsf{e}}{\longrightarrow}}\mathsf{\mathsf{Q}}\_{\mathsf{m}}(\tau(\mathsf{q})\wedge\langle\mathsf{U}\rangle\,\mathsf{self}\,\mathsf{I}\mathsf{Loop}).\\\tau(\mathsf{G}) & \stackrel{\scriptstyle\mathsf{d}\mathsf{e}}{\stackrel{\scriptstyle\mathsf{e}}{\longrightarrow}}\mathsf{\mathsf{Q}}\top\wedge\neg\tau(\mathsf{T}). & \tau(\mathsf{\mathsf{A}}^{\mathsf{e}}\,\varphi)\stackrel{\scriptstyle\mathsf{d}\mathsf{e}}{\stackrel{\scriptstyle\mathsf{e}}{\longrightarrow}}\mathsf{\mathsf{Q}}\_{\mathsf{m}}^{\mathsf{e}}(\tau(\mathsf{q})\wedge\langle\mathsf{U}\rangle\,\mathsf{self}\,\mathsf{I}\mathsf{Loop}).\\\tau(\mathsf{(U}\,\bigotimes)\stackrel{\scriptstyle\mathsf{d}\mathsf{e}}{\stackrel{\scriptstyle\mathsf{e}}{\longrightarrow}}\langle\mathsf{U}\rangle(\bigcirc\mathsf{s}\,\texttt{e}\,\mathsf{L}\mathsf{f}\,\mathsf{L}\mathrm{cop}\wedge\tau(\mathsf{q})). \end{array}$$

We highlight two points of this translation. First, () essentially asks to find a submodel where every path reaches the self-loop and the current evaluation node is in one of these paths. Second, notice how the translation of ⧫ and ⧫∗checks that the model is updated so that the self-loop is not lost, as required by our encoding. It should be noted that this requirement cannot be met if we were translating the definition of ALT from [31], featuring the ∗ operator. Indeed, by partitioning the model into two pieces, this operator removes the self-loop from one of the two parts, breaking our encoding. The following lemma (proved by structural induction on ) shows the correctness of our translation.

**Lemma 11.** *Let* (*, ,* ) *be a pointed model s.t.* ≠ *and* ∉ dom()*. Let* (*,* ) *be an encoding of* (*, ,* )*. Given a formula in* ALT*,* (*, ,* ) *⊧ iff* (*,* ) *⊧* ()*.*

To conclude the reduction we show that we can characterise the class of models encoding pointed forests, i.e. the finite Kripke functions with exactly one cycle, which is a self-loop. We first define the formula = ⧫∗ ML ( ⟨U⟩ ◊*⊤* ∧ [U](◊*⊤* ⇒ ◊◊*⊤*) ) that checks if a finite Kripke function has at least one cycle. Then, the desired property can be simply defined by stating that there is a self-loop which, whenever removed, leads to an acyclic submodel: = ⟨U⟩ ( ∧ ¬ ⧫ML(□⟂ ∧ ) ) .

**Lemma 12.** *Every formula in* ALT *is equisatisfiable with* () ∧ *.*

For the proof of Lemma 12, both Lemma 4(1) and (2) are used in order to restrict ourselves to pointed forest (*, ,* ) s.t. ≠ and ∉ dom(). Then, we apply Lemma 11.

**Theorem 3.** *The fragment of* MLH *and* MSL *with Boolean operators,* ◊ *and* ⟨U⟩ *modalities, and* ∗ *(alternatively,* ⧫ML *and* ⧫∗ ML *) has a* TOWER*-complete satisfiability problem.*

## **5 Conclusions**

We studied an *Auxiliary Logic on Trees* (ALT), a quite simple formalism that admits a TOWER-complete satisfiability problem. ALT is shown to be easily captured by various non-elementary logics: first-order separation logic, quantified CTL, modal logic of heaps and modal separation logic. Through ALT, we were not only able to connect these logics, but also to refine their analysis and find strict fragments that are still TOWER-hard. Most importantly, with ALT we hope to have shown a set of simple and concrete properties, centred around reachability and submodel reasoning, that when put together lead to logics having a non-elementary satisfiability problem.

This work leaves a few questions open. First, the fragments of ALT where ⧫ or ⧫∗are removed from the logic have not being studied yet. The logic without ⧫∗is of particular interests, as it is connected with the sabotage logics from [4]. Second, the analysis done on first-order separation logic and on modal logic of heaps (Sections 4.1 and 4.3) reveals that the complexity of these logics does not change when the ∗ operator and the predicate are replaced with the less general operators ⧫ and ⧫∗. We find this point interesting, as from an overview of the literature, it seems that this result also holds for the separation logics considered in [9,17,19,30,31]. Moreover, for the logics whose expressiveness is known, i.e. the ones in [19,30], it seems that also the expressive power remains unchanged. However, we struggle to see how to uniformly express the operator ∗ with ⧫ and ⧫∗, as the resulting logics reason on the model in a different way (as as shown in Section 2). Lastly, this work illustrates the potential of ALT as a tool for proving the TOWER-hardness of logics interpreted on tree-like structures. As the operators of our logic are simple, we hope ALT to be useful to study logics with unknown complexities.

**Acknowlegements.** I would like to thank S. Demri and E. Lozes for their feedback.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction**

Thomas Neele1() , Antti Valmari2, and Tim A.C. Willemse1

1 Eindhoven University of Technology, Eindhoven, The Netherlands {t.s.neele<EMAIL_ADDRESS>2 University of Jyv¨askyl¨a, Jyv¨askyl¨a, Finland

<EMAIL_ADDRESS>
**Abstract.** In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.

## **1 Introduction**

In formal methods, model checking is a technique to automatically decide the correctness of a system's design. The many interleavings of concurrent processes can cause the state space to grow exponentially with the number of components, known as the *state-space explosion* problem. *Partial-order reduction* (POR) is one technique that can alleviate this problem. Several variants of POR exist, such as *ample sets* [11], *persistent set* [7] and *stubborn sets* [16,21]. For each of those variants, sufficient conditions for preservation of stutter-trace equivalence have been identified. Since LTL without the next operator (LTL−X) is invariant under finite stuttering, this allows one to check most LTL properties under POR.