Damien Doligez

Jael Kriener

Leslie Lamport

Tomer Libal

Stephan Merz

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics *

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

Introduction

Verification of distributed and concurrent systems requires reasoning about temporal behaviors. A common approach is to express the properties to be proved in a modal logic having one or more temporal modalities. For verifying real-world systems, a proof language must also include equality, quantification, interpreted theories, and local definitions. It must therefore encompass FOML (F irst O rder M odal Logic) and support operator definitions. One such language is TLA + [START_REF] Lamport | Specifying Systems, The TLA + Language and Tools for Hardware and Software Engineers[END_REF], based on the logic TLA that has two temporal modalities: the usual 2 (always) operator of linear-time temporal logic and ′ (prime), a restricted next-state operator such that e ′ is the value of e at the next state if e is an expression that does not contain a modal operator.

A common way to prove an FOML sequent Γ |= ϕ (ϕ holds in context Γ) is to translate it to a semantically equivalent FOL sequent Γ * |= FOL ϕ * and to prove this FOL sequent. For some FOMLs, this method is semantically complete-that is, Γ |= ϕ is valid iff Γ * |= FOL ϕ * is [START_REF] Jürgen | Semantics-based translation methods for modal logics[END_REF]. This approach has been followed for embedding FOML in SPASS [START_REF] Hustadt | MSPASS: Modal reasoning by translation and first-order resolution[END_REF], Saturate [START_REF] Ganzinger | The Saturate system[END_REF], and other theorem provers.

Such a semantic translation may be appropriate for completely automatic provers. However, we are very far from being able to automatically prove a formula that expresses a correctness property of a non-trivial system. A person must break the proof into smaller steps that we call proof obligations, usually by interacting with the prover. Requiring the user to interactively prove the semantic translation of the FOML formula destroys the whole purpose of using modal logic, which is to allow her to think in terms of the simpler FOML abstraction of the theorem. The user should therefore decompose the FOML proof into FOML proof obligations.

In this paper we describe a method called coalescing that handles many FOML proof obligations by soundly abstracting them into formulas of either FOL or propositional modal logic (ML). The resulting formulas are dealt with by existing theorem provers for these logics. Although the basic idea of coalescing is simple, some care has to be taken in the presence of equality and bound variables. The translation becomes trickier in the presence of defined operators.

Outline of this Paper. Section 2 motivates our proposal by its application within the TLA + Proof System TLAPS. Section 3 formally introduces FOML and its two fragments, FOL and ML. Sections 4 and 5 present coalescing for modal and first-order expressions respectively, proving their soundness. Section 6 extends the results to languages containing local definitions. In Section 7 we outline a proof of the completeness of coalescing for proving safety properties. Section 8 discusses semantic translation vs. coalescing and suggests some optimizations and future work.

Motivation 2.1 A Sample TLA + Proof

Our motivation comes from designing the TLAPS proof system [START_REF] Cousineau | TLA + proofs[END_REF] for TLA + , which can check correctness proofs of complex, real-world algorithms [START_REF] Lamport | Byzantizing Paxos by refinement[END_REF]. The essence of TLA proofs is to decompose proofs of temporal logic formulas so that most of the obligations contain no modal operator except prime. Figure 1 contains the outline of the proof of a simple safety property in TLAPS that illustrates this decomposition. The system specification is formula Spec, defined to equal Init ∧ 2 [Step] v . In this formula, Init is a state predicate that describes the possible initial states, and Step is an action predicate that describes possible state transitions. Syntactically: Init is a FOL formula containing state (a.k.a. flexible) variables;

Step is a formula containing state variables, FOL operators, and the prime operator; and v is a tuple of all state variables in the specification. The formula [Step] v is a shorthand for Step ∨ (v ′ = v ), and 2 is the usual "always" operator of temporal logic. The temporal logic formula Spec is evaluated over ω-sequences of states; it is true of a sequence s 0 s 1 . . . iff Init is true at state s 0 and, for all pairs of states s i and s i+1 , either Step is true or the value of v does not change. The definitions of the formulas Init and Step, and the reason for writing 2 [Step] v instead of 2Step, are irrelevant in the context of this paper. We wish to prove that a state formula Safe(p) is true throughout any behavior described by Spec, for every process p ∈ Proc.

The right-hand side of Figure 1 shows the assertion and proof of the theorem. The first step in the proof is purely first-order: it introduces a fresh constant p, assumes p ∈ Proc, and reduces the overall proof to showing the implication Spec ⇒ 2Safe(p).

Step 1 1 asserts that the initial condition implies Safe(p). This formula does not contain any modal operators. Step 1 2 shows that Safe(p) is preserved by every transition (as specified by [Step] v ). The proof of this step is essentially first-order, although TLAPS must handle the prime modality. The basic idea is to distribute primes inward in expressions using rules such as (x + y) and then to replace the remaining primed expressions by new atoms. For this example, we are assuming that the specification is so simple that, after the definitions of Init , Next , v , and Safe have been expanded, the FOL proof obligations generated for these two steps can be discharged by a theorem prover.

′ = x ′ + y ′ , Init ∆ = . . . Step ∆ = . . . v ∆ = . . . Spec ∆ = Init ∧ 2[Step] v Safe(p) ∆ = . . . theorem Spec ⇒ ∀ p ∈ Proc : 2Safe(p) 1 . suffices assume new p ∈ Proc prove Spec ⇒ 2Safe(p) obvious 1 1. Init ⇒ Safe(p) by def Init , Safe 1 2. Safe(p) ∧ [Step] v ⇒ Safe(p) ′ by def Safe, Step, v 1 3. qed by 1 1, 1 2, PTL def Spec
Step 1 3 concludes the proof. It is justified by propositional temporal reasoning, in particular the principle

P ∧ A ⇒ P ′ P ∧ 2A ⇒ 2P
The PTL in the step's proof tells TLAPS to invoke a PTL decision procedure, which it does after replacing Spec by its definition and the formulas Init , Safe(p) and [Next ] v by fresh atoms. This effectively hides all operators other than those of propositional logic, 2, and prime.

We call coalescing the process of replacing expressions by atoms. It is similar to the introduction of names for subformulas that theorem provers apply during pre-processing steps such as CNF transformation. However, it has a different purpose: the fresh names hide complex formulas that are meaningless to a proof backend for a fragment of the original logic. As explained in the example above, TLAPS uses coalescing in its translations to invoke FOL and PTL backend provers, where the first do not support the modal operators 2 and prime, and the second do not support first-order constructs such as quantification, equality or terms. An idea similar to coalescing underlies the KSAT decision procedure [START_REF] Giunchiglia | Building decision procedures for modal logics from propositional decision procedures: The case study of modal k(m)[END_REF] for propositional multi-modal logic in that modal top-level literals are abstracted by fresh atoms. Unlike KSAT, we consider first-order modal logic, and we do not recursively construct formulas that must be analyzed at deeper modal levels.

Coalescing cannot in itself be semantically complete because it cannot support proof steps that rely on the interplay of the sublogics. For example, separate FOL and PTL provers cannot prove rules that distribute quantifiers over temporal modalities. Similarly, proofs of liveness properties via well-founded orderings essentially mix quantification and temporal logic. However, we need very few such proof steps in actual proofs, and we can handle them using a more traditional backend that relies on a FOL translation of temporal modalities. Coalescing is complete for a class of temporal logic properties that includes safety properties, which can be established by propositional temporal logic from action-level hypotheses. For these applications, we have found coalescing to be more flexible and more powerful in practice than a more traditional FOL translation. In particular, proofs need not follow the simple schema of the proof shown in Figure 1 but can invoke auxiliary invariants or lemmas. The inductive reasoning underlying much of temporal logic is embedded in PTL decision procedures but would be difficult to automate in a FOL prover. On the other hand, the prime modality by itself is simple enough that it can be handled by a pre-processing step applied before passing the proof obligation to a FOL prover.

Coalescing In First-Order Modal Logic

We believe that coalescing will be useful for proofs in modal logics other than TLA + . We therefore present its fundamental principles here using a simpler FOML containing a single modal operator 2. Corresponding to the translations we have implemented in TLAPS, we give two translations of FOML obligations, one into FOL and the other into ML, and we prove their soundness.

The idea underlying coalescing is very simple: abstract away a class of operators by introducing a fresh atom in place of a subformula whose principal operator is in that class. However, doing this in a sound way in the presence of equality is not trivial because of the Leibniz prin-ciple, which asserts (d = e) ⇒ (P (d ) = P (e)) for any expressions d and e and operator P . The Leibniz principle is valid in FOL but not FOML, which makes translating from FOML obligations to FOL obligations tricky [START_REF] Fitting | First-Order Modal Logic[END_REF].

For example, the formula (v = 0) ⇒ 2(v = 0) is not valid in TLA + or more generally in FOML when v is flexible. A naive application of standard FOL provers could propagate the equality in the antecedent by substituting 0 for v throughout this formula, effectively applying the instance ((v = 0) = true) ⇒ (2(v = 0) = 2true) of the Leibniz principle, and consequently prove the formula using the axiom 2true. Such an approach is clearly unsound. The standard translation of FOML into predicate logic [START_REF] Jürgen | Semantics-based translation methods for modal logics[END_REF] avoids this problem by making explicit the states at which formulas are evaluated, but at the price of adding significant complexity to the formula. Moreover, one typically assumes specific properties about the accessibility relation(s) underlying modal logics. Incorporating these into first-order reasoning may not be easy. For example, the 2 modality of TLA + corresponds to the transitive closure of the prime modality, and this is not first-order axiomatizable. Of course, whether this is an issue or not depends on the particular modal logic one is interested in: semantic translation works very well in applications such as [START_REF] Benzmüller | Gödel's God on the computer[END_REF] that are based on a modal logic whose frame conditions are first-order axiomatizable.

Our approach is to coalesce expressions and formulas that are outside the scope of a given theorem prover. For the example above, coalescing to FOL yields (v = 0) ⇒ 2(v = 0) where 2(v = 0) is a new 0-ary predicate symbol, and this formula is clearly not provable. Similarly, coalescing to ML yields v = 0 ⇒ 2 v = 0 of propositional modal logic, and again, this formula is not provable. We give a detailed description of how to derive a new symbol exp for an arbitrary expression exp. Care has to be taken when the coalesced expression contains bound variables. For example, a naive coalescing into FOL of the formula ∀ a : 2(a = 1) ⇒ a = 1, which is valid over reflexive frames, would yield ∀ a : 2(a = 1) ⇒ a = 1, from which we can deduce 2(a = 1) ⇒ 0 = 1 and then ∀ a : ¬2(a = 1), which is clearly not valid. A correct coalescing yields ∀ a : 2(a = 1) (a) ⇒ a = 1.

Operator Definitions. Coalescing is trickier for a language with operator definitions like P (x , y) ∆ = exp , where exp does not contain free variables other than x and y. Definitions are necessary for structuring specifications and for managing the complexity of proofs through lemmas about the defined operators. We therefore do not want to systematically expand all defined operators in order to obtain formulas of basic FOML. The Leibniz principle may not hold for an expression P (a, b) if the operator P is defined in terms of modal operators-that is, (a = c) ∧ (b = d ) need not imply P (a, b) = P (c, d ). It would therefore be unsound to encode P as an uninterpreted predicate symbol in first-order logic. We show how soundness is preserved by replacing an expression P (a, b) with P , ǫ 1 , ǫ 2 (a, b), for some suitable expressions ǫ 1 and ǫ 2 (described in Section 6.3 below), where P , ǫ 1 , ǫ 2 can be defined so it satisfies the Leibniz principle and also satisfies P , ǫ 1 , ǫ 2 (a, b) = P (a, b) in suitably extended models of FOML, ensuring equisatisfiability of the original and the coalesced formula. Since it satisfies the Leibniz principle, P , ǫ 1 , ǫ 2 can be taken to be an uninterpreted predicate symbol by a first-order theorem prover. Our construction extends to the case of definitions of second-order operators, which are allowed in TLA + .

3 First-Order Modal Logic 3.1 Syntax.

We introduce a language of first-order modal logic whose modal operator we denote by ∇ in order to avoid confusion with the 2 of TLA + . The language omits the customary distinction between function and predicate symbols, and hence between terms and formulas. This simplifies notation and allows our results to apply to TLA + as well as to a conventional language that does distinguish terms and formulas-the conventional language just having a smaller set of legal formulas.

We assume a first-order signature consisting of non-empty distinct denumerable sets X of rigid variables, V of flexible variables, and O of operator symbols. Operator symbols have arities in N and generalize both function and predicate symbols. Expressions e of FOML are then inductively defined by the following grammar:

e ::= x | v | op(e, . . . , e) | e = e | false | e ⇒ e | ∀ x : e | ∇e
where x ∈ X , v ∈ V, op ∈ O, and arities are respected (empty parentheses are omitted for 0-ary symbols). We do not allow quantification over flexible variables, so our flexible variables are really "flexible function symbols of arity 0". While TLA + allows quantification over flexible variables, it can be considered as another modal operator for the purposes of coalescing.

The notions of free and bound (rigid) variables are the usual ones. We say that an expression is rigid iff it contains neither flexible variables nor subexpressions of the form ∇e. The standard propositional (true, ¬, ∧, ∨, ≡) and first-order (∃) connectives are defined in the usual way. The dual modality ∆ is introduced by defining ∆e as ¬∇¬e. The extension to a multi-modal language is straightforward.

Semantics.

A Kripke model M for FOML is a 6-tuple (I, ξ, W, R, ζ, ∇ M ), where:

• I is a standard first-order interpretation consisting of a universe |I| and, for every operator symbol op, an interpretation I(op) : |I| n → |I| where n agrees with the arity of op. We assume that the universe |I| contains two distinguished, distinct values tt and ff.

• ξ : X → |I| is a valuation of the rigid variables.

• W is a non-empty set of states, and R ⊆ W × W is the accessibility relation.

• ζ : V × W → |I| is a valuation of the flexible variables at the different states of the model.

• ∇ M : 2 |I| → |I| is a function such that ∇ M (S ) = tt iff S ⊆ {tt}.
Note that we assume a constant universe, independent of the states of the model, and we also assume that all operators in O are rigid-i.e., interpreted independently of the states.

We inductively define the interpretations of expressions [[e]] M

w at state w of model M. When the model M is understood from the context, we drop it from the notation.

• [[x ]] M w = def ξ(x ) for x ∈ X • [[v ]] M w = def ζ(v , w ) for v ∈ V • [[op(e 1 , . . . , e n )]] M w = def I(op)([[e 1 ]] M w , . . . , [[e n ]] M w ) for op ∈ O • [[e 1 = e 2 ]] M w = def tt if [[e 1 ]] M w = [[e 2 ]] M w ff otherwise • [[false]] M w = def ff • [[ϕ ⇒ ψ]] M w = def tt if [[ϕ]] M w = tt or [[ψ]] M w = tt ff otherwise • [[∀ x : ϕ]] M w = def    tt if [[ϕ]] M ′ w = tt for all M ′ = (I, ξ ′ , W, R, ζ, ∇ M ) such that ξ ′ (y) = ξ(y) for all y ∈ X different from x ff otherwise • [[∇ϕ]] M w = def ∇ M ({[[ϕ]] M w ′ : (w , w ′ ) ∈ R}) We write M, w |= ϕ instead of [[ϕ]] M w = tt.
We say that ϕ is valid iff M, w |= ϕ holds for all M and w , and that it is satisfiable iff M, w |= ϕ for some M and w . We define a consequence relation |= as follows (where Γ is a set of formulas): Γ |= ϕ iff for all M, if M, w |= ψ for all ψ ∈ Γ and w ∈ W, then M, w |= ϕ for all w ∈ W.

Our definition of the semantics is a straightforward extension of the standard Kripke semantics to our setting, where ∇e need not denote a truth value. The condition on the function ∇ M used for interpreting ∇ ensures that M, w |= ∇ϕ iff M, w ′ |= ϕ for all w ′ such that (w , w ′ ) ∈ R as in the standard Kripke semantics. Because we assume a constant domain of interpretation, both Barcan formulas are valid-that is, we have validity of (∀x : ∇ϕ) ≡ ∇(∀x : ϕ).

(

Moreover, since all operator symbols have rigid interpretations, it is easy to prove by induction on the expression syntax that [[e]] w = [[e]] w ′ holds for all states w , w ′ whenever e is a rigid expression. It follows that implications of the form ϕ ⇒ ∇ϕ are valid for rigid ϕ-for example:

∀ x , y : (x = y) ⇒ ∇(x = y).

(2) w ∈ {tt, ff} specializes to the following clauses:

FOL and ML fragments of FOML

• [[v ]] K w = ζ(v , w ) for v ∈ V • [[false]] K w = ff • [[ϕ ⇒ ψ]] K w = tt iff [[ϕ]] K w = ff or [[ψ]] K w = tt • [[∇ϕ]] K w = tt iff [[ϕ]] K w ′ = tt for all w ′ ∈ W such that (w , w ′ ) ∈ R
The notions of validity |= ML ϕ, satisfiability, and consequence carry over as usual.

Coalescing Modal Expressions 4.1 Definition of the abstraction e FOL

One of our objectives is to apply standard first-order theorem provers for proving theorems of FOML that are instances of first-order reasoning. Since the operator ∇ is not available in first-order logic, we must translate FOML formulas ψ to purely first-order formulas ψ FOL such that the consequence Γ FOL |= FOL ϕ FOL entails Γ |= ϕ. A naive but unsound approach would be to replace the modal operator ∇ by a fresh monadic operator symbol Nec. As explained in Section 2, this approach is not sound. As we observed, a sound approach is to define ϕ FOL by using the well-known standard translation from modal logic to first-order logic [START_REF] Braüner | First order modal logic[END_REF][START_REF] Jürgen | Semantics-based translation methods for modal logics[END_REF] that makes explicit the FOML semantics. However, that translation introduces additional complexity-complexity that is unnecessary for proof obligations that follow from ordinary first-order reasoning.

Instead, we define ϕ FOL to be a syntactic first-order abstraction of ϕ in which modal subexpressions are coalesced-that is, replaced by fresh operators. If

ϕ is (v = 0) ⇒ ∇(v = 0), then ϕ FOL is (v = 0) ⇒ ∇(v = 0) , where ∇(v = 0) is a new 0-ary operator symbol.
We want to ensure that subexpressions appearing more than once are abstracted by the same operators, allowing for instances of first-order theorems to remain valid. This requires some care for expressions that contain bound variables. For example, we expect to prove

(∃ x , z : ∇(v = x )) ≡ (∃ y : ∇(v = y)) (3)
We therefore define the fresh operator symbols ∇e as λ-abstractions over the bound variables occurring in e, and these are identified modulo α-equivalence. Formally, we let e FOL = e ε

FOL

where ε denotes the empty list and, for a list y of rigid variables, the first-order expression e y FOL over the extended set of variables X ∪ V is defined inductively as follows.

• x y FOL = def x for x ∈ X a rigid variable, With these definitions, the formula (3) is coalesced as

• v y FOL = def v for v ∈ V a
(∃ x , z : λx : ∇(v = x ) (x )) ≡ (∃ y : λy : ∇(v = y) (y)) (4)
which is an instance of the valid first-order equivalence (∃ x , z : P (x )) ≡ (∃ y : P (y))

In particular, the two operator symbols occurring in (4) are identified because the two λexpressions are α-equivalent. Identification of coalesced formulas modulo α-equivalence ensures that the translation is insensitive to the names of bound (rigid) variables. Section 8 discusses techniques for abstracting from less superficial differences in first-order expressions, such as between λx , y and λy, x and between a = b and b = a.

Soundness of coalescing to FOL

For a set Γ of FOML formulas, we denote by Γ FOL the set of all formulas ψ FOL , for ψ ∈ Γ. We now show the soundness of the abstraction.

Theorem 1. For any set Γ of FOML formulas and any FOML formula ϕ, if

Γ FOL |= FOL ϕ FOL then Γ |= ϕ.
Proof (sketch).

Assume that Γ |= ϕ, so M = (I, ξ, W, R, ζ, ∇ M ) is a Kripke model such that M, w ′ |= ψ for all ψ ∈ Γ and w ′ ∈ W, but that M, w |= ϕ for some w ∈ W.

For the extended set of variables X ∪ V, define the first-order structure S = (I ′ , ξ ′ ) where I ′ agrees with I for all operator symbols that appear in Γ or ϕ, and where the valuation ξ ′ is defined by ξ ′ (x ) = ξ(x ) for x ∈ X and ξ ′ (v ) = ζ(w , v ) for v ∈ V. For the additional operator symbols introduced in Γ FOL and ϕ FOL , we define

I ′ ( λz : ∇e )(d 1 , . . . , d n ) = [[∇e]] M ′ w
where M ′ agrees with M except for the valuation ξ ′ that assigns the i th variable of z to d i . This interpretation is well-defined: if ∇e 1 and ∇e 2 are two expressions in Γ or ϕ that give rise to the same operator symbol, then (λz 1 : ∇e 1 ) and (λz 2 : ∇e 2 ) must be α-equivalent, and therefore

I ′ ( λz 1 : ∇e 1 )(d 1 , . . . , d n ) = I ′ ( λz 2 : ∇e 2 )(d 1 , . . . , d n ). It is straightforward to prove that [[e FOL ]] S = [[e]] M
w holds for all expressions e FOL that appear in Γ FOL or ϕ FOL . In particular, it follows that S |= FOL ψ FOL for all ψ ∈ Γ and S |= FOL ϕ FOL . This shows that Γ FOL |= FOL ϕ FOL and concludes the proof.

q.e.d.

Coalescing First-Order Expressions

We now define an abstraction ϕ ML of FOML formulas to formulas of propositional modal logic. Again, we require for soundness that Γ |= ϕ whenever Γ ML |= ML ϕ ML -that is, consequence between abstracted formulas implies consequence between the original ones. In this way, we can use theorem provers for propositional modal logic to carry out FOML proofs that are instances of propositional modal reasoning. The abstraction ϕ ML replaces all first-order subexpressions e of ϕ by new (propositional) flexible variables e , where variables ∀ x : e are once again identified modulo α-equivalence. Formally, the translation is defined as follows.

• x ML = def x for x ∈ X a rigid variable,

• v ML = def v for v ∈ V a flexible variable, • (op(t 1 , . . . , t n )) ML = def op(t 1 , . . . , t n ) for op ∈ O,
• (e 1 = e 2 ) ML = def e 1 = e 2 ,

• false ML = def false,

• (e 1 ⇒ e 2 ) ML = def (e 1 ) ML ⇒ (e 2 ) ML ,

• (∀ x : e) ML = def ∀ x : e ,

• (∇e) ML = def ∇e ML .

As an example, coalescing the formula

(x = y) ∧ ∇∆true ⇒ ∇∆(x = y) yields the ML-formula x = y ∧ ∇∆true ⇒ ∇∆ x = y (5)
The implication ( 5) is not ML-valid. However, for rigid variables x and y, it follows from the hypothesis x = y ⇒ ∇ x = y , which is justified by the FOML law (2). For a set Γ of FOML formulas, we denote by Γ ML the set of modal abstractions ψ ML , for all ψ ∈ Γ. Moreover, we define the set H(Γ) to consist of all formulas of the form e ⇒ ∇ e , for all flexible variables e introduced in Γ ML that correspond to rigid expressions e in Γ.

Theorem 2. Assume that Γ is a set of FOML formulas and that ϕ is a FOML formula. If Γ ML , H(Γ ∪ {ϕ}) |= ML ϕ ML then Γ |= ϕ.

Proof (sketch).

As in Theorem 1, we prove the contra-positive. Assume that M = (I, ξ, W, R, ζ, ∇ M ) is a Kripke model such that M, w ′ |= ψ for all ψ ∈ Γ and w ′ ∈ W, but M, w |= ϕ for a certain w ∈ W.

Define the propositional Kripke model K = (W, R, ζ ′ ) where ζ ′ assigns truth values in {tt, ff} to all states w ′ ∈ W and flexible variables in Γ ML or ϕ ML :

ζ ′ (w ′ , v ) = tt iff ζ(w ′ , v ) = tt for v ∈ V ζ ′ (w ′ , x ) = tt iff ξ(x ) = tt for x ∈ X ζ ′ (w ′ , op(t 1 , . . . , t n ) ) = tt iff [[op(t 1 , . . . , t n )]] M w ′ = tt ζ ′ (w ′ , e 1 = e 2 ) = tt iff [[e 1 ]] M w ′ = [[e 2 ]] M w ′ ζ ′ (w ′ , ∀ x : e ) = tt iff M, w ′ |= ∀ x : e
Again, ζ ′ is well-defined. It is easy to prove, for all w ′ ∈ W and all e such that e ML appears in Γ ML or ϕ ML , that K, w ′ |= e ML iff [[e]] M w ′ = tt. In particular, it follows that K, w ′ |= ψ ML for all ψ ∈ Γ and that K, w |= ML ϕ ML .

Furthermore, the definition of K ensures that K, w ′ |= ψ holds for all ψ ∈ H(Γ ∪ {ϕ}) and all

w ′ ∈ W because [[e]] M w ′ = [[e]] M
w ′′ holds for all rigid expressions e and all states w ′ , w ′′ ∈ W. It follows that Γ ML , H(Γ ∪ {ϕ}) |= ML ϕ ML , which concludes the proof.

q.e.d.

6 Coalescing in the presence of operator definitions

Operator definitions

We now extend our language to allow definitions of the form

d (x 1 , . . . , x n ) ∆ = e
where d is a fresh symbol, x 1 , . . . , x n are pairwise distinct rigid variables, and e is an expression whose free rigid variables are among x 1 , . . . , x n .

For an operator d defined as above and expressions e 1 , . . . , e n , the application d (e 1 , . . . , e n ) is a well-formed expression whose semantics is given by:

[[d (e 1 , . . . , e n )]] M w = [[e[e 1 /x 1 , . . . , e n /x n ]]] M w
In other words, the defining expression is evaluated when the arguments have been substituted for the variables. However, when reasoning about expressions containing defined operators, one does not wish to systematically expand definitions. If the precise definition is unimportant, it is better to leave the operator unexpanded in order to keep the formulas small. We now extend the coalescing techniques introduced in the preceding sections to handle expressions that may contain defined operators.

It is easy to see that the algorithm introduced in Section 5 for abstracting first-order subexpressions remains sound if we handle defined operators like operators in O. In particular, two expressions d (e 1 ) and d (e 2 ) are abstracted by the same flexible variable only if they are syntactically equal up to α-equivalence. However, this simple approach does not work for the algorithm of Section 4 that abstracts modal subexpressions. As an example, consider the definition

cst (x ) ∆ = ∃ y : ∇(x = y) (6)
and the formula

(u = v ) ⇒ (cst (u) ≡ cst (v )) (7)
where u and v are flexible variables. An expression e satisfies cst (e) at state w iff the value of e is the same at all reachable states w ′ . Hence, formula ( 7) is obviously not valid. If cst were treated like an operator in O, the algorithm of Section 4 would leave [START_REF] Ganzinger | The Saturate system[END_REF] unchanged. However, u and v would be considered ordinary (rigid) variables and cst would be considered an uninterpreted operator symbol, so [START_REF] Ganzinger | The Saturate system[END_REF], seen as a FOL formula, would be provable. Thus, it would be unsound to simply treat defined operators like operators in O in our algorithm for coalescing modal subexpressions.

Rigid arguments and Leibniz positions

The example above shows that in the presence of definitions, FOML formulas without any visible modal operators may violate the Leibniz principle that substituting equals for equals should yield equal results. However, a first observation shows that the Leibniz principle still holds for rigid arguments.

Lemma 3. For any defined n-ary operator d , expressions e 1 , . . . , e n , any i ∈ 1 .. n with e i rigid, Kripke model M, state w , and rigid variable x that does not occur free in any e j , we have

[[d (e 1 , . . . , e n )]] M w = [[d (e 1 , . . . , e i-1 , x , e i+1 , . . . , e n )]] M ′ w
where M ′ agrees with M except for the valuation ξ ′ of rigid variables, which is like

ξ but assigns x to [[e i ]] M w .
Proof (sketch). Since e i is rigid, the value of [[e i ]] M w ′ , for any w ′ ∈ W , is independent of the state w ′ . The assertion is then proved by induction on the defining expression for operator d .

q.e.d.

For a non-rigid argument of a defined operator, the Leibniz principle is preserved when the argument does not appear in a modal context in the defining expression. We inductively define which argument positions of an FOML operator or connective are Leibniz (satisfy the Leibniz principle).

Definition 4 (Leibniz argument positions).

• All argument positions of the operators in O and of all FOML connectives except ∇ are Leibniz. The single argument position of ∇ is not Leibniz.

• For an operator defined by d (x 1 , . . . , x n ) ∆ = e, the i th argument position of d is Leibniz iff x i does not occur within a non-Leibniz argument position in e.

In other words, the i th argument position of a defined operator is Leibniz iff the i th parameter does not appear in the scope of any occurrence of ∇ in the full expansion of the defining expression.

Lemma 5. Assume that d is a defined n-ary operator whose i th argument position is Leibniz (for i ∈ 1 .. n). For any expressions e 1 , . . . , e n , Kripke model M, state w and rigid variable x that does not occur free in any e j , we have

[[d (e 1 , . . . , e n )]] M w = [[d (e 1 , . . . , e i-1 , x , e i+1 , . . . , e n )]] M ′ w
where M ′ agrees with M except for the valuation ξ ′ of rigid variables, which is like ξ but assigns x to [[e i ]] M w .

Proof (sketch). Induction on the syntax of the defining expression for d . q.e.d.

It follows from Lemmas 3 and 5 that the implication

(e i = f ) ⇒ (d (e 1 , . . . , e n ) = d (e 1 , . . . , e i-1 , f , e i+1 , . . . , e n ))
is valid when e i and f are rigid expressions or when the i th argument position of d is Leibniz.

Coalescing for defined operators

The definition of the syntactic abstraction e FOL for the extended language is now completed by defining

• (d (e 1 , . . . , e n )) y FOL = def d , ǫ 1 , . . . , ǫ n ((e 1 ) y FOL , . . . , (e n ) y FOL ) for a defined n-ary operator d where

ǫ i = * if the i th position of d is Leibniz or e i is a rigid expression, ǫ i = e i otherwise.
With these definitions, the single argument position of operator cst introduced by ( 6) is not Leibniz, and coalescing formula [START_REF] Ganzinger | The Saturate system[END_REF] yields

(v = w ) ⇒ ( cst , v (v ) ≡ cst , w (w ))
for two distinct fresh operators cst , v and cst , w . As expected, this formula cannot be proved. However, the formula ∀ x , y : (x = y) ⇒ (cst (x ) ≡ cst (y)) is coalesced as ∀ x , y : (x = y) ⇒ ( cst , * (x ) ≡ cst , * (y)) and is valid. Theorem 6. Theorem 1 remains valid for FOML formulas in the presence of defined operator symbols.

Proof (sketch). Extending the proof of Theorem 1, we define the interpretation of the fresh operator symbols as follows:

I ′ ( d , ǫ 1 , . . . , ǫ n )(d 1 , . . . , d n ) = [[d (α 1 , . . . , α n )]] M ′ w where α i = e i if ǫ i = e i x i if ǫ i = *
In this definition, w is the state fixed in the proof and M ′ agrees with M except for the valuation ξ ′ that assigns the variables

x i to d i . Again, one proves that [[e FOL ]] S = [[e]] M
w for all expressions e FOL that appear in Γ FOL or ϕ FOL . For the expressions corresponding to applications of defined operators, the proof is obvious for those arguments where ǫ i = e i , and it makes use of Lemmas 3 and 5 when ǫ i = * .

q.e.d.

Proving Safety Properties by Coalescing in TLA

We now give evidence for the usefulness of coalescing by showing that it can be the basis for a complete proof system for establishing safety properties in TLA + , assuming the ability to prove any valid first-order formula in the set-theoretic language underlying TLA + . In fact, we argue that proofs of arbitrary safety properties can be transformed into the form used in Section 2.

In TLA + , properties of systems are expressed as temporal logic formulas, which are evaluated over infinite sequences of states. We say that a formula is true of a finite sequence of states if it is true for some infinite extension of that finite sequence. A formula expresses a safety property if it holds for an infinite sequence of states if and only if it holds for every finite prefix of that sequence.

The standard form of a TLA + specification is Init ∧2[Next ] v ∧L where Init is a state predicate (a first-order formula that contains only unprimed state variables), v is a tuple containing all state variables, Next is an action formula (a formula of first-order logic extended by the prime operator), and L is a conjunction of fairness conditions that are irrelevant for proving safety properties. In order to prove that the specification establishes a safety property P , we need to establish the theorem

Init ∧ 2[Next ] v ⇒ P .
The first step is to reformulate the problem as an invariant assertion of the form

HInit ∧ 2[HNext ] hv ⇒ 2Inv ( 8
)
where Inv is a state predicate. A general way to do this is to add a history variable [START_REF] Abadi | The existence of refinement mappings[END_REF] to the original specification. The history variable records the sequence of states seen so far, and Inv is true for a given value of the history variable if and only if the safety property P is true for the corresponding sequence of states.

The second step is to prove the invariance of Inv by using an inductive invariant -a state predicate IInv such that all of the following formulas are valid:

1. HInit ⇒ IInv 2. IInv ∧ [HNext ] hv ⇒ IInv ′ 3. IInv ⇒ Inv
Assuming that formula ( 8) is valid, a suitable inductive invariant IInv exists under standard assumptions on the expressiveness of the language of state predicates (see, e.g., [START_REF] Krzysztof | Ten years of Hoare's logic: A survey-part I[END_REF]), and these assumptions are satisfied by the set-theoretic language underlying TLA + .

By coalescing to propositional temporal logic using the techniques described in Section 5, a PTL decision procedure easily checks that (8) follows from facts (1)-( 3) above. In practice, we find it preferable to verify inferences in temporal logic by appealing to a decision procedure rather than by applying a fixed set of rules because the user is then free to structure the proof in the most convenient way. For example, the inductive invariant could be split into several mutually inductive formulas, for which the corresponding facts may be easier to check than (1)-( 3) in the standard invariance proof above. On the other hand, the inductive nature of the typical temporal logic proofs such as the one above makes it unrealistic to expect that an ordinary FOL prover would be able to establish the FOL translation of ( 8) from ( 1)- [START_REF] Benzmüller | Gödel's God on the computer[END_REF].

Completing the proof of ( 8) requires proving formulas (1)-( 3). Observe that (1) and ( 3) are state predicates and thus ordinary first-order formulas in TLA + 's set theory. By assumption, their proofs can be discharged by the underlying FOL prover.

Formula ( 2) is an action formula and therefore contains TLA + 's prime operator in addition to first-order logic, but no other operator of temporal logic. We now show how we reduce the proof of an action formula A to FOL proofs with the help of coalescing.

We begin by eliminating all defined operators that occur in A, expanding their definitions. This results in an action formula B that is equivalent to A, but that only contains built-in TLA + operators. Second, we use the fact that prime distributes over all non-modal built-in TLA + operators and rewrite formula B to an equivalent action formula C in which prime is only applied to flexible variables. 1 Finally, we apply the coalescing technique described in Section 4 for abstracting the prime modality, and obtain a formula C FOL . It can be shown that for the restricted fragment where all modal expressions are of the form v ′ for flexible variables v , the formula C is FOML-valid if and only if C FOL is FOL-valid, and therefore the underlying FOL prover will be able to prove formula (2) above.

The procedure above shows how in theory the two forms of coalescing that we have proposed in this paper can be complete for proving safety properties in TLA + , assuming that we have a complete proof procedure for the set theory underlying TLA + . In practice, no such procedure can exist and it is preferable to keep formulas small, so it is important not to expand all definitions. These practical considerations underlie the handling of defined operators described in Section 6.

Although we have focused on safety properties, for which we can obtain a completeness result, the same overall technique can also be applied to the proof of liveness properties. In TLA, liveness properties are also proved by combining action-level reasoning and temporal logic proof rules. Most of the steps in such a proof can be reduced by coalescing to FOL or propositional ML reasoning. However, there will often be a few steps that require nonpropositional temporal logic reasoning-for example, because they are based on well-founded orderings. Because there are not many such steps, a backend prover for them with a low degree of automation should be acceptable.

Conclusion

We presented a technique of coalescing that allows a user to decompose the proof of FOML formulas into purely first-order and purely propositional modal reasoning. This technique is inspired by reasoning about TLA + specifications and has been implemented in the TLA + Proof System, where we have found it useful for verifying temporal logic properties. In particular, the overwhelming majority of proof obligations that arise during TLA + proofs contain only the prime modal operator. For this fragment, rewriting by the valid equality op(e 1 , . . . , e n ) ′ = op(e ′ 1 , . . . , e ′ n ), for operators op ∈ O, followed by coalescing to FOL is complete. Many of the proof obligations that involve the 2 modality of TLA + are instances of propositional temporal reasoning, and these can be handled by coalescing to ML and invoking a decision procedure for propositional temporal logic.

Coalescing to FOL eschews semantic translation of FOML formulas [START_REF] Jürgen | Semantics-based translation methods for modal logics[END_REF] in favor of replacing a subformula whose principal operator is modal by a fresh operator symbol. The resulting formulas are simpler than those obtained by semantic translation, and they can readily be understood in terms of the original FOML formulation of the problem. Coalescing is not a complete proof procedure in itself. For example, the valid Barcan formula (1) cannot be proved using only our two translations. TLA proofs contain only a small number of such proof obligations, and we expect TLAPS to be able to handle them with a semantic translation to FOL. In our context, the validity problem of first-order temporal logic is Π 1 1 -complete, so incompleteness should not be considered an argument against the use of coalescing. Semantic translation of temporal logic would require inductive reasoning over natural numbers, and we could not even expect simple proofs such as the one shown in Section 2 to be discharged automatically, whereas proof by coalescing benefits from efficient decision procedures for propositional temporal logic. For applications other than TLA + theorem proving that require first-order modal reasoning, the trade-off in choosing between semantic translation and coalescing will depend upon how effective one expects semantic translation and standard first-order theorem proving to work in practice. One recent experiment [START_REF] Benzmüller | Gödel's God on the computer[END_REF] found this technique entirely satisfactory, but it used a modal logic too weak to handle the applications that concern us.

The definition of coalescing to FOL presented in Section 4 identifies modal subformulas such as (3) that are identical up to the names of bound rigid variables that they contain. This definition can be refined to identify formulas that differ in less superficial ways. For example, it may be desirable to reorder bound variables according to their appearance in coalesced subformulas. This would allow us to coalesce the formula (∃ y ∀ x : 2P (x , y)) ⇒ (∀ x ∃ y : 2P (x , y))

to the valid FOL formula (∃ y ∀ x : λx , y : 2P (x , y) (x , y)) ⇒ (∀ x ∃ y : λx , y : 2P (x , y) (x , y)) rather than the formula (∃ y ∀ x : λy, x : 2P (x , y) (y, x )) ⇒ (∀ x ∃ y : λx , y : 2P (x , y) (x , y)) obtained according to the definition given in Section 4, which results in the two fresh operators being distinct. In general, we would like coalesced versions of different expressions to use the same atomic symbol wherever that would be valid. For example, e 1 = e 2 and e 2 = e 1 could be the same symbol.

Rewriting a formula before coalescing can also make the translated obligation easier to prove. For example, the formula 2e for a rigid expression e can be replaced by 2false ∨ e. In a modal logic whose 2 modality is reflexive, the disjunct 2false is not necessary. In this way, the formula ∀ x , y : 2(x = y) ⇒ 2(f (x ) = f (y))

for f ∈ O could be proved directly by translating with coalescing to FOL instead of requiring two steps, the first proving (x = y) ⇒ (f (x ) = f (y)) with FOL and the second being translated to ML. Another such rewriting is distributing TLA's modal prime operator over rigid operators used by TLAPS when translating to FOL. We don't know yet if optimizations of the translations beyond those we have already implemented in TLAPS will be useful in practice. So far, we have proved only safety properties for realistic algorithms, which in TLA requires little temporal reasoning. We have begun writing formal liveness proofs, but TLAPS will not completely check them until we have a translation that can handle formulas which, like the Barcan formula, inextricably mix quantifiers and modal operators.

Figure 1 :

 1 Figure 1: Proof of a safety property in TLAPS.

  Two natural sublogics of FOML are first-order logic (FOL) and propositional modal logic (ML).FOL does not have flexible variables V or expressions ∇e. A first-order structure (I, ξ) consists of an interpretation I as above and a valuation ξ of the (rigid) variables. The inductive definition of the semantics consists of the relevant clauses of the one given above for FOML, and the notions of first-order validity |= FOL ϕ, satisfiability, and consequence carry over in the usual way.ML does not have rigid variables, quantifiers, operator symbols or equality. A (propositional) Kripke model for ML is given asK = (W, R, ζ)where the set of states W and the accessibility relation R are as for FOML, and the valuation ζ : V × W → {tt, ff} assigns truth values to flexible variables at every state. The inductive definition of [[e]] K

  flexible variable, • (op(e 1 , . . . , e n )) y FOL = def op((e 1 ) y FOL , . . . , (e n ) y FOL ) for op ∈ O, • (e 1 = e 2 ) y FOL = def (e 1 ) y FOL = (e 2 ) y FOL , • false y FOL = def false • (e 1 ⇒ e 2 ) y FOL = def (e 1 ) y FOL ⇒ (e 2 ) y FOL , • (∀ x : e) y FOL = def ∀ x : e x ,y FOL , • (∇e) y FOL = def λz : ∇e (z) where z is the subsequence of rigid variables in y that appear free in e. (If z is the empty sequence, this is simply ∇e .)

The syntax of TLA + ensures that prime cannot be nested.

This work has been partially funded by the Microsoft Research-Inria Joint Centre, France. It has also been supported by the European Union Seventh Framework Programme under grant agreement no. 295261 (MEALS) and by the French BGLE Project ADN4SE.