A Proof Theory for Model Checking: An Extended Abstract

TL;DR

This paper introduces a proof-theoretic foundation for model checking using sequent calculus, employing focused proof systems to handle state exploration and verification tasks more naturally.

Contribution

It develops a focused proof system that combines additive and multiplicative inference rules to improve the theoretical foundation of model checking.

Findings

Provides a proof-theoretic framework for reachability and non-reachability

Enables direct state exploration through synthetic rules

Supports bisimulation and winning strategies analysis

Abstract

While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of model checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since such rules allow provability to directly describe truth conditions. Unfortunately, the additive treatment of quantifiers requires inference rules to have infinite sets of premises and the additive treatment of model descriptions provides no natural notion of state exploration. By employing a focused proof system, it is possible to construct large scale, synthetic rules that also qualify as additive but contain elements of multiplicative inference. These additive synthetic rules -- essentially rules built from the description of a model -- allow a direct treatment of state exploration. This proof theoretic framework provides a natural treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.

Equations

$$⊢B,\Delta ⊢\Delta ⊢\Delta ,B⊢\Delta ,B,B⊢B,\neg B⊢\Delta {,}_{\_}1{\Delta }_{\_}2⊢{\Delta }_{\_}1,B⊢{\Delta }_{\_}2,\neg B$$

$$⊢B\wedge C,\Delta ⊢B,\Delta ⊢C,\Delta ⊢B\wedge C,{\Delta }_{\_}1,{\Delta }_{\_}2⊢B,{\Delta }_{\_}1⊢C,{\Delta }_{\_}2$$

$$⊢B_{\_}1\wedge B_{\_}2,\Delta ⊢B_{\_}1,\Delta ⊢B_{\_}2,\Delta ⊢t,\Delta ⊢B_{\_}1\vee B_{\_}2,\Delta ⊢B_{\_}1,\Delta ⊢B_{\_}1\vee B_{\_}2,\Delta ⊢B_{\_}2,\Delta$$

$$⊢t=t,\Delta ⊢t\ne s,\Delta$$

$$⊢\exists x.B,\Delta ⊢B[t/x],\Delta ⊢\forall x.B,\Delta \{⊢B[t/x],\Delta |\Sigma -termt\}$$

$$\forall x.(x\ne 0\wedge x\ne 1)\vee x=0\vee x=1\vee x=2$$

$$\mathcal{X};\Gamma ⊢A\text{and}B,\Delta \mathcal{X};\Gamma ⊢A,\Delta \mathcal{X};\Gamma ⊢B,\Delta \mathcal{X};\Gamma ⊢t^{-},\Delta \mathcal{X};\Gamma ,A\text{and}B⊢\Delta \mathcal{X};\Gamma ,A⊢\Delta \mathcal{X};\Gamma ,A\text{and}B⊢\Delta \mathcal{X};\Gamma ,B⊢\Delta$$

$$\mathcal{X};\Gamma ,A\vee B⊢\Delta \mathcal{X};\Gamma ,A⊢\Delta \mathcal{X};\Gamma ,B⊢\Delta \mathcal{X};\Gamma ,f⊢\Delta \mathcal{X};\Gamma ⊢A\vee B,\Delta \mathcal{X};\Gamma ⊢A,\Delta \mathcal{X};\Gamma ⊢A\vee B,\Delta \mathcal{X};\Gamma ⊢B,\Delta$$

$$\mathcal{X};\Gamma ,{\Gamma }^{\prime }⊢A\wedge {}^{+}B,\Delta ,{\Delta }^{\prime }\mathcal{X};\Gamma ⊢A,\Delta \mathcal{X};{\Gamma }^{\prime }⊢B,{\Delta }^{\prime }\mathcal{X};⊢t^{+},\mathcal{X};\Gamma ,A\wedge {}^{+}B⊢\Delta \mathcal{X};\Gamma ,A,B⊢\Delta \mathcal{X};\Gamma ,t^{+}⊢\Delta \mathcal{X};\Gamma ⊢\Delta$$

$$\mathcal{X};\Gamma ⊢A\supset B,\Delta \mathcal{X};\Gamma ,A⊢B,\Delta \mathcal{X};\Gamma ,{\Gamma }^{\prime },A\supset B⊢\Delta ,{\Delta }^{\prime }\mathcal{X};\Gamma ⊢A,\Delta \mathcal{X};{\Gamma }^{\prime },B⊢{\Delta }^{\prime }$$

$$\mathcal{X};\Gamma ⊢\exists x.B,\Delta \mathcal{X};\Gamma ⊢B[t/x],\Delta \mathcal{X};\Gamma ⊢\forall x.B,\Delta \mathcal{X},y;\Gamma ⊢B[y/x],\Delta \mathcal{X};⊢t=t\mathcal{X};t\ne t⊢$$

$$\vbox{\noindent When $t$ and $s$ are not unifiable,}\quad{\cal X}\,;\,\Gamma,t=s\vdash\Delta\qquad{\cal X}\,;\,\Gamma\vdash t\not=s,\Delta$$

$$\vbox{\noindent Otherwise, set $\theta=\hbox{mgu}(t,s)$}\quad{\cal X}\,;\,\Gamma,t=s\vdash\Delta\theta{\cal X}\,;\,\theta\Gamma\vdash\theta\Delta\qquad{\cal X}\,;\,\Gamma\vdash t\not=s,\Delta\theta{\cal X}\,;\,\theta\Gamma\vdash\theta\Delta$$

$$\cdot ;\cdot ⊢\forall x.(x=0\vee x=1)\supset (x=0\vee x=1\vee x=2)x;x=0\vee x=1⊢x=0\vee x=1\vee x=2\text{lx@proof@logical@and}x;x=0⊢x=0\vee x=1\vee x=2\cdot ;\cdot ⊢0=0\vee 0=1\vee 0=2\cdot ;\cdot ⊢0=0x;x=1⊢x=0\vee x=1\vee x=2\cdot ;\cdot ⊢1=0\vee 1=1\vee 1=2\cdot ;\cdot ⊢1=1$$

$$\mu (\lambda A\lambda x\lambda y.(x=a\wedge {}^{+}y=b)\vee$$

$$\displaystyle\mu(\lambda{}A\lambda{}x\lambda{}z.\,{x}\buildrel\over{\longrightarrow}{z}\mathbin{\vee}(\exists{}y.\,{x}\buildrel\over{\longrightarrow}{y}\mathbin{\wedge\kern-1.5pt^{+}}{}A\,y\,z)).$$

$$\mathcal{X};\Gamma ⊢\mu B\bar{t},\Delta \mathcal{X};\Gamma ⊢B(\mu B)\bar{t},\Delta \mathcal{X};\Gamma ,\mu B\bar{t}⊢\Delta \text{lx@proof@logical@and}\mathcal{X};\Gamma ,S\bar{t}⊢\Delta \mathcal{X},\bar{x};BS\bar{x}⊢S\bar{x}$$

$$\mathcal{X};\Gamma ,\nu B\bar{t}⊢\Delta \mathcal{X};\Gamma ,B(\nu B)\bar{t}⊢\Delta \mathcal{X};\Gamma ⊢\nu B\bar{t},\Delta \text{lx@proof@logical@and}\mathcal{X};\Gamma ⊢S\bar{t},\Delta \bar{x};S\bar{x}⊢BS\bar{x}$$

$$\begin{array}[]{c}{\cal X}\,;\,\Gamma,\mu{}B\bar{t}\vdash\Delta{\cal X}\,;\,\Gamma,B(\mu{}B)\bar{t}\vdash\Delta\qquad{\cal X}\,;\,\Gamma\vdash\nu{}B\bar{t},\Delta{\cal X}\,;\,\Gamma\vdash B(\nu{}B)\bar{t},\Delta\end{array}$$

$$\frac{a\text{buildrel}}{⟶c⊢\cdot (a=a\wedge {}^{+}c=b)\vee (a=b\wedge {}^{+}c=c)\vee (a=c\wedge {}^{+}c=b)⊢\cdot a=a\wedge {}^{+}c=b⊢\cdot a=a,c=b⊢\cdot a=b\wedge {}^{+}c=c⊢\cdot a=b,c=c⊢\cdot a=c\wedge {}^{+}c=b⊢\cdot a=c,c=b⊢\cdot }$$

$$\mathcal{X};\Gamma ,\text{sl}path(t,s)⊢\Delta \mathcal{X};\Gamma ⊢\Delta \mathcal{X};\Gamma ,\text{sl}path(t,y)⊢\Delta \{\mathcal{X};\Gamma ,\text{sl}path(s,y)⊢\Delta |⟨t,s⟩\in \text{sl}Adj\}$$

$$\mathrm{Nature}=$$

$$\text{sl}plus=$$

$$\forall n\forall m\forall p.\mathrm{Nature}n\supset \mathrm{Nature}m\supset \text{sl}plusnmp\supset \text{sl}plusmnp$$

$$\text{sl}lt=\mu \lambda L\lambda x\lambda y((x=z\wedge {}^{+}\exists y^{\prime }.y=s{y}^{\prime })\vee (\exists x^{\prime }\exists y^{\prime }.x=s{x}^{\prime }\wedge {}^{+}y=s{y}^{\prime }\wedge {}^{+}L{x}^{\prime }{y}^{\prime }))$$

$$\mathcal{X};\mu B\bar{t}⊢\mu B\bar{t}\mathcal{X};\nu B\bar{t}⊢\nu B\bar{t}$$

Full text

1 Introduction

Model checking was introduced in the early 1980’s as a way to establish properties about (concurrent) computer programs that were hard or impossible to establish using traditional, axiomatic proof techniques such as those describe by Floyd and Hoare [6]. In this extended abstract we show that model checking can be given a proof theoretic foundation using the sequent calculus of Gentzen [7], the linear logic of Girard [8], and a treatment of fixed points [3, 5, 12, 18]. The main purpose of this extended abstract is foundational and conceptual. Our presentation will not shed any new light on the algorithmic aspects of model checking but it will show how model checkers can be seen as having a “proof search” foundation shared with logic programming and (inductive) theorem proving.

Since the emphasis of model checking is on establishing the truth of a property in a model, a natural connection with proof theory is via the use of additive connectives and their inference rules. We illustrate in Section 3 how the proof theory of additive connectives naturally leads to the usual notion of truth-table evaluation for propositional connectives. Relying only on additive connectives, however, fails to provide an adequate inference-based approach to model checking since it only rephrases truth-functional semantic conditions and requires rules with potentially infinite sets of premises.

The proof theory of sequent calculus contains additional inference rules, namely, the multiplicative inference rules which can be used to encode much of the algorithmic aspects of model checking such as, for example, those related to determining reachability and simulation (or winning strategies). In order to maintain a close connection between model checking and truth in model, we shall put additive inference rules back in the center of our framework but this time these rules will be additive synthetic inference rules. The synthesizing process will allow multiplicative connectives and inference rules to appear inside the construction of synthetic rules but they will not appear outside such synthetic rules. The construction of synthetic inference rules will be governed by the well established proof theoretic notions of polarization and focused proof systems [2, 9].

The connection between the proof theory based on such synthetic inference rules and model checking steps is close enough that certificates for both reachability and non-reachability as well as bisimulation and non-bisimulation are representable as sequent calculus proofs.

2 The basics of the sequent calculus

Let $\Delta$ and $\Gamma$ range over multisets of formulas. A sequent is either one-sided, written $\vdash\Delta$, or two-sided, written $\Gamma\vdash\Delta$ (we first consider two-sided sequents in Section 5). Inference rules have one sequent as their conclusion and zero or more sequents as premises. We divide inference rules into three groups: the identity rules, the structural rules, and the introduction rules. The following are the two structural rules and two identity rules we consider.

[TABLE]

The negation symbol $\neg(\cdot)$ is used here not as a logical connective but as a function that computes the negation normal form of a formula. The remaining rules of the sequent calculus are introduction rules: for these rules, a logical connective has an occurrence in the conclusion and does not have an occurrence in the premises. (We shall see several different sets of introduction inference rules shortly.)

When a sequent calculus inference rule has two (or more) premises, there are two natural schemes for managing the side formulas (i.e., the formulas not being introduced) in that rule. The following rules illustrate these two choices for conjunction.

[TABLE]

The choice on the left is the additive version of the rule: here, the side formulas in the conclusion are the same in all the premises. The choice on the right is the multiplicative version of the rule: here, the various side formulas of the premises are accumulated to be the side formulas of the conclusion. Note that the cut rule above is an example of a multiplicative inference rule. A logical connective with an additive right introduction rule is also classified as additive. In addition, the de Morgan dual and the unit of an additive connective are also additive connectives. Similarly, a logical connective with a multiplicative right-introduction rule is called multiplicative; so are its de Morgan dual and their units.

The multiplicative and additive versions of inference rules are, in fact, inter-admissible if the proof system contains weakening and contraction. In linear logic, where these structural rules are not available, the conjunction and disjunction have additive versions $\mathbin{\&}$ and $\mathbin{\oplus}$ and multiplicative versions $\mathbin{\otimes}$ and $\mathbin{\wp}$, respectively, and these different versions of conjunction and disjunction are not provably equivalent. Linear logic provides two exponentials, namely the $\mathop{!}$ and $\mathop{?}$, that permit limited forms of the structural rules for suitable formulas. The familiar exponential law $x^{n+m}=x^{n}x^{m}$ extends to the logical additive and multiplicative connectives since $\mathop{!}(B\mathbin{\&}C)\equiv\mathop{!}B\mathbin{\otimes}\mathop{!}C$ and $\mathop{?}(B\mathbin{\oplus}C)\equiv\mathop{?}B\mathbin{\wp}\mathop{?}C$.

While we are interested in model checking as it is practiced, we shall be interested in only performing inference in classical logic. One of the surprising things to observe about our proof theoretical treatment of model checking is that almost all of it can be seen as taking place within the proof theory of linear logic, a logic that sits behind classical (and intuitionistic) logic. As a result, the distinction between additive and multiplicative connectives remains an important distinction for our framework. Also, weakening and contraction will not be eliminated completely but will be available for only certain formulas and in certain inference steps (echoing the fact that in linear logic, these structural rules can be applied to formulas annotated with exponentials).

3 Additive propositional connectives

Let ${\cal A}$ be the set of formulas built from the propositional connectives $\{\wedge,t,\vee,f\}$ (no propositional constants included). Consider the following small proof system involving one-sided sequents.

[TABLE]

Here, $t$ is the unit of $\wedge$, and $f$ is the unit of $\vee$. Notice that $\vee$ has two introduction rules while $f$ has none. Also, $t$ and $\wedge$ are de Morgan duals of $f$ and $\vee$, respectively. We say that the multiset $\Delta$ is provable if and only if there is a proof of $\vdash\Delta$ using these inference rules. Also, we shall consider no additional inference rules (that is, no contraction, weakening, initial, or cut rules): this inference system is composed only of introduction rules and all of these introduction rules are for additive logical connectives.

The following theorem identifies an important property of this purely additive setting. This theorem is proved by a straightforward induction on the structure of proofs.

Theorem 1** (Strengthening)**

If $\Delta$ is a multiset of ${\cal A}$-formulas and $\vdash\Delta$ then $\exists\;B\in\Delta$ such that $\vdash B$.

This theorem shows that provability of purely additive formulas is independent of their context. It also establishs that the proof system is consistent, since the empty sequent $\vdash\cdot$ is not provable.

The following three theorems state that the missing inference rules of weakening, contraction, initial, and cut are all admissible in this proof system. The first theorem is an immediate consequence of Theorem 1. The following two theorems are proved, respectively, by induction on the structure of formulas and by induction on the structure of proofs.

Theorem 2** (Weakening & contraction admissibility)**

Let $\Delta_{\_}1$ and $\Delta_{\_}2$ be multisets of ${\cal A}$-formulas such that $\Delta_{\_}1$ is a subset of $\Delta_{\_}2$ (when viewed as sets). If $\vdash\Delta_{\_}1$ is provable then $\vdash\Delta_{\_}2$ is provable.

Theorem 3** (Initial admissibility)**

Let $B$ be a ${\cal A}$-formula. Then $\vdash B,\neg B$ is provable.

Theorem 4** (Cut admissibility)**

Let $B$ be an ${\cal A}$-formula and let $\Delta_{\_}1$ and $\Delta_{\_}2$ be multisets of ${\cal A}$-formulas. If both $\vdash B,\Delta_{\_}1$ and $\vdash\neg B,\Delta_{\_}2$ are provable, then there is a proof of $\vdash\Delta_{\_}1,\Delta_{\_}2$.

These theorems lead to the following truth-functional semantics for ${\cal A}$ formulas: define $v(\cdot)$ as a mapping from ${\cal A}$ formulas to booleans such that $v(B)$ is $t$ if $\vdash B$ is provable and is $f$ if $\vdash\neg B$ is provable. Theorem 3 implies that $v(\cdot)$ is always defined and Theorem 4 implies that $v(\cdot)$ is functional (does not map a formula to two different booleans). The introduction rules describe this function denotationally: e.g., $v(A\wedge B)$ is the truth-functional conjunction of $v(A)$ and $v(B)$ (similarly for $\vee$).

While this logic of ${\cal A}$-formulas is essentially trivial, we will soon introduce much more powerful additive inference rules: their connection to truth functional interpretations (a la model checking principles) will arise from the fact that their provability is not dependent on other formulas in a sequent.

4 Additive first-order structures

We move to first-order logic by adding terms, equality on terms, and quantification.

We shall assume that some ranked signature $\Sigma$ of term constructors is given: such a signature associates to every constructor a natural number indicating that constructor’s arity. Term constants are identified with signature items given rank 0. A $\Sigma$-term is a (closed) term built from only constructors in $\Sigma$ and obeying the rank restrictions. For example, if $\Sigma$ is $\{a/0,b/0,f/1,g/2\}$, then $a$, $(f~{}a)$, and $(g~{}(f~{}a)~{}b)$ are all $\Sigma$-terms.We shall consider only signatures for which there exist $\Sigma$-terms: for example, the set $\{f/1,g/2\}$ is not a valid signature. The usual symbols $\forall$ and $\exists$ will be used for the universal and existential quantification over terms. We assume that these quantifiers range over $\Sigma$-terms for some fixed signature. The arities of ranked signatures will often not be listed explicitly.

The equality and inequality of terms will be treated as (de Morgan dual) logical connectives in the sense that their meaning is given by the following introduction rules.

[TABLE]

Here, $t$ and $s$ are $\Sigma$-terms for some ranked signature $\Sigma$.

Consider (only for the scope of this section) the following two inference rules for quantification. In these introduction rules, $[t/x]$ denotes the capture-avoiding substitution.

[TABLE]

Although $\forall$ and $\exists$ form a de Morgan dual pair, the rule for introducing the universal quantifier is not the standard one used in the sequent calculus (we will introduce the standard one later). This rule, which is similar to the $\omega$-rule [15], is an extensional approach to modeling quantification: a universally quantified formula is true if all instances of it are true.

Consider now the logic built with the (additive) propositional constants of the previous section and with equality, inequality, and quantifiers. The corresponding versions of all four theorems in Section 3 holds for this logic. Similarly, we can extend the evaluation function for ${\cal A}$-formulas to work for the quantifiers: in particular, $v(\forall x.Bx)=\bigwedge_{\_}tv(Bt)$ and $v(\exists x.Bx)=\bigvee_{\_}tv(Bt)$. Such a result is not surprising, of course, since we have repeated within inference rules the usual semantic conditions. The fact that these theorems hold indicates that the proof theory we have presented so far offers nothing new over truth functional semantics. Similarly, this bit of proof theory offers nothing appealing to model checking, as illustrated by the following example.

Example 5

Let $\Sigma$ contain the ranked symbols $z/0$ and $s/1$ and let us abbreviate the terms $z$, $(s~{}z)$, $(s~{}(s~{}z))$, $(s~{}(s~{}(s~{}z)))$, etc by 0, 1, 2, 3, etc. Let $A$ and $B$ be the set of terms $\{{\bf 0},{\bf 1}\}$ and $\{{\bf 0},{\bf 1},{\bf 2}\}$, respectively. These sets can be encoded as the predicate expressions $\lambda x.x={\bf 0}\vee x={\bf 1}$ and $\lambda x.x={\bf 0}\vee x={\bf 1}\vee x={\bf 2}$. The fact that $A$ is a subset of $B$ can be denoted by the formula $\forall x.\neg(A\,x)\vee B\,x$ or, equivalently, as

[TABLE]

Proving this formula requires an infinite number of premises of the form $(t\not={\bf 0}\wedge t\not={\bf 1})\vee t={\bf 0}\vee t={\bf 1}\vee t={\bf 2}$. Since each of these premises can, of course, be proved, the original formula is provable, albeit with an “infinite proof”.

While determining the subset relation between two finite sets is a typical example of a model checking problem, one would not use the above-mentioned inference rule for $\forall$ except in the extreme cases where there is a finite and small set of $\Sigma$-terms. As we can see, the additive inference rule for $\forall$-quantification generally leads to “infinitary proofs” (an oxymoron that we now avoid at all costs).

5 Multiplicative connectives

Our departure from purely additive inference rules now seems forced and we continue by adding multiplicative inference rules.

Our first multiplicative connective is the intuitionistic implication: since the most natural treatment of this connective uses two-sided sequents, we make the move away from the one-sided sequents that we have presented so far (see Figure 1). Note that taking the two multiplicative rules of implication right introduction and initial yields a proof system that violates the strengthening theorem (Section 3): the sequent $\vdash p\mathbin{\supset}q,p$ is provable while neither $\vdash p\mathbin{\supset}q$ nor $\vdash p$ are provable.

A common observation in proof theory is that the curry/uncurry equivalence between $A\mathbin{\supset}B\mathbin{\supset}C$ and $(A\wedge B)\mathbin{\supset}C$ can be mimicked precisely by the proof system: in this case, such precision does not occur with the additive rules for conjunction but rather with the multiplicative version of conjunction. To this end, we add the multiplicative conjunction $\mathbin{\wedge\kern-1.5pt^{+}}$ and its unit $t^{+}$ and, for the sake of symmetry, we rename $\wedge$ as $\and$ and $t$ to $t^{-}$. (The plus and minus symbols are related to the polarization of logical connectives that is behind the construction of synthetic connectives.) These two conjunctions and two truth symbols are logically equivalent in classical and intuitionistic logic although they are different in linear logic where it is more traditional to write $\mathbin{\&}$, $\top$, $\mathbin{\otimes}$, $\mathbf{1}$ for $\and$, $t^{-}$, $\mathbin{\wedge\kern-1.5pt^{+}}$, $t^{+}$, respectively. The “multiplicative false” $f^{-}$ (written as $\perp$ in linear logic) can be defined as $t\not=t$ (assuming that there is a first-order term $t$).

Eigenvariables are binders at the sequent level that align with binders within formulas (i.e., quantifiers). Binders are an intimate and low-level feature of logic: the addition of eigenvariables requires redefining the notions of term and sequent.

Let the set ${\cal X}$ denote first-order variables and let $\Sigma({\cal X})$ denote all terms built from constructors in $\Sigma$ and from the variables ${\cal X}$: in the construction of $\Sigma({\cal X})$-terms, variables act as constructors of arity 0. (We assume that $\Sigma$ and ${\cal X}$ are disjoint.) A $\Sigma({\cal X})$-formula is one where all term constructors are taken from $\Sigma$ and all free variables are contained in ${\cal X}$. Sequents are now written as ${\cal X}\,;\,\Gamma\vdash\Delta$: the intended meaning of such a sequent is that the variables in the set ${\cal X}$ are bound over the formulas in $\Gamma$ and $\Delta$. We shall also assume that formulas in $\Gamma$ and $\Delta$ are all $\Sigma({\cal X})$-formulas. All inference rules are modified to account for this additional binding: see Figure 1. The variable $y$ used in the $\forall$ introduction rule is called, of course, an eigenvariable.

The left introduction rules for equality in Figure 1 significantly generalizes the version involving only closed terms by making reference to unifiability and to most general unifiers. In the latter case, the domain of the substitution $\theta$ is a subset of ${\cal X}$, and the set of variables $\theta{\cal X}$ is the result of removing from ${\cal X}$ all the variables in the domain of $\theta$ and then adding in all those variables free in the range of $\theta$. This treatment of equality was developed independently by Schroeder-Heister [14] and Girard [10] and has been extended to include simply typed $\lambda$-terms [12].

While the use of eigenvariables in proofs allows us to deal with quantifiers with finite proofs, that treatment is not directly related to model theoretic semantics. In particular, the strengthening theorem does not hold for this proof system. As a result, obtaining a soundness and completeness theorem for this logic is no longer trivial.

The inference rules in Figure 1 provide a proper proof of the theorem considered in Example 5.

Example 6

*Let $\Sigma$ and the sets $A$ and $B$ be as in Example 5. Showing that $A$ is a subset of $B$ requires showing that the formula $\forall x(Ax\mathbin{\supset}Bx)$ is provable. That is, we need to find a proof of the sequent $\vdash\forall x.(x={\bf 0}\vee x={\bf 1})\mathbin{\supset}(x={\bf 0}\vee x={\bf 1}\vee x={\bf 2}).$ The following proof of this sequent uses the rules from Figure 1: a double line means that two or more inference rules might be chained together. *

[TABLE]

The proof in this example is able to account for a simple version of “reachability” in the sense that we only need to consider checking membership in set $B$ for just those elements “reached” in $A$.

6 Fixed points

A final step in building a logic that can start to provide a foundation for model checking is the addition of least and greatest fixed points and their associated rules for induction and coinduction. Given that processes generally exhibit potentially infinite behaviors and that term structures are not generally bounded in their size, it is important for a logical foundation of model checking to allow for some treatment of infinity. The logic described by the proof system in Figure 1 is a two-sided version of MALL= (multiplicative additive linear logic extended with first-order quantifiers and equality) [5]. The decidability of this logic is easy to show: as one moves from conclusion to premise in every inference rule, the number of occurrences of logical connectives decrease. As a result, it is a simple matter to write an exhaustive search procedure that must necessarily terminate (such a search procedure can also make use of the decidable procedure of first-order unification).

In order to extend the expressiveness of MALL, Girard added the exponentials $\mathop{!}$, $\mathop{?}$ to MALL to get full linear logic [8]. The standard inference rules for exponentials allows for some forms of the contraction rule (Section 2) to appear in proofs and, as a result, provability is no longer decidable. A different approach to extending MALL with the possibility of having unbounded behavior was proposed in [5]: add to MALL= the least and greatest fixed point operators, written as $\mu$ and $\nu$, respectively. The proof theory of the resulting logic, called $\mu\hbox{MALL}^{=}$, was been developed in [3] and exploited in a prototype model checker [4].

Fixed point expressions are written as $\mu{}B\,\bar{t}$ or $\nu{}B\,\bar{t}$, where $B$ is an expression representing a monotonic higher-order abstraction, and $\bar{t}$ is a list of terms; by monotonic, we mean that the higher-order argument of $B$ can only occur in $B$ under even numbers of negations. The unfolding of the fixed point expressions $\mu B\,\bar{t}$ and $\nu B\,\bar{t}$ are $B(\mu{}B)\,\bar{t}$ and $B(\nu{}B)\,\bar{t}$, respectively.

Example 7

Horn clauses (in the sense of Prolog) can be encoded as purely positive fixed point expressions. For example, here is the Horn clause logic program (using the $\lambda$Prolog syntax, the sigma Y\ construction encodes the quantifier $\exists{}Y$) for specifying a (tiny) graph and its transitive closure:

step a b. step b c. step c b. path X Y :- step X Y. path X Z :- sigma Y\ step X Y, path Y Z. *

We can translate the step relation into the binary predicate ${\cdot}\buildrel\over{\longrightarrow}{\cdot}$ defined by

[TABLE]

which only uses positive connectives. Likewise, path can be encoded as the relation $\hbox{\sl path}(\cdot,\cdot)$:

[TABLE]

To illustrate unfolding of the adjacency relation, note that unfolding the expression ${a}\buildrel\over{\longrightarrow}{c}$ yields the formula $(a=a\mathbin{\wedge\kern-1.5pt^{+}}c=b)\mathbin{\vee}(a=b\mathbin{\wedge\kern-1.5pt^{+}}c=c)\mathbin{\vee}(a=c\mathbin{\wedge\kern-1.5pt^{+}}c=b)$ which is not provable. Unfolding the expression $\hbox{\sl path}(a,c)$ and performing $\beta$-reductions yields the expression {a}\buildrel\over{\longrightarrow}{c}\mathbin{\vee}(\exists{}y.\,{a}\buildrel\over{\longrightarrow}{y}\mathbin{\wedge\kern-1.5pt^{+}}{}\hbox{\sl path}\,y\,c).

In $\mu\hbox{MALL}^{=}$, both $\mu$ and $\nu$ are treated as logical connectives in the sense that they will have introduction rules. They are also de Morgan duals of each other. The inference rules for treating fixed points are given in Figure 2. The rules for induction and coinduction ($\mu L$ and $\nu R$, respectively) use a higher-order variable $S$ which represents the invariant and coinvariant in these rules. As a result, it will not be the case that cut-free proofs will necessarily have the sub-formula properties: the invariant and coinvariant are not generally subformulas of the rule that they conclude. The following unfolding rules are also admissible since they can be derived using induction and coinduction.

[TABLE]

The introduction rules in Figures 1 and 2 are exactly the introduction rules of $\mu\hbox{MALL}^{=}$, except for two shallow differences. The first difference is that the usual presentation of $\mu\hbox{MALL}^{=}$ is via one-sided sequents (here, we use two-sided sequents). The second difference is that we have written many of the connectives differently (hoping that our set of connectives will feel more comfortable to those not familiar with linear logic). To be precise, to uncover the linear logic presentation of formulas, one must translate $\and$, $t^{-}$, $\mathbin{\wedge\kern-1.5pt^{+}}$, $t^{+}$, $\vee$, and $\supset$ to $\mathbin{\&}$, $\top$, $\mathbin{\otimes}$, $\mathbf{1}$, $\oplus$, and $\mathbin{-\circ}$ [8]. Note that the linear implication $B\mathbin{-\circ}C$ can be taken as an abbreviation of $\neg B\mathbin{\wp}C$.

The following example shows that it is possible to prove some negations using either unfolding (when there are no cycles in the resulting state exploration) or induction.

Example 8

*Below is a proof that the node $a$ is not adjacent to $c$: the first step of this proof involves unfolding the definition of the adjacency predicate into its description. *

[TABLE]

A simple proof exists for $\hbox{\sl path}(a,c)$: one simply unfolds the fixed point expression for $\hbox{\sl path}(\cdot,\cdot)$ and chooses correctly when presented with a disjunction and existential on the right of the sequent arrow. Given the definition of the path predicate, the following rules are clearly admissible. We write $\langle t,s\rangle\in\hbox{\sl Adj}$ whenever $\cdot\vdash{t}\buildrel\over{\longrightarrow}{s}$ is provable.

[TABLE]

The second rule has a premise for every pair $\langle t,s\rangle$ of adjacent nodes: if $t$ is adjacent to no nodes, then this rule has no premises and the conclusion is immediately proved. A naive attempt to prove that there is no path from $c$ to $a$ gets into a loop (using these admissible rules): attempt to prove $\hbox{\sl path}(c,a)\vdash\cdot$ leads to an attempt to prove $\hbox{\sl path}(b,a)\vdash\cdot$ and again attempting to prove $\hbox{\sl path}(c,a)\vdash\cdot$. Such a cycle can be examined to yield an invariant that makes it possible to prove the end-sequent. In particular, the set of nodes reachable from $c$ is $\{b,c\}$, subset of $N=\{a,b,c\}$. The invariant $S$ can be described as the set which is the complement (with respect to $N\times N$) of the set $\{b,c\}\times\{a\}$, or equivalently as the predicate $\lambda x\lambda y.\bigvee_{\_}{\langle u,v\rangle\in S}(x=u\mathbin{\wedge\kern-1.5pt^{+}}y=v)$. With this invariant, the induction rule ($\mu L$) yields two premises. The left premise simply needs to confirm that the pair $\langle c,a\rangle$ is not a member of $S$. The right premise sequent $\bar{x}\,;\,BS\bar{x}\vdash S\bar{x}$ establishes that $S$ is an invariant for the $\mu{}B$ predicate. In the present case, the argument list $\bar{x}$ is just a pair of variables, say, $x,z$, and $B$ is the body of the path predicate: the right premise is the sequent \ x,z\;;\;{x}\buildrel\over{\longrightarrow}{z}\mathbin{\vee}(\exists{}y.\,{x}\buildrel\over{\longrightarrow}{y}\mathbin{\wedge\kern-1.5pt^{+}}{}S\,y\,z)\vdash S\,x\,z. A formal proof of this follows easily by blindly applying applicable inference rules.

While the rules for fixed points (via induction and coinduction) are strong enough to transform cyclic behaviors into, for example, non-reachabilty or (bi)simulation assertions, these rules are not strong enough to prove other simple facts about fixed points. For example, consider the following two named fixed point expressions used for identifying natural numbers and the ternary relation of addition.

[TABLE]

The following formula (stating that the addition of two numbers is commutative)

[TABLE]

is not provable using the inference rules we have described. The reason that this formula does not have a proof is not because the induction rule ($\mu L$ in Figure 2) is not strong enough or that we are actually sitting inside linear logic: it is because an essential feature of inductive arguments is missing. Consider attempting a proof by induction that the property $P$ holds for all natural numbers. Besides needing to prove that $P$ holds of zero, we must also introduce an arbitrary integer $j$ (corresponding to the eigenvariables of the right premise in $\mu L$) and show that the statement $P(j+1)$ reduces to the statement $P(j)$. That is, after manipulating the formulas describing $P(j+1)$ we must be able to find in the resulting argument, formulas describing $P(j)$. Up until now, we have only “performed” formulas (by applying introduction rules) instead of checking them for equality. More specifically, while we do have a logical primitive for checking equality of terms, the proof system described so far does not have an equality for comparing formulas. As a result, some of the most basic theorems are not provable in this system. For example, there is no proof of $\forall n.({\rm Nature}~{}n\supset{\rm Nature}~{}n)$.

Model checking is not the place where we should be attempting proofs involving arbitrary infinite domains: inductive theorem provers are used for that. If we restrict to finite domains, however, proofs appear. For example, consider the less-than binary relation defined as

[TABLE]

The formula $(\forall n.\hbox{\sl lt}~{}n~{}{\bf 10}\supset\hbox{\sl lt}~{}n~{}{\bf 10})$ has a proof that involves generating all numbers less than 10 and then showing that they are, in fact, all less than 10. Similarly, a proof of the formula $\forall n\forall m\forall p(\hbox{\sl lt}~{}n~{}{\bf 10}\supset\hbox{\sl lt}~{}m~{}{\bf 10}\supset\hbox{\sl plus}~{}n~{}m~{}p\supset\hbox{\sl plus}~{}m~{}n~{}p)$ exists and consists of enumerating 100 pairs of numbers $\langle n,m\rangle$ and checking that the result of adding $n+m$ yields the same value as adding $m+n$.

The full proof system for $\mu\hbox{MALL}^{=}$ contains the cut rule and the following two initial rules.

[TABLE]

The more general instance of the initial rule can be eliminated in favor of these two specific instances.

7 Conclusions

Linear logic is usually understood as being an intensional logic whose semantic treatments are quite remote from the simple model theory consideration of first-order logic and arithmetic. Thus, we draw the possibly surprising conclusions that the proof theory of linear logic provides a suitable framework for model checking. Many of the salient features of linear logic—lack of structural rules, two conjunctions and two disjunctions, polarization—play important roles in this framework. The role of linear logic here seems completely different and removed from, say, the use of linear logic to model multiset rewriting and Petri nets [11]: we use it instead as the logic behind logic. In order to capture model checking, we need to deal with possibly unbounded behaviors in specifications. Instead of using the rule of contraction (which states, for example, that the hypothesis $B$ can be repeated as the two hypotheses $B,B$) we have used the theory of fixed points: there, unfolding replaces $\mu B\bar{t}$ with $(B(\mu B)\bar{t})$, thus copying the definition of $B$. The use of fixed points also allows for the direct and natural applications of the induction and coinduction principles. In the full version of this paper, we show how a focused proof system for $\mu\hbox{MALL}^{=}$ can be used to describe large scale (synthetic) additive inference rules that are built from smaller scale inference rules that may be multiplicative.

There can be several benefits for establishing and developing model checking within proof theory. One way to integrate theorem provers and model checkers would be to allow them to exchange proof certificates in a common language of formulas and proofs. The logic of $\mu\hbox{MALL}^{=}$ is close to the logic and proofs used in some inductive theorem provers. Also, linear logic is rich in duality. Certain techniques used in model checking topics should be expected to dualize well. For example, what is the dual notion for least fixed points of the notion of bisimulation-up-to? What does predicate abstraction look like when applied to greatest fixed points? Proof theory is a framework that supports rich abstractions, including term-level abstractions, such as bindings in terms. Thus, moving from model checking using first-order terms to using simply typed $\lambda$-terms is natural in proof theory: such proof theoretic investigations of model checking over linguistic structures including binders have been studied in [13] and have been implemented in the Bedwyr system [4] which has been applied to various model checking problems related to the $\pi$-calculus [16, 17].

Acknowledgments. We thank the reviewers of an earlier draft of this abstract for their comments. This work has been funded by the ERC Advanced Grant ProofCert.