Modal Logics for Nominal Transition Systems

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, Tjark Weber
Uppsala University
Sweden
Abstract

We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.

License CC-BY.

1 Introduction

Transition systems

Transition systems are ubiquitous in models of computing, and specifications to say what may and must happen during executions are often formulated in a modal logic. There is a plethora of different versions of both transition systems and logics, including a variety of higher-level constructs such as updatable data structures, new name generation, alias generation, dynamic topologies for parallel components etc. In this paper we formulate a general framework where such aspects can be treated uniformly, and define accompanying modal logics which are adequate for bisimulation. This is related to, but independent of, our earlier work on psi-calculi [5], which proposes a particular syntax for defining behaviours. The present paper does not depend on any such language, and provides general results for a large class of transition systems.

In any transition system there is a set of states P,Q, representing the configurations a system can reach, and a relation telling how a computation can move between them. Many formalisms, for example all process algebras, define languages for expressing states, but in the present paper we shall make no assumptions about any such syntax.

In systems describing communicating parallel processes the transitions are labelled with actions α,β, representing the externally observable effect of the transition. A transition P𝛼P thus says that in state P the execution can progress to P while conducting the action α, which is visible to the rest of the world. For example, in CCS these actions are atomic and partitioned into output and input communications. In value-passing calculi the actions can be more complicated, consisting of a channel designation and a value from some data structure to be sent along that channel.

Scope openings

With the advent of the pi-calculus [20] an important aspect of transitions was introduced: that of name generation and scope opening. The main idea is that names (i.e., atomic identifiers) can be scoped to represent local resources. They can also be transmitted in actions, to give a parallel entity access to this resource. In the monadic pi-calculus such an action is written a¯(νb), to mean that the local name b is exported along the channel a. These names can be subjected to alpha-conversion: if Pa¯(νb)P and c is a fresh name then also Pa¯(νc)P{c/b}, where P{c/b} is P with all bs replaced by cs. Making this idea fully formal is not entirely trivial and many papers gloss over it. In the polyadic pi-calculus several names can be exported in one action, and in psi-calculi arbitrary data structures may contain local names. In this paper we make no assumptions about how actions are expressed, and just assume that for any action α there is a finite set of names 𝖻𝗇(α), the binding names, representing exported names. In our formalization we use nominal sets, an attractive theory to reason about objects depending on names on a high level and in a fully rigorous way.

State predicates

The final general components of our transition systems are the state predicates ranged over by φ, representing what can be concluded in a given state. For example state predicates can be equality tests of expressions, or connectivity between communication channels. We write Pφ to mean that in state P the state predicate φ holds.

A structure with states, transitions, and state predicates as discussed above we call a nominal transition system.

Hennessy-Milner Logic

Modal logic has been used since the 1970s to describe how facts evolve through computation. We use the popular and general branching time logic known as Hennessy-Milner Logic [17] (HML). Here the idea is that an action modality α expresses a possibility to perform an action α. If A is a formula then αA says that it is possible to perform α and reach a state where A holds. With conjunction and negation this gives a powerful logic shown to be adequate for bisimulation equivalence: two processes satisfy the same formulas exactly if they are bisimilar. In the general case, conjunction must take an infinite number of operands when the transition systems have states with an infinite number of outgoing transitions. The fully formal treatment of this requires care in ensuring that such infinite conjunctions do not exhaust all names, leaving none available for alpha-conversion. All previous works that have considered this issue properly have used uniformly bounded conjunction, i.e., the set of all names in all conjuncts is finite.

Contributions

Our definition of nominal transition systems is very general since we leave open what the states, transitions and predicates are. The only requirement is that transitions satisfy alpha-conversion. A technically important point is that we do not assume the usual name preservation principle, that if P𝛼P then the names occurring in P must be a subset of those occurring in P and α. This means that the results are applicable to a wide range of calculi. For example, the pi-calculus represents a trivial instance where there are no state predicates. CCS represent an even more trivial instance where 𝖻𝗇 always returns the empty set. In the fusion calculus and the applied pi-calculus the state contains an environmental part which tells what expressions are equal to what. In the general framework of psi-calculi the states are processes with assertions describing their environments.

We define a modal logic with the α operator that binds the names in 𝖻𝗇(α), and contains operators for state predicates. In this way we get a logic for an arbitrary nominal transition system such that logical equivalence coincides with bisimilarity. We also show how variants of the logic correspond to late, open and hyperbisimilarity in a uniform way. The main technical difficulty is to ensure that formulas and their alpha-equivalence classes throughout are finitely supported, i.e., only depend on a finite set of names, even in the presence of infinite conjunction. Instead of uniformly bounded conjunction we use the notion of finite support from nominal sets. This results in greater generality and expressiveness. For example, we can now define quantifiers and the next step modalities as derived operators.

Formalization

Our main definitions and theorems have been formalized in Nominal Isabelle [29]. This has required significant new ideas to represent data types with infinitary constructors like infinite conjunction and their alpha-equivalence classes. As a result we corrected several details in our formulations and proofs, and now have very high confidence in their correctness. The formalization effort has been substantial, but certainly less than half of the total effort, and we consider it a very worthwhile investment.

Exposition

In the following section we provide the necessary background on nominal sets. In Section 3 we present our main definitions and results on nominal transition systems and modal logics. In Section 4 we derive useful operators such as quantifiers and fixpoints, and indicate some practical uses. Section 5 shows how to treat variants of bisimilarity such as late and open in a uniform way, and in Section 6 we compare with related work and demonstrate how our framework can be applied to recover earlier results uniformly. Finally Section 7 concludes with some remarks on the formalization in Nominal Isabelle. All full proofs are contained in the appendix of the technical report [24].

2 Background on nominal sets

Nominal sets [27] is a general theory of objects which depend on names, and in particular formulates the notion of alpha-equivalence when names can be bound. The reader need not know nominal set theory to follow this paper, but some key definitions will make it easier to appreciate our work and we recapitulate them here.

We assume an infinitely countable multi-sorted set of atomic identifiers or names 𝒩 ranged over by a,b,. A permutation is a bijection on names that leaves all but finitely many names invariant. The singleton permutation which swaps names a and b and has no other effect is written (ab), and the identity permutation that swaps nothing is written id. Permutations are ranged over by π,π. The effect of applying a permutation π to an object X is written πX. Formally, the permutation action can be any operation that satisfies idX=X and π(πX)=(ππ)X, but a reader may comfortably think of πX as the object obtained by permuting all names in X according to π.

A set of names N supports an object X if for all π that leave all members of N invariant it holds πX=X. In other words, if N supports X then names outside N do not matter to X. If a finite set supports X then there is a unique minimal set supporting X, called the support of X, written 𝗌𝗎𝗉𝗉(X), intuitively consisting of exactly the names that matter to X. As an example the set of names textually occurring in a datatype element is the support of that element, and the set of free names is the support of the alpha-equivalence class of the element. Note that in general, the support of a set is not the same as the union of the support of its members. An example is the set of all names; each element has itself as support, but the whole set has empty support since π𝒩=𝒩 for any π.

We write a#X, pronounced “a is fresh for X”, for a𝗌𝗎𝗉𝗉(X). The intuition is that if a#X then X does not depend on a in the sense that a can be replaced with any fresh name without affecting X. If A is a set of names we write A#X for aA.a#X.

A nominal set S is a set with a permutation action such that XSπXS, and where each member XS has finite support. A main point is that then each member has infinitely many fresh names available for alpha-conversion. Similarly, a set of names N supports a function f on a nominal set if for all π that leave N invariant it holds πf(X)=f(πX), and similarly for relations and functions of higher arity. Thus we extend the notion of support to finitely supported functions and relations as the minimal finite support, and can derive general theorems such as 𝗌𝗎𝗉𝗉(f(X))𝗌𝗎𝗉𝗉(f)𝗌𝗎𝗉𝗉(X).

An object that has empty support we call equivariant. For example, a unary function f is equivariant if πf(X)=f(πX) for all π,X. The intuition is that an equivariant object does not treat any name special.

3 Nominal transition systems and Hennessy-Milner logic

Definition 1.

A nominal transition system is characterized by the following

  • states : A nominal set of states ranged over by P,Q .

  • pred : A nominal set of state predicates ranged over by φ .

  • An equivariant binary relation on states and pred . We write Pφ to mean that in state P the state predicate φ holds.

  • act : A nominal set of actions ranged over by α .

  • An equivariant function 𝖻𝗇 from act to finite sets of names, which for each α returns a subset of 𝗌𝗎𝗉𝗉(α) , called the binding names .

  • An equivariant transition relation on states and residuals. A residual is a pair of action and state. For (P,(α,P)) we write P𝛼P . The transition relation must satisfy alpha-conversion of residuals: If a𝖻𝗇(α) , b#α,P and P𝛼P then also P(ab)α(ab)P .

Definition 2.

A bisimulation R is a symmetric binary relation on states in a nominal transition system satisfying the following two criteria: R(P,Q) implies

  1. 1.

    Static implication : Pφ implies Qφ .

  2. 2.

    Simulation : For all α,P such that 𝖻𝗇(α)#Q there exist Q such that if P𝛼P then Q𝛼Q and R(P,Q)

We write PQ to mean that there exists a bisimulation R such that R(P,Q).

Static implication means that bisimilar states must satisfy the same state predicates; this is reasonable since these can be tested by an observer. The simulation requirement is familiar from the pi-calculus.

Proposition 1.

is an equivariant equivalence relation.

The minimal HML for nominal transition systems is the following.

Definition 3.

The nominal set of formulas 𝒜 ranged over by A is defined by induction as follows:

A::=iIAi|¬A|φ|αA

Support and name permutation are defined as usual (permutation distributes over all formula constructors). In iIAi it is assumed that the indexing set I has bounded cardinality, by which we mean that |I|κ for some fixed infinite cardinal κ at least as large as the cardinality of states, act and pred. It is also required that the set of conjuncts {Ai|iI} has finite support; this is then the support of the conjunction. Alpha-equivalent formulas are identified; the only binding construct is in αA where 𝖻𝗇(α) binds into A.

Compared to previous work there are two main novelties in Definition 3. The first is that we use conjunction of a possibly infinite and finitely supported set of conjuncts. In comparison, the earliest HML for CCS, Hennessy and Milner (1985) [17], uses finite conjunction, meaning that the logic is adequate only for finite branching transition systems. In his subsequent book (1989) [22] Milner admits arbitrary infinite conjunction, disregarding the danger of running into paradoxes. Abramsky (1991) [4] employs a kind of uniformly bounded conjunction, with a finite set of names that supports all conjuncts, an idea that is also used in the first HML for the pi-calculus (1993) [21]. All subsequent developments follow one of these three approaches. Our main point is that both finite and uniformly bounded conjunction are expressively weak, in that the logic is not adequate for the full range of nominal transition systems, and in that quantifiers over infinite structures are not definable. In contrast, our use of finitely supported sets of conjuncts is adequate for all nominal transition systems (cf. Theorems 1 and 2 below) and admits quantifiers as derived operators (cf. Section 4 below). As a simple example, universal quantification over names x𝒩.A(x) is usually defined to mean that A(n) must hold for all n𝒩. We can define this as the (infinite) conjunction of all these A(n). This set of conjuncts is not uniformly bounded if n𝗌𝗎𝗉𝗉(A(n)). But it is supported by 𝗌𝗎𝗉𝗉(A) since, for any permutation π not affecting 𝗌𝗎𝗉𝗉(A) we have πA(n)=A(π(n)) which is also a conjunct; thus the set of conjuncts is unaffected by π.

The second novelty is the use of a nominal set of actions α with binders, and the formal definition of alpha-equivalence. We define it by structural recursion over formulas. Two conjunctions iIAi and iIBi are alpha-equivalent if for every conjunct Ai there is an alpha-equivalent conjunct Bj, and vice versa. The other cases are standard; two formulas αA and βB are alpha-equivalent if there exists a permutation π, renaming the binding names of α to those of β, such that πA and B are alpha-equivalent, and πα=β. Moreover, π must leave names that are free in A invariant. The free names in a formula are also defined by structural recursion. Most cases are standard again; a name is free in αA if it is in 𝗌𝗎𝗉𝗉(α) or free in A, and not contained in 𝖻𝗇(α). However, the free names in a conjunction are given by the support of its alpha-equivalence class (rather than by the union of free names in all conjuncts). This is analogous to the situation for nominal sets in general, whose support is not necessarily the same as the union of the support of its members. Fortunately, our formalization proves that we need not keep the details of this construction in mind, but can simply identify alpha-equivalent formulas. The notions of free names and support then coincide.

The validity of a formula A for a state P is written PA and is defined by recursion over A as follows.

Definition 4.
PiIAiif for all    iI    it holds that    PAiP¬Aif not    PAPφif    PφPαAif there exists    P    such that    P𝛼P    and    PA

In the last clause we assume that αA is a representative of its alpha-equivalence class such that 𝖻𝗇(α)#P. It is easy to show that is an equivariant relation.

Definition 5.

Two states P and Q are logically equivalent, written P=Q, if for all A it holds that PA iff QA

Theorem 1.

PQP=Q

The proof is by induction over formulas. The converse result uses the idea of distinguishing formulas.

Definition 6.

A distinguishing formula for P and Q is a formula A such that PA and not QA.

The following lemma says that we can find such a formula where, a bit surprisingly, the support does not depend on Q.

Lemma 1.

If P=Q then there exists a distinguishing formula B for P and Q such that supp(B)supp(P).

The proof is by direct construction. If P=Q then there exists a distinguishing formula A for P and Q. Let ΠP be the group of finite permutations that leave names in 𝗌𝗎𝗉𝗉(P) invariant, i.e., ΠP={π|n𝗌𝗎𝗉𝗉(P).π(n)=n}. Then {πA|πΠP} is supported by 𝗌𝗎𝗉𝗉(P). Since is equivariant we have that for all πΠP it holds P=πPπA. Let B=πΠPπA, thus PB but Q⊧̸B since the identity is in ΠP and Q⊧̸A. Note that B here uses a conjunction which is not uniformly bounded.

Theorem 2.

P=QPQ

The main idea of the proof is to establish that = is a bisimulation. The simulation requirement is by contradiction: Assume that = does not satisfy the simulation requirement. Then there exist P,Q,P,α such that P=Q and P𝛼P and, letting 𝒬={Q|Q𝛼Q}, for all Q𝒬 it holds P=Q. By Lemma 1 we can find a distinguishing formula BQ for P and Q with 𝗌𝗎𝗉𝗉(BQ)𝗌𝗎𝗉𝗉(P). Therefore the formula B=Q𝒬BQ is well-formed with support included in 𝗌𝗎𝗉𝗉(P). We thus get that PαB but not QαB, contradicting P=Q.

This proof of the simulation property is different from other such proofs in the literature. For finite branching transition systems, 𝒬 is finite so finite conjunction is enough to define B. For transition systems with the name preservation property, i.e., that if P𝛼P then 𝗌𝗎𝗉𝗉(P)𝗌𝗎𝗉𝗉(P)𝗌𝗎𝗉𝗉(α), uniformly bounded conjunction suffices with common support 𝗌𝗎𝗉𝗉(P)𝗌𝗎𝗉𝗉(Q)𝗌𝗎𝗉𝗉(α). Without the name preservation property, we here use a not uniformly bounded conjunction in Lemma 1.

4 Derived formulas

Dual connectives

We define logical disjunction iIAi in the usual way as ¬iI¬Ai, when the indexing set I has bounded cardinality and {Ai|iI} has finite support. A special case is I={1,2}: we then write A1A2 instead of iIAi, and dually for A1A2. We write for the empty conjunction i, and for ¬. The must modality [α]A is defined as ¬α¬A, and requires A to hold after every possible α-labelled transition from the current state. For example, [α](AB) is equivalent to [α]A[α]B, and dually α(AB) is equivalent to αAαB.

Quantifiers

Let S be any finitely supported set of bounded cardinality and use v to range over members of S. Write A{/v}x for the substitution of v for x in A, and assume this substitution function is equivariant. Then we define xS.A as vSA{/v}x. There is not necessarily a common finite support for the formulas A{/v}x, for example if S is some term algebra over names, but the set {A{/v}x|vS} has finite support bounded by {x}𝗌𝗎𝗉𝗉(S)𝗌𝗎𝗉𝗉(A). In our examples in Section 6, substitution is defined inductively on the structure of formulas, based on primitive substitution functions for actions and state predicates, avoiding capture and preserving the binding names of actions.

Existential quantification xS.A is defined as the dual ¬xS.¬A. When X is a metavariable used to range over a nominal set 𝒳, we simply write X for “X𝒳”. As an example, a.A means that the formula A{/n}a holds for all names n𝒩.

New name quantifier

The new name quantifier 𝐍x.A intuitively states that PA{/n}x holds where n is a fresh name for P. For example, suppose we have actions of the form ab for input, and a¯b for output where a and b are free names, then the formula 𝐍x.[ax]b¯x expresses that whenever a process inputs a fresh name x on channel a, it has to be able to output that name on channel b. If the name received is not fresh (i.e., already present in P) then P is not required to do anything. Therefore this formula is weaker than x.[ax]b¯x.

To define this formally we use name permutation rather than substitution. Since A and P have finite support, if P(xn)A holds for some n fresh for P, by equivariance it also holds for almost all n, i.e., all but finitely many n. Conversely, if it holds for almost all n, it must hold for some n#𝗌𝗎𝗉𝗉(P). Therefore 𝐍x is often pronounced “for almost all x”. In other words, P𝐍x.A holds if {x|PA(x)} is a cofinite set of names [27, Definition 3.8]. Letting cof={S𝒩|𝒩S is finite} we thus encode 𝐍x.A as ScofnS(xn)A. This formula states there is a cofinite set of names such that for all of them A holds. The support of nS(xn)A is bounded by (𝒩S)𝗌𝗎𝗉𝗉(A) where Scof, and the support of the encoding ScofnS(xn)A is bounded by 𝗌𝗎𝗉𝗉(A).

Next step

We generalise the action modality to sets of actions in the following way. If T is a finitely supported set of actions such that 𝖻𝗇(α)#A for all αT, we write TA for αTαA. The support of the set {αA|αT} is bounded by 𝗌𝗎𝗉𝗉(T)𝗌𝗎𝗉𝗉(A) and thus finite. Dually, we write [T]A for ¬T¬A, denoting that A holds after all transitions with actions in T.

To encode the next-step modality, let actA={α|𝖻𝗇(α)#A}. Note that 𝗌𝗎𝗉𝗉(actA)𝗌𝗎𝗉𝗉(A) is finite. We write A for actAA, meaning that we can make some (non-capturing) transition to a state where A holds. As an example, means that the current state is not deadlocked. The dual modality []A=¬¬A means that A holds after every transition from the current state. Larsen [19] uses the same approach to define next-step operators in HML, though his version is less expressive since he uses a finite action set to define the next-step modality.

Fixpoints

Fixpoint operators are a way to introduce recursion into a logic. For example, they can be used to concisely express safety and liveness properties of a transition system, where by safety we mean that some invariant holds for all reachable states, and by liveness that some property will eventually hold. Kozen (1983) [18] introduced the least (μX.A) and the greatest (νX.A) fixpoints in modal logic. Intuitively, the least fixpoint states a property that holds for states of a finite path, while the greatest holds for states of an infinite path.

Theorem 3.

The least and greatest fixpoint operators are expressible in our HML.

For the full proofs and definitions, see the appendix of [24]. The idea is to start with an extended language with the forms μX.A and X, where X ranges over a countable set of variables and all occurrences of X in A are in the scope of an even number of negations. Write A(B) for the capture-avoiding substitution of B for X in A, and let A0(B)=B and Ai+1(B)=A(Ai(B)). Then the encoding of a least fixpoint μX.A is iAi(), given that fixpoints have been recursively expanded in A. The disjunction has finite support 𝗌𝗎𝗉𝗉(A), since substitution is equivariant. When interpreting formulas as elements of the power-set lattice of states, this encoding yields a fixpoint of A(): the sequence of formulas Ai() yields an approximation from below. We define the greatest fixpoint operator νX.A in terms of the least as ¬μX.¬A(¬X).

Using the greatest fixpoint operator we can state global invariants: νX.[α]XA expresses that A holds along all paths labelled with α. Temporal operators such as eventually can also be encoded using the least fixpoint operator: the formula μX.αXA states that eventually A holds along some path labelled with α. We can freely mix the fixpoint operators to obtain formulas like νX.[α]X(μY.βYA) which means that for each state along any path labelled with α, a state where A holds is reachable along a path labelled with β. Formulas with mixed fixpoint combinators are very expressive, and with the next operator they can encode the branching-time logic CTL* [13].

5 Logics for variants of bisimilarity

The bisimilarity of Section 3 is of the early kind: any substitutive effect of an input (typically replacing a variable with the value received) must have manifested already in the action corresponding to the input, since we apply no substitution to the target state. Alternative treatments of substitutions include late-, open- and hyperbisimilarity, where the input action instead contains the variable to be replaced, and there are different ways to make sure that bisimulations are preserved by relevant substitutions.

In our definition of nominal transition systems there are no particular input variables in the states or in the actions, and thus no a priori concept of “substitution”. We therefore choose to formulate the alternatives using so called effect functions. An effect is simply a finitely supported function from states to states. For example, in the monadic pi-calculus the effects would be the functions replacing one name by another. In a value-passing calculus the effects would be substitutions of values for variables. In the psi-calculi framework the effects would be sequences of parallel substitutions. Our definitions and results are applicable to any of these; our only requirement is that the effects form a nominal set which we designate by . Variants of bisimilarity then correspond to requiring continuation after various effects. For example, if the action contains an input variable x then the effects appropriate for late bisimilarity would be substitutions for x.

We will formulate these variants as F/L-bisimilarity, where F (for first) represents the set of effects that must be observed before following a transition, and L (for later) is a function that represents how this set F changes depending on the action of a transition, i.e., L(α,F) is the set of effects that must follow the action α if the previous effect set was F. In the following let 𝒫fs() ranged over by F be the finitely supported subsets of , and L range over equivariant functions from actions and 𝒫fs() to 𝒫fs().

Definition 7.

An L-bisimulation where L:act×𝒫𝑓𝑠()𝒫𝑓𝑠() is a 𝒫𝑓𝑠()-indexed family of symmetric binary relations on states satisfying the following:

If RF(P,Q) then:

  1. 1.

    Static implication : for all fF it holds that f(P)φ implies f(Q)φ .

  2. 2.

    Simulation : For all fF and α,P such that 𝖻𝗇(α)#f(Q) there exist Q such that

    if f(P)𝛼P then f(Q)𝛼Q and RL(α,F)(P,Q)

We write PF/LQ, called F/L-bisimilarity, to mean that there exists an L-bisimulation R such that RF(P,Q).

Most strong bisimulation varieties can be formulated as F/L-bismilarity. Write idstates for the identity function on states, ID for the singleton set {idstates} and allID for the constant function λ(α,F).ID.

  • Early bisimilarity, precisely as defined in Definition 2, is ID/allID-bisimilarity.

  • Early equivalence, i.e., early bisimilarity for all possible effects, is /allID-bisimilarity.

  • Late bisimilarity is ID/L-bisimilarity, where L(α,F) yields the effects that represent substitutions for variables in input actions α (and ID for other actions).

  • Late equivalence is similarly /L-bisimilarity.

  • Open bisimilarity is /L-bisimilarity where L(α,F) is the set F minus all effects that change bound output names in α.

  • Hyperbisimilarity is /λ(α,F).-bisimilarity.

All of the above are generalizations of known and well-studied definitions. The original value-passing variant of CCS [22] uses early bisimilarity. The original bisimilarity for the pi-calculus is of the late kind [20], where it also was noted that late equivalence is the corresponding congruence. Early bisimilarity and equivalence and open bisimilarity for the pi-calculus were introduced in 1993 [21, 28], and hyperbisimilarity for the fusion calculus in 1998 [25].

In view of this we only need to provide a modal logic adequate for F/L-bisimilarity; it can then immediately be specialized to all of the above variants. For this we introduce a new kind of logical operator as follows.

Definition 8.

For each f the logical unary effect consequence operator f has the definition

PfA𝑖𝑓f(P)A

Thus the formula fA means that A holds if the effect f is applied to the state. Note that by definition this distributes over conjunction and negation, e.g. P¬fA iff Pf¬A iff not f(P)A etc. The effect consequence operator is similar in spirit to the action modalities: both fA and αA assert that something (an effect or action) must be possible and that A holds afterwards. Indeed, effects can be viewed as a special case of transitions (as formalised in Definition 10 below) which is why we give the operators a common syntactic appearance.

Now define the formulas that can directly use effects from F and after actions use effects according to L, ranged over by AF/L, in the following way:

Definition 9.

Given L as in Definition 7, for all F𝒫𝑓𝑠() define 𝒜F/L as the set of formulas given by the mutually recursive definitions:

AF/L::=iIAiF/L|¬AF/L|fφ|fαAL(α,F)/L

where we require fF and that the conjunction has bounded cardinality and finite support.

Let P=F/LQ mean that P and Q satisfy the same formulas in 𝒜F/L.

Theorem 4.

PF/LQP=F/LQ

Proof: The direction is a generalization of Theorem 1. The other direction is a generalization of Theorem 2: we prove that =F/L is an F/L-bisimulation. It needs a variant of Lemma 1:

Lemma 2.

If A𝒜F/L is a distinguishing formula for P and Q, then there exists a distinguishing formula B𝒜F/L for P and Q such that supp(B)supp(P,F).

The proof is an easy generalisation of Lemma 1.

An alternative to the effect consequence operators is to transform the transition system such that standard (early) bisimulation on the transforms coincides with F/L-bisimilarity. The idea is to let the effect function be part of the transition relation, thus f(P)=P becomes P𝑓P.

Definition 10.

Assume and L as above. The L-transform of a nominal transition system T is a nominal transition system where:

  • The states are of the form ac(F,f(P)) and ef(F,P) , for fF𝒫𝑓𝑠() and states P of T . The intuition is that states of kind ac can perform ordinary actions, and states of kind ef can commit effects.

  • The state predicates are those of T .

  • ac(F,P)φ if in T it holds Pφ , and ef(F,P)φ never holds.

  • The actions are the actions of T and the effects in .

  • 𝖻𝗇 is as in T , and additionally 𝖻𝗇(f)= for f .

  • The transitions are of two kinds. If in T it holds P𝛼P , then there is a transition ac(F,P)𝛼ef(L(α,F),P) . And for each fF it holds ef(F,P)𝑓ac(F,f(P)) .

Theorem 5.

PF/LQ in T if and only if ef(F,P)ef(F,Q) in the L-transform of T .

The proof idea is that from an F/L-bisimulation in T it is easy to construct an (ordinary) bisimulation in the L-transform of T, and vice versa. A direct consequence is that PF/LQ iff ef(F,P)=ef(F,Q) in the L-transform of T. Here the actions in the logic would include effects f.

6 Related work and examples

In this first part of this section we discuss other modal logics for process calculi, with a focus on how their constructors can be captured by finitely supported conjunction in our HML. This comparison is by necessity somewhat informal; a fully formal correspondence would fail to hold in many cases due to differences in the conjunction operator of the logic (finite, uniformly bounded or unbounded vs. bounded support). In the later part of this section, we obtain novel, adequate HMLs for more recent process calculi.

HML for CCS

The first published HML is Hennessy and Milner (1985) [17]. They use finite (binary) conjunction with the assumption of image-finiteness for ordinary CCS. The same goes for the value-passing calculus and logic by Hennessy and Liu (1995) [16], where image-finiteness is due to a late semantics and the logic contains quantification over data values. A similar idea and argument is in a logic for LOTOS by Calder et al. (2002) [9], though that only considers stratified bisimilarity up to ω.

Hennessy and Liu’s value-passing calculus is based on abstractions (x)P and concretions (v,P) where v is drawn from a set of values. To encode the modalities of their logic in ours, we add effects idstates and ?v, with ?v((x)P)=P{/v}x, and transitions (v,P)!vP. Letting L(a?,_)={?v|vvalues} and L(α,_)={idstates} otherwise, late bisimilarity is {idstates}/L-bisimilarity as defined in Section 5. We can then encode their universal quantifier x.A as v?vA{/v}x, which has support 𝗌𝗎𝗉𝗉(A){x}, and their output modality c!xA as c!v!vA{/v}x, with support {c}(𝗌𝗎𝗉𝗉(A){x}).

An infinitary HML for CCS is discussed in Milner’s book (1989) [22], where also the process syntax contains infinite summation. There are no restrictions on the indexing sets and no discussion about how this can exhaust all names. The adequacy theorem is proved by stratifying bisimilarity and using transfinite induction over all ordinals, where the successor step basically is the contraposition of the argument in Theorem 2, though without any consideration of finite support. A more rigorous treatment of the same ideas is by Abramsky (1991) [4] where uniformly bounded conjunction is used throughout.

Pi-calculus

The first HML for the pi-calculus is by Milner et al. (1993) [21], where infinite conjunction is used in the early semantics and conjunctions are restricted to use a finite set of free names. The adequacy proof is of the same structure as in this paper. The logic defined in this paper, applied to the pi-calculus transition system omitting bound input actions x(y), contains the logic of Milner et al., or the equipotent logic if we take the set of name matchings [a=b] as state predicates.

Spi Calculus

Frendrup et al. (2002) [14] provide three Hennessy-Milner logics for the spi calculus [3]. The action modalities in Frendrup’s logic only use parts of the labels: on process output, the modality a¯ tests only the channel used. On process input, the modality aξ describes how the observer σ computed the received message M=𝐞(ξσ), where ξ is an expression that may contain decryptions and projections, and 𝗌𝗎𝗉𝗉(ξ)𝖽𝗈𝗆(σ) is fresh for P and σ. Simplifying the labels of the transition system to τ and the aforementioned a¯ and aξ labels, our minimal HML applied to the particular nominal transition system of the spi calculus has the same modalities as the logic of Frendrup et al., although the latter uses infinite conjunction without any mechanism to prevent formulas from exhausting all names, leaving none available for alpha-conversion. Thus their notion of substitution is not formally well defined.

Their logic replaces the simple input modality by an early input modality a¯(x)EA, which (after a minor manipulation of the input labels) can be encoded as the conjunction ξaξA{/ξ}x, which has support 𝗌𝗎𝗉𝗉(A){x}. We do not consider their logic that uses a late input modality, since its application relies on sets that do not have finite support [14, Theorem 6.12], which are not meaningful in nominal logic.

Applied Pi-calculus

A more recent work is a logic by Pedersen (2006) [26] for the applied pi-calculus [2], where the adequacy theorem uses image-finiteness of the semantics in the contradiction argument. The logic contains atomic formulae for equality in the frame of a process, corresponding to our state predicates. The main difference to our logic is an early input modality and a quantifier x.

Their early input modality a¯(x)A can be straightforwardly encoded as the conjunction Ma¯MA{/M}x, with support {a}(𝗌𝗎𝗉𝗉(A){x}). For the existential quantifier, there is a requirement that the received term M can be computed from the current knowledge available to an observer of the process, which we here write M𝒮(P). We addactions M/x with 𝖻𝗇(M/x)=x and transitions PM/xP{/M}x if M𝒮(P) and x#P. We can then encode x.A as MM/xA, which has support 𝗌𝗎𝗉𝗉(A){x}.

Fusion calculus

In an HML for the fusion calculus by Haugstad et al. (2006) [15] the fusions (i.e., equality relations on names) are action labels φ. The corresponding modal operator φA has the semantics that the formula A must be satisfied for all substitutive effects of φ (intuitively, substitutions that map each name to a fixed representative for its equivalence class). By making the substitutive effects of fusion actions visible in the transition system, we can encode this modal operator. Their adequacy theorem uses the contradiction argument with infinite conjunction, with no argument about finiteness of names for the distinguishing formula.

Nominal transition systems

De Nicola and Loreti (2008) [11] define a general format for nominal transition systems and an associated modal logic, that is adequate for image-finite transition systems only and uses several different modalities for name revelation and resource consumption. In contrast, we seek a small and expressive HML for general nominal transition systems. Indeed, the logic of De Nicola and Loreto can be seen as a special case of ours: their different transition systems can be merged into a single one, and we can encode their quantifiers and fixpoint operator as described in Section 4. Nominal SOS of Cimini et al. (2012) [10] is also a special case of nominal transition systems.

In each of the final two examples below, no HML has to our knowledge yet been proposed, and we immediately obtain one by instantiating the logic in the present paper.

Concurrent constraint pi calculus

The concurrent constraint pi calculus (CC-pi) by Buscemi and Montanari (2007) [7] extends the explicit fusion calculus [30] with a more general notion of constraint stores c. The reference equivalence for CC-pi is open bisimulation [8] (closely corresponding to hyperbisimulation in the fusion calculus [25]), which differs from labelled bisimulation in two ways: First, two equivalent processes must be equivalent under all store extensions. To encode this, we let the effects be the set of constraint stores c different from 0, and let c(P)=cP. Second, when simulating a labelled transition P𝛼P, the simulating process Q can use any transition Q𝛽Q with an equivalent label, as given by a state predicate α=β. As an example, if α=a¯x is a free output label then Pα=β iff β=b¯y where Pa=b and Px=y. To encode this, we transform the labels of the transition system by replacing them with their equivalence classes, i.e., P𝛼P becomes P[α]PP where β[α]P iff Pβ=α. Hyperbisimilarity (Definition 7) on this transition system then corresponds to open bisimilarity, and the modal logic defined in Section 5 is adequate.

Psi-calculi

In psi-calculi by Bengtson et al. (2011) [5], the labelled transitions take the form ΨP𝛼P, where the assertion environment Ψ is unchanged after the step. We model this as a nominal transition system by letting the set of states be pairs (Ψ,P) of assertion environments and processes, and define the transition relation by (Ψ,P)𝛼(Ψ,P)if ΨP𝛼P. The notion of bisimulation used with psi-calculi also uses an assertion environment and is required to be closed under environment extension, i.e., if ΨPQ, then ΨΨPQ for all Ψ. We let the effects  be the set of assertions, anddefine Ψ((Ψ,P))=(ΨΨ,P). Hyperbisimilarity on this transition system then subsumes the standard psi-calculi bisimilarity, and the modal logic defined in Section 5 is adequate.

7 Conclusion

We have given a general account of transition systems and Hennessy-Milner Logic using nominal sets. The advantage of our approach is that it is more expressive than previous work. We allow infinite conjunctions that are not uniformly bounded, meaning that we can encode e.g. quantifiers and the next-step operator. We have given ample examples of how the definition captures different variants of bisimilarity and how it relates to many different versions of HML in the literature.

We have formalized the results of Section 3, including Theorems 1 and 2, using Nominal Isabelle [29].11Our Isabelle theories are available at https://github.com/tjark/ML-for-NTS. Nominal Isabelle is an implementation of nominal logic in Isabelle/HOL [23], a popular interactive proof assistant for higher-order logic. It adds convenient specification mechanisms for, and automation to reason about, datatypes with binders.

However, Nominal Isabelle does not directly support infinitely branching datatypes. Therefore, the mechanization of formulas (Definition 3) was challenging. We construct formulas from first principles in higher-order logic, by defining an inductive datatype of raw formulas (where alpha-equivalent raw formulas are not identified). The datatype constructor for conjunction recurses through sets of raw formulas of bounded cardinality, a feature made possible only by a recent re-implementation of Isabelle/HOL’s datatype package [6].

We then define alpha-equivalence of raw formulas. For finitely branching datatypes, alpha-equivalence is based on a notion of free variables. Here, to obtain the correct notion of free variables of a conjunction, we define alpha-equivalence and free variables via mutual recursion. This necessitates a fairly involved termination proof. (All recursive functions in Isabelle/HOL must be terminating.) To obtain formulas, we quotient raw formulas by alpha-equivalence, and finally carve out the subtype of all terms that can be constructed from finitely supported ones. We then prove important lemmas; for instance, a strong induction principle for formulas that allows the bound names in αA to be chosen fresh for any finitely supported context.

Our development, which in total consists of about 2700 lines of Isabelle definitions and proofs, generalizes the constructions that Nominal Isabelle performs for finitely branching datatypes to a type with infinite branching. To our knowledge, this is the first mechanization of an infinitely branching nominal datatype in a proof assistant.

Acknowledgements

We thank Andrew Pitts for enlightening discussions on nominal datatypes with infinitary constructors, and Dmitriy Traytel for providing a formalization of cardinality-bounded sets.

References

  • [1] (2001-01) 28thAnnual symposium on principles of programming languages (popl)(london, uk). ACM. Cited by: 2.
  • [2] M. Abadi and C. Fournet (2001-01) Mobile values, new names, and secure communication. See 1, pp. 104–115. Cited by: 6.
  • [3] M. Abadi and A. D. Gordon (1999) A calculus for cryptographic protocols: the Spi calculus. Journal of Information and Computation 148 (1), pp. 1–70. Cited by: 6.
  • [4] S. Abramsky (1991) A domain equation for bisimulation. Journal of Information and Computation 92 (2), pp. 161–218. External Links: Link, Document Cited by: 3, 6.
  • [5] J. Bengtson, M. Johansson, J. Parrow and B. Victor (2011) Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science 7 (1). External Links: Link, Document Cited by: 1, 6.
  • [6] J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu and D. Traytel (2014) Truly modular (co)datatypes for Isabelle/HOL. LNCS, Vol. 8558, pp. 93–110. External Links: Link, Document Cited by: 7.
  • [7] M. G. Buscemi and U. Montanari (2007) CC-Pi: a constraint-based language for specifying service level agreements. LNCS, Vol. 4421, pp. 18–32. Cited by: 6.
  • [8] M. G. Buscemi and U. Montanari (2008) Open bisimulation for the concurrent constraint pi-calculus. See 12, pp. 254–268. External Links: Link, Document Cited by: 6.
  • [9] M. Calder, S. Maharaj and C. Shankland (2002) A modal logic for full LOTOS based on symbolic transition systems. The Computer Journal 45 (1), pp. 55–61. Cited by: 6.
  • [10] M. Cimini, M. R. Mousavi, M. A. Reniers and M. J. Gabbay (2012-09) Nominal SOS. Electron. Notes Theor. Comput. Sci. 286, pp. 103–116. External Links: ISSN 1571-0661, Link, Document Cited by: 6.
  • [11] R. De Nicola and M. Loreti (2008) Multiple-labelled transition systems for nominal calculi and their logics. Mathematical Structures in Computer Science 18 (1), pp. 107–143. External Links: Link, Document Cited by: 6.
  • [12] S. Drossopoulou (Ed.) (2008) Programming languages and systems, 17th european symposium on programming, ESOP 2008, held as part of the joint european conferences on theory and practice of software, ETAPS 2008, budapest, hungary, march 29-april 6, 2008. proceedings. LNCS, Vol. 4960, Springer. External Links: ISBN 978-3-540-78738-9 Cited by: 8.
  • [13] E. A. Emerson (1997) Model checking and the mu-calculus. pp. 185–214. Cited by: 4.
  • [14] U. Frendrup, H. Hüttel and J. N. Jensen (2002) Modal logics for cryptographic processes. Electr. Notes Theor. Comput. Sci. 68 (2), pp. 124–141. Cited by: 6, 6.
  • [15] A. M. M. Haugstad, A. F. Terkelsen and T. Vindum (2006) A modal logic for the fusion calculus. Note: Unpublished, University of Aalborg, http://vbn.aau.dk/ws/files/61067487/1149104946.pdf Cited by: 6.
  • [16] M. Hennessy and X. Liu (1995) A modal logic for message passing processes. Acta Informatica 32 (4), pp. 375–393 (English). External Links: ISSN 0001-5903, Document, Link Cited by: 6.
  • [17] M. Hennessy and R. Milner (1985) Algebraic laws for nondeterminism and concurrency. J. ACM 32 (1), pp. 137–161. Cited by: 1, 3, 6.
  • [18] D. Kozen (1983) Results on the propositional mu-calculus. Theoretical Computer Science 27 (3), pp. 333 – 354. Note: Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982 External Links: Document, ISSN 0304-3975, Link Cited by: 4.
  • [19] K. G. Larsen (1988) Proof systems for Hennessy-Milner logic with recursion. in M. Dauchet and M. Nivat (Eds.), Proceedings of CAAP ’88, LNCS, Vol. 299, pp. 215–230. External Links: ISBN 978-3-540-19021-9, Document, Link Cited by: 4.
  • [20] R. Milner, J. Parrow and D. Walker (1992) A calculus of mobile processes, I. Inf. Comput. 100 (1), pp. 1–40. External Links: Link, Document Cited by: 1, 5.
  • [21] R. Milner, J. Parrow and D. Walker (1993) Modal logics for mobile processes. Theoretical Computer Science 114 (1), pp. 149 – 171. External Links: Document, ISSN 0304-3975, Link Cited by: 3, 5, 6.
  • [22] R. Milner (1989) Communication and concurrency. Prentice Hall. Cited by: 3, 5, 6.
  • [23] T. Nipkow, L. C. Paulson and M. Wenzel (2002) Isabelle/HOL - A proof assistant for higher-order logic. LNCS, Vol. 2283, Springer. External Links: Link, Document, ISBN 3-540-43376-7 Cited by: 7.
  • [24] J. Parrow, J. Borgström, L. Eriksson, R. Gutkovas and T. Weber (2015-06) Modal logics for nominal transition systems. Technical report Technical Report 2015-021, Department of Information Technology, Uppsala University. Cited by: 1, 4.
  • [25] J. Parrow and B. Victor (1998) The fusion calculus: expressiveness and symmetry in mobile processes. pp. 176–185. External Links: Link, Document Cited by: 5, 6.
  • [26] M. Pedersen (2006) Logics for the applied pi calculus. Master’s Thesis, Aalborg University. Note: BRICS RS-06-19 Cited by: 6.
  • [27] A. M. Pitts (2013) Nominal sets. Cambridge University Press. Note: Cambridge Books Online External Links: ISBN 9781139084673, Link Cited by: 2, 4.
  • [28] D. Sangiorgi (1993) A theory of bisimulation for the π-calculus. in E. Best (Ed.), Proceedings of CONCUR ’93, LNCS, Vol. 715, pp. 127–142 (English). External Links: ISBN 978-3-540-57208-4, Document, Link Cited by: 5.
  • [29] C. Urban and C. Kaliszyk (2012) General bindings and alpha-equivalence in Nominal Isabelle. Logical Methods in Computer Science 8 (2). External Links: Link, Document Cited by: 1, 7.
  • [30] L. Wischik and P. Gardner (2005) Explicit fusions. Theoretical Computer Science 304 (3), pp. 606–630. Cited by: 6.