Electronic Notes in Theoretical Computer Science 3 (1996)

URL: http://www.elsevier.nl/locate/entcs/volume3.html 15 pages

Encoding Transition Systems in Sequent Calculus: Preliminary Report

Raymond McDowell

Computer and Information Science Department, University of Pennsylvania Philadelphia, PA 19104-6389 USA

Dale Miller

Computer and Information Science Department, University of Pennsylvania Philadelphia, PA 19104-6389 USA

Catuscia Palamidessi

Dipartimento di Informatica e Scienze dell’Informazione Via Dodecaneso, 35, 16146 Genova ITALY

Abstract Linear logic has been used to specify the operational semantics of various process calculi. In this paper we explore how meta-level judgments, such as simulation and bisimulation, can be established using such encodings. In general, linear logic is too weak to derive such judgments and we focus on an extension to linear logic using definitions. We explore this extension in the context of transition systems.

1 Proof theory preliminaries

In a recent note [5], Girard extended linear logic with a notion of definitions. If certain restrictions are placed on the structure of definitions then defined concepts have left and right introduction rules that enjoy a cut-elimination theorem. Some examples of using such a definition mechanism have been given for equality reasoning [5,9], forms of program completion in logic programming [6,10], and in the GCLA language project [1].

Given that linear logic has been successful in specifying various transition systems used in concurrency theory [3,7], it is natural to ask what such a definition facility adds to specifications written in linear logic. In this paper, we show that if the specification of a transition system is made into a definition (instead of just a theory), then it is possible to go beyond operational semantics and also prove judgments such as simulation and bisimulation.

We shall assume that the reader is familiar with the two-sided sequent calculus presentation of linear logic [4]. For the purposes of this paper, we

\begin{matrix}c \\ ◯ \end{matrix}1996 Elsevier Science B. V.

McDowell, Miller & Palamidessi

need only the connectives 1, ⊤, ⊗, &, −∘, ∀, ∃. Our meta-logic is provided with simple types: the type of logical formulas, for example, is o (following [2]). Definitions will be written in the following style:

∀x̄_{1}[p_{1}(t̄_{1}) ∘− H_{1}] ⋯ ∀x̄_{n}[p_{n}(t̄_{n}) ∘− H_{n}] (n ≥ 0)

Here, we assume that the formulas H_{1}, …, H_{n} do not contain exponentials (in our case, this is immediate since we have not admitted either ! or ?), all free variables of H_{i} are free in some term of the list of terms t̄_{i}, and all variables free in some t̄_{i} are contained in the list of variables x̄_{i} (i = 1, …, n). We do not assume that the predicates p_{1}, …, p_{n} are distinct. For i = 1, …, n, the expression ∀x̄_{i}[p_{i}(t̄_{i}) ∘− H_{i}] is a clause of the definition and H_{i} is the body and p_{i}(t̄_{i}) is the head of that clause.

Definitions can be used to give both left and right introduction rules for atomic formulas. If suitable restrictions are made on these definitions (such as the above mentioned one that no modals appear in the body of definitions), then cut-elimination can be proved for the resulting logic extended with these defined non-logical constants (for a proof, see [9]). The right and left introduction rules for definitions can be given as follows (here, A is atomic, Δ is a multiset of formulas, and B is a formula).

{Δ ⟶ θH_{i} \atop Δ ⟶ A} BC, where θ is a substitution such that A is θp_{i}(t̄_{i})
{θΔ, θH_{i} ⟶ θC | θ is the mgu for A and p_{i}(t̄_{i})}

Δ, A ⟶ C DR

Specifying a set of sequents as the premise in the left introduction rule should be understood to mean that each sequent in the set is a premise of the rule. Here we name the right introduction rule for definitions as backchaining (BC), since it has that name in the logic programming literature, and we name the left introduction rule for definitions as definitional reflection (DR), following Schroeder-Heister [9]. Notice the different “quantificational” interpretation of these two rules when reading them bottom-up: BC replaces A with the body of some clause in the definition whose head matches with A, while DR replaces A with the body of all the clauses whose heads unify with A. These different quantificational aspects play an important role in our uses of DR and BC below.

If D is a definition, we write D ⊢ Δ ⟶ C to mean that Δ ⟶ C is provable using the inference rules of linear logic plus BC for clauses in D, and D ⊢ Δ ⟶ C to mean that Δ ⟶ C is provable using the inference rules of linear logic plus BC and DR for clauses in D. The first notion can be reduced to provability in linear logic directly: If D is the definition displayed above and if D̂ is the formula

∀x̄_{1}[H_{1} −∘ p_{1}(t̄_{1})] & … & ∀x̄_{n}[H_{n} −∘ p_{n}(t̄_{n})]

then D ⊢ Δ ⟶ C if and only if !D̂, Δ ⟶ C has a proof in the usual sequent calculus for linear logic. The notion of D ⊢ Δ ⟶ C cannot be so reduced to provability in linear logic. In this case, D is treated as a definition and we consider the proof system of linear logic to be extended to include left and right rules (DR and BC) for the defined predicates in D. We write D ⊢ B and D ⊢ B as abbreviations for D ⊢⟶ B and D ⊢⟶ B, respectively.

2 Linear logic presentations of two process calculi

In this section, definitions will be treated just as theories, or, so to say, logic programs. In Section 3 we will start using the inference rule of definitional reflection.

2.1 Abstract Transition Systems

The triple T = ⟨Λ, S, δ⟩ is an abstract transition system (ats) if Λ is a nonempty set of actions, S is a non-empty set of states, and δ ⊆ S × Λ × S (Λ and S are assumed to be disjoint). We write p ⟶^{a} q if ⟨p, a, q⟩ ∈ δ. If w ∈ Λ^{∗} then we write p ⟹^{w} q to mean that p makes a transition to q along a path of actions given by w. More formally, this relation is defined by induction on the length of w: thus p ⟹^{ϵ} p and if p ⟶^{a} r and r ⟹^{w} q then p ⟹^{aw} q. The ats T is finite if both Λ and S are finite; is noetherian if it contains no infinite length paths; is determinate if for every state p and every action a, the set {q | (p, a, q) ∈ δ} is either empty or a singleton. Transitions as logical formulas. Our first encoding represents states as propositional constants and actions as propositional functions of type o → o. A transition ⟨p, a, q⟩ ∈ δ is encoded as the clause

p ∘− ∃W (aW ⊗ (W −∘ q)),

which could be written equivalently as the formula ∀W ((W −∘ q) −∘ (aW −∘ p)). Let ats_{1}(δ) be the definition composed of the clauses encoding all the transitions in δ. Finally, we represent a word a_{1} ⋯ a_{m} (m ≥ 0) from Λ^{∗} as the proposition a_{1}(… (a_{m}1) …) (the empty word is thus encoded as 1).

Proposition 2.1 Let ⟨Λ, S, δ⟩ be an ats. Then ats_{1}(δ) ⊢ q, w ⟶ p if and

only if p ⟹^{w} q.

This proposition can be proved by showing that a path in an ats can faithfully match a sequence of inference rules in a proof. For example, consider proving the sequent q, a(w′) ⟶ p, where p and q denote states and a denotes an action. Up to permutations of inference rules, this proof must end with the following inference rules:

\begin{matrix}a(w′) ⟶ a(w′) & {q, w′ ⟶ r \atop q ⟶ w′ −∘ r} −∘R \\ q, a(w′) ⟶ a(w′) ⊗ (w′ −∘ r) \end{matrix} ; ⊗R ; q, a(w′) ⟶ ∃W (aW ⊗ (W −∘ r)) ; ∃R ; q, a(w′) ⟶ p ; BC

We have reduced proving q, a(w′) ⟶ p to proving q, w′ ⟶ r: this corresponds to the state transition p ⟶^{a} r. The empty path then corresponds to the proof

{q ⟶ q \atop q, 1 ⟶ q} 1L

Transitions given as a table. In this second encoding we use the primitive type σ to denote elements of S and α to denote elements of Λ. Let one: σ → α → σ → o be a predicate of three arguments denoting the one step transition relation and let the definition ats_{2}(δ) contain the clause one(p, a, q) ∘− 1 for every ⟨p, a, q⟩ ∈ δ. This definition is simple in the sense that it does not use variables or (non-trivial) bodies. We also need the following definition, named path:

∀P  [ multi(P, nil, P) ∘− 1].
∀A, P, Q, W [multi(P, A :: W, Q) ∘− ∃R(one(P, A, R) ⊗ multi(R, W, Q))].

Here, members of Λ^{∗} are represented as terms of type list(α) using nil : list(α) for the empty list and :: of type α → list(α) → list(α) for the list constructor. The following proposition should be contrasted to the proposition above; its proof is similar.

Proposition 2.2 Let ⟨Λ, S, δ⟩ be an ats. Then ats_{2}(δ), path ⊢ multi(p, w, q) if and only if p ⟹^{w} q.

2.2 CCS

We use types σ and α here for CCS [8] expressions and for actions, respectively. The combinators for CCS that we consider here (ignoring renaming and hiding for convenience) are prefixing (of type α → σ → σ), plus and parallel composition (both of type σ → σ → σ), recursion given by the μ operator (of type (σ → σ) → σ), and 0, the inactive process. The expression μ_{x}P will be used to abbreviate μ(λx.P). Also, the over-bar constructor is of type α → α. Compare the following definitions with the usual CCS transition system given in Figure 1.

∀A, P [ one(A.P, A, P) ∘− 1].
∀A, P, Q, R [ one(P | R, A, Q | R) ∘− one(P, A, Q)].
∀A, P, Q, R [ one(R | P, A, R | Q) ∘− one(P, A, Q)].
∀A, P, Q, R [ one(P + R, A, Q) ∘− one(P, A, Q)].
∀A, P, Q, R [ one(P + R, A, Q) ∘− one(R, A, Q)].
∀A, P, Q [ one(μP, A, Q) ∘− one(P (μP), A, Q)].
∀P, Q, R, S [ one(P | Q, τ, R | S) ∘− ∃A, B(comp(A, B)⊗
one(P, A, R) ⊗ one(Q, B, S))].

Let A be a finite, non-empty set of actions (assume that τ : α is not a member of A) and let ccs(A) be the definition composed of all those formulas displayed above plus all formulas of the form comp(a, ā) ∘− 1 and comp(ā, a) ∘− 1 for every a ∈ A.

\begin{matrix}A.P ⟶^{A} P & {P ⟶^{A} Q \atop P | R ⟶^{A} Q | R} & {P ⟶^{A} Q \atop R | P ⟶^{A} R | Q} & \begin{matrix}P ⟶^{A} R & Q ⟶^{Ā} S \\ P | Q ⟶^{τ} R | S \end{matrix} \\ {P ⟶^{A} Q \atop P + R ⟶^{A} Q} & {R ⟶^{A} Q \atop P + R ⟶^{A} Q} & {P [fix(X = P)/X] ⟶^{A} Q \atop fix(X = P) ⟶^{A} Q} \end{matrix}

Fig. 1. CCS transition rules

Proposition 2.3 Let A be a finite set of actions. Then p ⟶^{a} q if and only if ccs(A) ⊢ one(p, a, q), and p ⟹^{w} q if and only if ccs(A), path ⊢ multi(p, w, q).

CCS can be seen as an abstract transition system where Λ = A ∪ Ā ∪ {τ} and S is the set of all expressions denoting CCS expressions (of type σ). A finite CCS process is a CCS process that does not contain μ. If S is instead the set of all finite CCS processes, then the resulting ats is noetherian. Also the judgment p ⟶^{a} q is decidable when p is a finite process.

3 Simulation and bisimulations for finite behaviors

A relation R is a simulation between p and q (notation pRq, to be read as “q simulates p”) if and only if for every transition p ⟶^{a} p′, there exists a transition q ⟶^{a} q′, such that p′Rq′. The largest such relation is written ⊑; that is, p ⊑ q if and only if there exists a simulation R such that pRq. A relation R is a bisimulation between p and q if and only if for every transition p ⟶^{a} p′, there exists a transition q ⟶^{a} q′ such that p′Rq′, and for every transition q ⟶^{a} q′, there exists a transition p ⟶^{a} p′ such that q′Rp′. The largest such relation is called the bisimulation equivalence and is denoted by ≡; that is, p ≡ q (read as “p is bisimilar to q”) if and only if there exists a bisimulation R such that pRq.

Given a finite ats M = ⟨Λ, S, δ⟩, define ⟨⟨p⟩⟩ = {(a, q) | (p, a, q) ∈ δ}. Now consider a proof of the sequent p ⟶ q using the definition ats_{1}(δ). If p and q are the same state then this sequent is initial. Otherwise, the only inference rules that can be applied to prove such a sequent are either BC or DR. It is easy to show that occurrences of DR can be permuted down over BC and the right introduction rules for ∃ and ⊗. So we can assume that the last inference rule used to prove this sequent is DR, and thus the proof has the form

{∃W (a_{1}W ⊗ (W −∘ p_{1})) ⟶ q … ∃W (a_{m}W ⊗ (W −∘ p_{m})) ⟶ q \atop p ⟶ q} DR,

where m ≥ 0 and ⟨⟨p⟩⟩ = {(a_{1}, p_{1}), …, (a_{m}, p_{m})}. Because of the presence of enough permutations, each of the premises here can be proved by left introduction rules for ∃ and ⊗, yielding the premises

a_{1}w_{1}, w_{1} −∘ p_{1} ⟶ q … a_{m}w_{m}, w_{m} −∘ p_{m} ⟶ q,

where w_{1}, …, w_{m} are variables. At this point, these sequents can only be proved by using BC. For example,

a_{i}w_{i}, w_{i} −∘ p_{i} ⟶ ∃W (a_{j}W ⊗ (W −∘ q_{j})),

where ⟨a_{j}, q_{j}⟩ ∈ ⟨⟨q⟩⟩. This proof will be successful only if i = j and ∃W is instantiated with w_{i} (using the ∃ right introduction rule). Thus, the above sequents would then become

a_{1}w_{1}, w_{1}−∘p_{1} ⟶ a_{1}w_{1}⊗(w_{1}−∘q_{1}) … a_{m}w_{m}, w_{m}−∘p_{m} ⟶ a_{m}w_{m}⊗(w_{m}−∘q_{m}).

Finally, using the right introduction rules for ⊗ and −∘ and the left introduction rule for −∘, these sequents reduce to

p_{1} ⟶ q_{1} … p_{m} ⟶ q_{m}.

Since these proof steps are forced, these several inference rules can be arranged into the following derived rule of inference

{p_{1} ⟶ q_{1} … p_{m} ⟶ q_{m} \atop p ⟶ q} SIM^{1}

provided that m ≥ 0, {(a_{1}, p_{1}), …, (a_{m}, p_{m})} = ⟨⟨p⟩⟩, and

{(a_{1}, q_{1}), …, (a_{m}, q_{m})} ⊆ ⟨⟨q⟩⟩.

Let _{SIM_{1}} ⊢ p ⟶ q denote the proposition that the sequent p ⟶ q can be proved using only the SIM_{1} inference rule (again, for the noetherian case; for the non-noetherian case, see Section 4). We have now provided the proof outline of the following proposition.

Proposition 3.1 Let ⟨Λ, S, δ⟩ be a finite, noetherian ats and let p, q ∈ S. Then ats_{1}(δ) ⊢ p ⟶ q if and only if _{SIM_{1}} ⊢ p ⟶ q.

Notice that in the SIM_{1} proof system, we do not need instances of the initial sequent rule: a proof of p ⟶ p using only the SIM_{1} rule is always possible for a noetherian ats. This observation is similar to the one that holds of most proof systems: the initial rule is needed to prove A ⟶ A only when A is atomic; that is, when A has a non-logical symbol as its head symbol. When using ats_{1}(δ), states become logical constants, in a sense, and, hence, we do not need any instance of the initial rule. We can now establish our first proof theoretic connection to simulation.

Proposition 3.2 Let ⟨Λ, S, δ⟩ be a finite, noetherian ats and let p, q ∈ S. Then ats_{1}(δ) ⊢ p ⟶ q if and only if q simulates p.

Proof Given Proposition 3.1, we need only show that _{SIM_{1}} ⊢ p ⟶ q if and only if q simulates p. First, assume that the sequent p ⟶ q has a proof that contains only the SIM_{1} inference rule. Let R be the set of all pairs ⟨r, s⟩ such that the sequent r ⟶ s has an occurrence in that proof. It is an easy matter to verify that R is a simulation.

Conversely, assume that q simulates p. Thus there is a simulation R such that pRq. We construct a proof tree which has the property that, for every sequent r ⟶ s in the proof, rRs. We begin with a single node labeled with the sequent p ⟶ q. We then repeat the following as long as there is a sequent r ⟶ s in the tree that is not the conclusion of an inference rule. By construction, rRs, so R contains pairs ⟨r_{1}, s_{1}⟩, …, ⟨r_{m}, s_{m}⟩, where {(a_{1}, r_{1}), …, (a_{m}, r_{m})} = ⟨⟨r⟩⟩ and {(a_{1}, s_{1}), …, (a_{m}, s_{m})} ⊆ ⟨⟨s⟩⟩ for some actions a_{1}, …, a_{m} (m ≥ 0). Now the sequent r ⟶ s can be placed at the conclusion of a SIM_{1} rule, whose premises are r_{1} ⟶ s_{1}, …, r_{m} ⟶ s_{m}. This process terminates since the given ats is noetherian and has a bound on the length of its paths.

A consequence of this theorem is that logical equivalence of two processes, namely (p −∘ q) & (q −∘ p), which is the finest equivalence relation definable using logic, is “two-way simulation”. Logical equivalence, however, is courser than bisimulation, as the following example shows.

Example 3.3 Consider the transition system with one label a, states {p_{1}, p_{2},

p_{3}, p_{4}, q_{1}, q_{2}, q_{3}}, and transitions p_{1} ⟶^{a} p_{2}, p_{2} ⟶^{a} p_{3}, p_{1} ⟶^{a} p_{4}, q_{1} ⟶^{a} q_{2},

q_{2} ⟶^{a} q_{3}. The relations

{⟨p_{1}, q_{1}⟩, ⟨p_{2}, q_{2}⟩, ⟨p_{3}, q_{3}⟩, ⟨p_{4}, q_{2}⟩} and {⟨q_{1}, p_{1}⟩, ⟨q_{2}, p_{2}⟩, ⟨q_{3}, p_{3}⟩}

witness the fact that q_{1} simulates p_{1} and p_{1} simulates q_{1}, respectively. It is easy to check, however, that there is no bisimulation that contains the pair ⟨p_{1}, q_{1}⟩.

Using the encoding ats_{1}(δ), simulation can be identified with the logical connective −∘. As a consequence of this example, bisimulation cannot in general be a logical connective: that is, it cannot be a predicate (of type o → o → o) with left and right introduction rules that enjoy cut-elimination. However, if we consider an ats that is also determinate then p ⊑ q and q ⊑ p imply p ≡ q, so logical equivalence and bisimulation coincide.

Proposition 3.4 Let ⟨Λ, S, δ⟩ be a finite, noetherian, and determinate ats and let p, q ∈ S. Then ats_{1}(δ) ⊢ (p −∘ q) & (q −∘ p) if and only if p is bisimilar to q.

If we switch representations of transitions systems to use the definition ats_{2}(δ), then it is possible to characterize simulation and bisimulation as predicates sim and bisim given by the following definition, named sims.

∀P, Q [sim(P, Q) ∘− ∀A∀P′. one(P, A, P′)−∘

∃Q′. one(Q, A, Q′) ⊗ sim(P′, Q′)]

∀P, Q [bisim(P, Q) ∘− [∀A∀P′. one(P, A, P′)−∘

∃Q′. one(Q, A, Q′) ⊗ bisim(P′, Q′)] &

[∀A∀Q′. one(Q, A, Q′)−∘
∃P′. one(P, A, P′) ⊗ bisim(Q′, P′)]].

We introduce an inference rule similar to the SIM_{1} given above, namely

⟶ sim(p_{1}, q_{1}) … ⟶ sim(p_{m}, q_{m})

⟶ sim(p, q) SIM_{2}

provided that m ≥ 0,

{(a_{1}, p_{1}), …, (a_{m}, p_{m})} = ⟨⟨p⟩⟩, and {(a_{1}, q_{1}), …, (a_{m}, q_{m})} ⊆ ⟨⟨q⟩⟩.

We also present an inference rule BISIM_{2} for bisimulation:

⟶ bisim(p_{1}, q_{1}) ⟶ bisim(q_{1}, p_{1}) … ⟶ bisim(p_{m}, q_{m}) ⟶ bisim(q_{m}, p_{m}) ⟶ bisim(p, q)

where m ≥ 0,

{(a_{1}, p_{1}), …, (a_{m}, p_{m})} = ⟨⟨p⟩⟩, and {(a_{1}, q_{1}), …, (a_{m}, q_{m})} = ⟨⟨q⟩⟩.

Let _{SIM_{2}} ⊢ Δ ⟶ C (respectively, _{BISIM_{2}} ⊢ Δ ⟶ C) denote the proposition that the sequent Δ ⟶ C can be proved using only the SIM_{2} (respectively, BISIM_{2}) inference rule.

Proposition 3.5 Let ⟨Λ, S, δ⟩ be a finite, noetherian ats and let p, q ∈ S. Then

• ats_{2}(δ), sims ⊢ sim(p, q) if and only if _{SIM_{2}} ⊢ sim(p, q), and

• ats_{2}(δ), sims ⊢ bisim(p, q) if and only if _{BISIM_{2}} ⊢ bisim(p, q).

Proof We outline the proof of the first case; the second can be done similarly. Consider a proof of the sequent ⟶ sim(p, q). This is provable only by a BC rule using sims, and thus the sequents

⟶ ∀A∀P′. one(p, A, P′) −∘ ∃Q′. one(q, A, Q′) ⊗ sim(P′, Q′)

and

one(p, A, P′) ⟶ ∃Q′. one(q, A, Q′) ⊗ sim(P′, Q′)

must be provable. If this latter sequent is provable, there is a proof of it ending with DR, and thus the sequents

⟶ ∃Q′. one(q, a_{1}, Q′)⊗sim(p_{1}, Q′) … ⟶ ∃Q′. one(q, a_{m}, Q′)⊗sim(p_{m}, Q′)

must be provable, where ⟨⟨p⟩⟩ = {(a_{1}, p_{1}), …, (a_{m}, p_{m})}. Each of these sequents is provable only if each of the ∃Q′ is instantiated with q_{i} where (a_{i}, q_{i}) ∈ ⟨⟨q⟩⟩, for i = 1, …, m. Thus, these sequents are provable only if the sequents

⟶ sim(p_{1}, q_{1}) … ⟶ sim(p_{m}, q_{m})

are provable.

Now the following can be proved using Proposition 3.5 in a manner analogous to the proof of Proposition 3.2 using Proposition 3.1.

Proposition 3.6 Let ⟨Λ, S, δ⟩ be a finite, noetherian ats, and let p and q be members of S. Then

• ats_{2}(δ), sims ⊢ sim(p, q) if and only if p ⊑ q, and

• ats_{2}(δ), sims ⊢ bisim(p, q) if and only if p ≡ q.

The following proposition can be proved similarly to the preceding proposition, although it is a bit more involved, owing to the fact that the definition of one-step transitions in CCS is given by recursion. Notice that CCS over a finite set of actions and restricted to finite processes is not a finite ats.

Proposition 3.7 The following equivalences hold for finite processes p and q of CCS.

• ccs(A), sims ⊢ sim(p, q) if and only if p ⊑ q.

• ccs(A), sims ⊢ bisim(p, q) if and only if p ≡ q.

4 Non-finite behavior cases

In the previous section we have expressed simulation and bisimulation in logic using recursive definitions of the form

∀P_{1} … ∀P_{n}[r(P_{1}, …, P_{n}) ∘− Φ], (1)

where the formula Φ contained the predicate r and free occurrences of the variables P_{1}, …, P_{n}. To this clause we associate a function ϕ from n-ary relations to n-ary relations defined as: ϕ(R) is the set of all tuples of terms ⟨t^{1}, …, t^{n}⟩ such that there is a set {⟨t_{1}^{1}, …, t_{1}^{n}⟩, …, ⟨t_{m}^{1}, …, t_{m}^{n}⟩} ⊆ R (m ≥ 0) and

ats_{2}(δ) ⊢ r(t_{1}^{1}, …, t_{1}^{n}) & … & r(t_{m}^{1}, …, t_{m}^{n}) ⟶ Φ[t^{1}/P_{1}, …, t^{n}/P_{n}].

To see that definitional reflection on (1) is sound for all the relations which are fixed points of ϕ, assume that for any relation r there is only one such definition (in case there are more, we group them in one definition which has as body the disjunction of the bodies). Then observe that the use of definitional reflection corresponds to reversing the implication in the definition, that is, to assuming the formula ∀P_{1} … ∀P_{n}[r(P_{1}, …, P_{n}) −∘ Φ].

Let Φ_{s} and Φ_{b} be the bodies of the definitions given in sims for sim and bisim, respectively, and consider the corresponding functions ϕ_{s} and ϕ_{b} on binary relations associated with these formulas. We can see from their definitions that ⊑ and ≡ are the greatest fixed points of ϕ_{s} and ϕ_{b}, respectively. Note that in proofs of ⟶ sim(p, q) and ⟶ bisim(p, q) using definitions ats_{2}(δ) and sims, DR is used with ats_{2}(δ) but not with sims. Backchaining on (1) is all that we need to prove the sequent ⟶ r(p_{1}, …, p_{n}) whenever p_{1}, …, p_{n} are related in the least fixed point of the function ϕ.

As the following example shows, when the transition system is not noetherian, the “if parts” of Proposition 3.6 may not hold.

Example 4.1 Consider a transition system with two states only, p and q, and two transitions p ⟶^{a} p and q ⟶^{a} q. Then p ⊑ q holds, but sim(p, q) cannot be proved. Note that the attempt to prove it would end up in a circularity.

In fact, both backchaining and definitional reflection on (1) are sound for all the relations which are fixed points of ϕ. If ats_{2}(δ), sims ⊢ r(p_{1}, …, p_{n}) holds then p_{1}, …, p_{n} must be related by every fixed point of ϕ, and thus by its least fixed point. In a noetherian ats, ϕ_{s} and ϕ_{b} each have unique fixed points, and this is why ⊑ and ≡ can be completely characterized in a noetherian ats by provability (Proposition 3.6).

One attempt to characterize the greatest fixed point of the relation transformer ϕ proof-theoretically is to introduce a notion of “finite or infinite proof”. An ω-proof of the sequent Δ ⟶ C with inference rules taken from the set L is a tree whose root is labeled by Δ ⟶ C, and such that for every node N there is an instance of an inference rule of L whose conclusion is the label of N, and whose premises are the labels of the children of N. We will denote by L ⊢_{ω} Δ ⟶ C the existence of an ω-proof in L for Δ ⟶ C. For example, SIM_{2} ⊢_{ω} Δ ⟶ C is true if Δ ⟶ C has an ω-proof using only SIM_{2}. If the set of inference rules L is determined by those in linear logic and those arising from using some definition, say D, then we write D ⊢_{ω} Δ ⟶ C. Notice that an ω-proof can have bounded or unbounded height. We now prove two propositions using ω-proofs that generalize Propositions 3.5 and 3.6 by dropping the noetherian condition.

Proposition 4.2 Let ⟨Λ, S, δ⟩ be a finite ats and let p, q ∈ S. Then

• ats_{2}(δ), sims ⊢_{ω} sim(p, q) if and only if _{SIM_{2}} ⊢_{ω} sim(p, q), and

• ats_{2}(δ), sims ⊢_{ω} bisim(p, q) if and only if _{BISIM_{2}} ⊢_{ω} bisim(p, q).

Proof We outline the proof of the first case; the second can be done similarly. Since the converse is immediate, we only show the forward direction. Assume that the sequent ⟶ sim(p, q) has an ω-proof using the definitions ats_{2}(δ). Since this sequent must be proved by one use of BC, two uses of ∀R, and one use of −∘R, we have

ats_{2}(δ) ⊢_{ω} one(p, A, P′) ⟶ ∃q′[one(q, A, q′) ⊗ sim(P′, q′)],

where A and P′ are variables. At this point, the proof can proceed by either DR or ∃R. If the choice is DR, then we quickly get that the proof is essentially an instance of SIM_{2} at the root, and we proceed recursively through the ωproof. Otherwise, a use of ∃R would give raise to a tensor, the first component of which is one(q, A, q_{0}) for some particular q_{0} ∈ S. It is not possible, however, to prove this atom using BC since no instance of a clause in the definition ats_{1}(δ) has the variable A in its head. Thus, this proof could not be built in that fashion.

Proposition 4.3 Let ⟨Λ, S, δ⟩ be a finite ats. Then p ⊑ q if and only if ats_{2}(δ), sims ⊢_{ω} sim(p, q), and p ≡ q if and only if ats_{2}(δ), sims ⊢_{ω} bisim(p, q).

Proof We prove only the first equivalence since the second follows similarly. First, assume that

ats_{2}(δ), sims ⊢_{ω} sim(p, q).

By the preceding Proposition, _{SIM_{2}} ⊢_{ω} sim(p, q). We now proceed as in the proof of Proposition 3.2: Let Ξ be a proof of ⟶ sim(p, q) that contains just the SIM_{2} inference rule and let R be the binary relation such that rRs if r ⟶ s has an occurrence in Ξ. It is easy to see that R is a simulation containing ⟨p, q⟩.

Assume next that p ⊑ q holds. We can construct a sequence of trees {T_{k}}_{k∈ω} such that for every k, the root of T_{k} is labeled by ⟶ sim(p, q), all the leaves of T_{k} are labeled by sequents of the form sim(p′, q′) where p′ ⊑ q′ holds, and T_{k} is a subtree of T_{k+1}. The construction process for such trees follows the same pattern as used in the proof of Proposition 3.2.

For these equivalences to hold, it is important that the ats is finite. If we consider a non-finite ats, say, ccs(A) (A is finite), then the reverse direction of these equivalences does not necessarily hold, as the following example illustrates.

Example 4.4 The CCS terms μ_{x}x and μ_{x}a.x are such that μ_{x}a.x ⊑ μ_{x}x does not hold. However, both the judgments ccs(A) ⊢_{ω} one(μ_{x}x, a, μ_{x}a.x), and ccs(A), sims ⊢_{ω} sim(μ_{x}a.x, μ_{x}x) hold.

In a sense, the infinite proof of one(μ_{x}x, a, μ_{x}a.x) is an “infinite failure”. If we restrict to finite CCS processes, then such infinite failures do not occur with respect to the one step transition steps and the only infinite proof behaviors will be those that positively verify the greatest fixed point properties of simulation and bisimulation. Thus, when restricted to finite CCS processes, the generalization of Proposition 4.3 where ats_{2}(δ) is replaced with ccs(A) holds.

5 Properties about defined relations

In previous sections we have shown how to encode in sequent calculus various relations over the states of a transition system. We now explore the kinds of properties on the relations that can be proved within the calculus or via some characterization provided by the calculus.

Example 5.1 The property “bisimulation is preserved by the prefix operator” holds in CCS. The corresponding encoding of this property is also provable in the sequent calculus; that is, we have

ccs(A), sims ⊢ ∀P ∀Q[bisim(P, Q) −∘ bisim(A.P, A.Q)],

a proof of which is easy to construct. The property “bisimulation is symmetric” holds in any transition system. The corresponding encoding of this property is also provable in the sequent calculus; that is, we have

ats_{2}(δ), sims ⊢ ∀P ∀Q[bisim(P, Q) −∘ bisim(Q, P)],

which is also easy to verify.

However, as the following examples illustrate, there are plenty of true properties of ≡ and ⊑ that cannot be proved within the logic. One reason for this lack is, intuitively, we can prove properties of sim and bisim only if they are true for every fixed point of ϕ_{s} and ϕ_{b}, but in the non-noetherian case, there is in general more than one fixed point.

Example 5.2 The property “bisimulation equivalence implies the largest simulation” (or more formally: ≡ is a subset of ⊑) is true in any transition system. This property can be expressed by the formula ∀P ∀Q[bisim(P, Q) −∘ sim(P, Q)] but, in general, if δ is a non-noetherian transition relation, this formula cannot be proved using the definitions ats_{2}(δ) and sims. For example, if we take the transition system ⟨{a}, {p}, {⟨p, a, p⟩}⟩ it is immediate to see that {⟨p, p⟩} is a bisimulation (the greatest fixed point of ϕ_{b}, namely bisimulation equivalence) and ∅ is a simulation (the least fixed point of ϕ_{s}). Hence, this formula cannot be proved for this transition system.

Example 5.3 The property “bisimulation equivalence is reflexive” holds in any transition system. The formula ∀P [bisim(P, P)] cannot be proved using the definitions ats_{2}(δ) and sims. Consider for instance the same transition system as in Example 5.2: the empty set ∅ is a bisimulation (the least fixed point of ϕ_{b}), and it is, of course, not reflexive.

Example 5.4 The property “bisimulation equivalence is preserved by the + operator” is true in CCS. This property can be expressed as the formula ∀P ∀Q∀R[bisim(P, Q)−∘bisim(P +R, Q+R))]. This sequent cannot be proved using ccs(A) and sims. In fact, take P = a.0, Q = a.0 + a.0 and R = μ_{x}a.x. The least fixed point of ϕ_{b} contains the pair ⟨a.0, a.0 + a.0⟩ but not the pair ⟨a.0 + μ_{x}a.x, a.0 + a.0 + μ_{x}a.x⟩.

The notion of “infinite proof”, introduced in the previous section, can be helpful to prove properties on the defined relations at the meta (mathematical) level. For instance, the properties of Examples 5.2 and 5.3 can both be proved by using the characterization of ≡ and ⊑ provided at the end of the previous section. It is easy to see, in fact, that ccs(A), sims ⊢_{ω} bisim(P, P). Concerning the implication bisim(P, Q) −∘ sim(P, Q), observe that any infinite proof for ⟶ bisim(P, Q) contains an infinite proof of ⟶ sim(P, Q).

The characterization of simulation or bisimulation using ω-proofs is not so helpful because the existence of an infinite proof for a given sequent is cosemidecidable but (in general) not semidecidable. A better approach would be to use co-induction: it is well known that, for finitely-branching transition systems, ϕ_{s} and ϕ_{b} are downward-continuous. Thus their greatest fixed point can be characterized as ⋂_{k} ϕ_{s}^{k}(S × S) and ⋂_{k} ϕ_{b}^{k}(S × S) respectively. We could then encode ⊑ and ≡ by using stratified versions of sim and bisim: Figure 2 contains just such a definition, which will be named ssims.

In order to encode co-induction, we can use inductions on natural numbers. We incorporate induction by introducing natural numbers using z for zero and s for successor and using the predicate nat. We introduce now the following “introduction” rules for this new predicate.

⟶ nat z

Δ ⟶ nat x
Δ ⟶ nat (sx)

Δ_{1} ⟶ Qz Qy ⟶ Q(sy) Δ_{2}, Qx ⟶ P Δ_{1}, Δ_{2}, nat x ⟶ P

Here, x, P, and Q are schematic variables of these inference rule, and y is a variable not free in Q. The first two rules can be seen as right-introduction rules for nat while the third rule, encoding induction over natural numbers, can

sim(P, Q) ∘− ∀K (nat K −∘ ssim(K, P, Q)).
ssim(z, P, Q) ∘− 1
ssim((sK), P, Q) ∘− [∀A∀P′. one(P, A, P′) −∘
∃Q′. one(Q, A, Q′) ⊗ ssim(K, P′, Q′)].
bisim(P, Q) ∘− ∀K (nat K −∘ sbisim(K, P, Q)).
sbisim(z, P, Q) ∘− 1.
sbisim((sK), P, Q) ∘− [∀A∀P′. one(P, A, P′) −∘
∃Q′. one(Q, A, Q′) ⊗ sbisim(K, P′, Q′)] &

[∀A∀Q′. one(Q, A, Q′) −∘

∃P′. one(P, A, P′) ⊗ sbisim(K, Q′, P′)].

Fig. 2. Stratified simulation and bisimulation definitions. Free variables are assumed to be universally quantified.

be seen as a left-introduction rule. In the left-introduction rule, Q ranges over formulas with one variable extracted (say, using λ-abstraction) and represents the property that is proved by induction: the third premise of that inference rule witnesses the fact that, in general, Q will express a property stronger than P. Notice that with this formulation of induction, cut-free proofs will not have the subformula property.

The following inference rules can be derived from these rules for nat.

Δ ⟶ Qz Qy ⟶ Q(sy) Δ, nat n ⟶ Qn Δ ⟶ C Δ, nat n ⟶ C Δ, nat n, nat n ⟶ C

Δ, nat n ⟶ C

The fact that a nat-atom can be weakened and contracted on the left follows from observation that it is possible to prove ∀n(nat n −∘ ! nat n) using our induction principle.

We can now prove properties of maximal simulation or bisimulation equivalence even if they are not valid for all fixed points of ϕ_{s} or ϕ_{b}; the only necessary condition is that they are valid on ⋂_{k} ϕ_{s}^{k}(S × S) or ⋂_{k} ϕ_{b}^{k}(S × S) . Of course, this encoding of ⊑ and ≡ as sim and bisim is sound only when ϕ_{s} and ϕ_{b} are downward-continuous; in general this is true when the transition system is finitely branching. In CCS, for instance, this condition is guaranteed whenever all the recursion variables in μ-expressions are prefixed.

It is now possible to prove, for instance, reflexivity of bisimulation equivalence, and bisimilarity of nodes involved in cyclic transitions. In particular, we can prove all of the following formulas using natural number induction and definitional reflection with the definitions ccs(A) and ssims.

bisim(μ_{x} a.x, μ_{x} (a.x + a.x)) ∀P bisim(P, P)
∀P bisim(P + 0, P) ∀P bisim(P + P, P)
∀P, Q (bisim(P, Q)) −∘ sim(P, Q))
∀P, Q, R (bisim(P, Q) −∘ bisim(P + R, Q + R))

We are continuing to consider the use of induction along with definitions to capture judgments about properties such as bisimulation.

6 Conclusion

It has been observed before and in this paper that linear logic can be used to specify transition systems. We have shown that if linear logic is extended with definitions, then certain properties about elements of transition systems, namely simulation and bisimulation, can be captured naturally. Furthermore, if induction over integers is added, then we can increase the expressiveness of logic to establish more high-level facts about these properties, such as the fact that bisimulation is an equivalence.

From a high-level point-of-view, we can characterize the experiments we have reported here in two ways. From a (traditional) logic programming point of view, a definition D is generally either a set of (positive) Horn clauses or an extension of them that allows negated atoms in the body of clauses. In that case, sequents in a proof of D ⊢ A, for atomic formula A, are either of the form ⟶ B or B ⟶. In the first case, backchaining is used to establish B and, in the second case, definition reflection is used to build a finite refutation of B. In this paper, we consider richer definitions so that the search for proofs must consider sequents of the form B ⟶ C; with such sequents, backchaining and definition reflection are used together. From a computational or concurrency point-of-view, proofs using just backchaining only capture the may behavior of a system: “there exists a computation such that …” is easily translated to “there exists a proof (in the sense of ⊢) of …”. The addition of the definitional reflection inference rules allows certain forms of must behavior to be captured.

Acknowledgments.

We would like to thank Robert Stärk for several helpful discussions and Chuck Liang for providing us with a prototype in λProlog of an interactive theorem prover for doing many of the formal (object-logic) proofs described in this paper. The authors have been funded in part by ONR N00014-93-1-1324, NSF CCR-92-09224, NSF CCR-94-00907, and ARO DAAH04-95-1-0092. Part of this work was done while Palamidessi was visiting the University of Pennsylvania and while Miller was visiting the University of Genova. We both wish to thank these institutions for their hospitality in hosting us.

References

[1] M. Aronsson, L.-H. Eriksson, A. Gäredal, L. Halnäs, and P. Olin. GCLA: a definitional approach to logic programming. New Generation Computing, 4:381–404, 1990.

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

[3] Vijay Gehlot and Carl Gunter. Normal process representatives. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 200–207, Philadelphia, Pennsylvania, June 1990. IEEE Computer Society Press.

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

[5] Jean-Yves Girard. A fixpoint theorem in linear logic. A message posted on the linear@cs.stanford.edu mailing listing, http://www.csl.sri.com/linear/

mailing-list-traffic/www/07/mail_3.html, February 1992.

[6] Lars Hallnäs and Peter Schroeder-Heister. A proof-theoretic approach to logic programming. ii. Programs as definitions. Journal of Logic and Computation, pages 635–660, October 1991.

[7] Dale Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242–265. Springer-Verlag, 1993.

[8] Robin Milner. Communication and Concurrency. Prentice-Hall International, 1989.

[9] Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Eighth Annual Symposium on Logic in Computer Science, pages 222–232. IEEE, June 1993.

[10] Robert Stärk. A complete axiomatization of the three-valued completion of logic programs. Journal of Logic and Computation, 1(6):811–834, 1991.