Modal Logics for Nominal Transition Systems
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 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 thus says that in state the execution can progress to 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 , to mean that the local name is exported along the channel . These names can be subjected to alpha-conversion: if and is a fresh name then also , where is with all s replaced by s. 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 to mean that in state 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 is a formula then says that it is possible to perform and reach a state where 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 then the names occurring in must be a subset of those occurring in 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 permutation is a bijection on names that leaves all but finitely many names invariant. The singleton permutation which swaps names and and has no other effect is written , and the identity permutation that swaps nothing is written id. Permutations are ranged over by . The effect of applying a permutation to an object is written . Formally, the permutation action can be any operation that satisfies and , but a reader may comfortably think of as the object obtained by permuting all names in according to .
A set of names supports an object if for all that leave all members of invariant it holds . In other words, if supports then names outside do not matter to . If a finite set supports then there is a unique minimal set supporting , called the support of , written , intuitively consisting of exactly the names that matter to . 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 , pronounced “ is fresh for ”, for . The intuition is that if then does not depend on in the sense that can be replaced with any fresh name without affecting . If is a set of names we write for .
A nominal set is a set with a permutation action such that , and where each member 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 supports a function on a nominal set if for all that leave invariant it holds , 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 .
An object that has empty support we call equivariant. For example, a unary function is equivariant if for all . 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 .
-
•
pred : A nominal set of state predicates ranged over by .
-
•
An equivariant binary relation on states and pred . We write to mean that in state 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 we write . The transition relation must satisfy alpha-conversion of residuals: If , and then also .
Definition 2.
A bisimulation is a symmetric binary relation on states in a nominal transition system satisfying the following two criteria: implies
-
1.
Static implication : implies .
-
2.
Simulation : For all such that there exist such that if then and
We write to mean that there exists a bisimulation such that .
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 is defined by induction as follows:
Support and name permutation are defined as usual (permutation distributes over all formula constructors). In it is assumed that the indexing set has bounded cardinality, by which we mean that 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 has finite support; this is then the support of the conjunction. Alpha-equivalent formulas are identified; the only binding construct is in where binds into .
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 is usually defined to mean that must hold for all . We can define this as the (infinite) conjunction of all these . This set of conjuncts is not uniformly bounded if . But it is supported by since, for any permutation not affecting we have 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 and are alpha-equivalent if for every conjunct there is an alpha-equivalent conjunct , and vice versa. The other cases are standard; two formulas and are alpha-equivalent if there exists a permutation , renaming the binding names of to those of , such that and are alpha-equivalent, and . Moreover, must leave names that are free in invariant. The free names in a formula are also defined by structural recursion. Most cases are standard again; a name is free in if it is in or free in , 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 for a state is written and is defined by recursion over as follows.
Definition 4.
In the last clause we assume that is a representative of its alpha-equivalence class such that . It is easy to show that is an equivariant relation.
Definition 5.
Two states and are logically equivalent, written , if for all it holds that iff
Theorem 1.
The proof is by induction over formulas. The converse result uses the idea of distinguishing formulas.
Definition 6.
A distinguishing formula for and is a formula such that and not .
The following lemma says that we can find such a formula where, a bit surprisingly, the support does not depend on .
Lemma 1.
If then there exists a distinguishing formula for and such that .
The proof is by direct construction. If then there exists a distinguishing formula for and . Let be the group of finite permutations that leave names in invariant, i.e., . Then is supported by . Since is equivariant we have that for all it holds . Let , thus but since the identity is in and . Note that here uses a conjunction which is not uniformly bounded.
Theorem 2.
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 such that and and, letting , for all it holds . By Lemma 1 we can find a distinguishing formula for and with . Therefore the formula is well-formed with support included in . We thus get that but not , contradicting .
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 . For transition systems with the name preservation property, i.e., that if then , uniformly bounded conjunction suffices with common support . 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 in the usual way as , when the indexing set has bounded cardinality and has finite support. A special case is : we then write instead of , and dually for . We write for the empty conjunction , and for . The must modality is defined as , and requires to hold after every possible -labelled transition from the current state. For example, is equivalent to , and dually is equivalent to .
Quantifiers
Let be any finitely supported set of bounded cardinality and use to range over members of . Write for the substitution of for in , and assume this substitution function is equivariant. Then we define as . There is not necessarily a common finite support for the formulas , for example if is some term algebra over names, but the set has finite support bounded by . 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 is defined as the dual . When is a metavariable used to range over a nominal set , we simply write for “”. As an example, means that the formula holds for all names .
New name quantifier
The new name quantifier intuitively states that holds where is a fresh name for . For example, suppose we have actions of the form for input, and for output where and are free names, then the formula expresses that whenever a process inputs a fresh name on channel , it has to be able to output that name on channel . If the name received is not fresh (i.e., already present in ) then is not required to do anything. Therefore this formula is weaker than .
To define this formally we use name permutation rather than substitution. Since and have finite support, if holds for some fresh for , by equivariance it also holds for almost all , i.e., all but finitely many . Conversely, if it holds for almost all , it must hold for some . Therefore is often pronounced “for almost all ”. In other words, holds if is a cofinite set of names [27, Definition 3.8]. Letting we thus encode as . This formula states there is a cofinite set of names such that for all of them holds. The support of is bounded by where , and the support of the encoding is bounded by .
Next step
We generalise the action modality to sets of actions in the following way. If is a finitely supported set of actions such that for all , we write for . The support of the set is bounded by and thus finite. Dually, we write for , denoting that holds after all transitions with actions in .
To encode the next-step modality, let . Note that is finite. We write for , meaning that we can make some (non-capturing) transition to a state where holds. As an example, means that the current state is not deadlocked. The dual modality means that 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 () and the greatest () 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 and , where ranges over a countable set of variables and all occurrences of in are in the scope of an even number of negations. Write for the capture-avoiding substitution of for in , and let and . Then the encoding of a least fixpoint is , given that fixpoints have been recursively expanded in . The disjunction has finite support , since substitution is equivariant. When interpreting formulas as elements of the power-set lattice of states, this encoding yields a fixpoint of : the sequence of formulas yields an approximation from below. We define the greatest fixpoint operator in terms of the least as .
Using the greatest fixpoint operator we can state global invariants: expresses that holds along all paths labelled with . Temporal operators such as eventually can also be encoded using the least fixpoint operator: the formula states that eventually holds along some path labelled with . We can freely mix the fixpoint operators to obtain formulas like which means that for each state along any path labelled with , a state where 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 [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 then the effects appropriate for late bisimilarity would be substitutions for .
We will formulate these variants as -bisimilarity, where (for first) represents the set of effects that must be observed before following a transition, and (for later) is a function that represents how this set changes depending on the action of a transition, i.e., is the set of effects that must follow the action if the previous effect set was . In the following let ranged over by be the finitely supported subsets of , and range over equivariant functions from actions and to .
Definition 7.
An L-bisimulation where is a -indexed family of symmetric binary relations on states satisfying the following:
If then:
-
1.
Static implication : for all it holds that implies .
-
2.
Simulation : For all and such that there exist such that
if then and
We write , called -bisimilarity, to mean that there exists an -bisimulation such that .
Most strong bisimulation varieties can be formulated as -bismilarity. Write for the identity function on states, ID for the singleton set and for the constant function .
-
•
Early bisimilarity, precisely as defined in Definition 2, is -bisimilarity.
-
•
Early equivalence, i.e., early bisimilarity for all possible effects, is -bisimilarity.
-
•
Late bisimilarity is -bisimilarity, where yields the effects that represent substitutions for variables in input actions (and ID for other actions).
-
•
Late equivalence is similarly -bisimilarity.
-
•
Open bisimilarity is -bisimilarity where is the set minus all effects that change bound output names in .
-
•
Hyperbisimilarity is -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 -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 the logical unary effect consequence operator has the definition
Thus the formula means that holds if the effect is applied to the state. Note that by definition this distributes over conjunction and negation, e.g. iff iff not etc. The effect consequence operator is similar in spirit to the action modalities: both and assert that something (an effect or action) must be possible and that 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 and after actions use effects according to , ranged over by , in the following way:
Definition 9.
Given as in Definition 7, for all define as the set of formulas given by the mutually recursive definitions:
where we require and that the conjunction has bounded cardinality and finite support.
Let mean that and satisfy the same formulas in .
Theorem 4.
Proof: The direction is a generalization of Theorem 1. The other direction is a generalization of Theorem 2: we prove that is an -bisimulation. It needs a variant of Lemma 1:
Lemma 2.
If is a distinguishing formula for and , then there exists a distinguishing formula for and such that .
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 -bisimilarity. The idea is to let the effect function be part of the transition relation, thus becomes .
Definition 10.
Assume and as above. The -transform of a nominal transition system T is a nominal transition system where:
-
•
The states are of the form and , for and states 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 .
-
•
if in T it holds , and never holds.
-
•
The actions are the actions of T and the effects in .
-
•
is as in T , and additionally for .
-
•
The transitions are of two kinds. If in T it holds , then there is a transition . And for each it holds .
Theorem 5.
in T if and only if in the -transform of T .
The proof idea is that from an -bisimulation in T it is easy to construct an (ordinary) bisimulation in the -transform of T, and vice versa. A direct consequence is that iff in the -transform of T. Here the actions in the logic would include effects .
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 and concretions where is drawn from a set of values. To encode the modalities of their logic in ours, we add effects and , with , and transitions . Letting and otherwise, late bisimilarity is -bisimilarity as defined in Section 5. We can then encode their universal quantifier as , which has support , and their output modality as , with support .
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 , contains the logic of Milner et al., or the equipotent logic if we take the set of name matchings 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 tests only the channel used. On process input, the modality describes how the observer computed the received message , where is an expression that may contain decryptions and projections, and is fresh for and . Simplifying the labels of the transition system to and the aforementioned and 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 , which (after a minor manipulation of the input labels) can be encoded as the conjunction , which has support . 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 .
Their early input modality can be straightforwardly encoded as the conjunction , with support . For the existential quantifier, there is a requirement that the received term can be computed from the current knowledge available to an observer of the process, which we here write . We addactions with and transitions if and . We can then encode as , which has support .
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 has the semantics that the formula 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 . 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 different from , and let . Second, when simulating a labelled transition , the simulating process can use any transition with an equivalent label, as given by a state predicate . As an example, if is a free output label then iff where and . To encode this, we transform the labels of the transition system by replacing them with their equivalence classes, i.e., becomes where iff . 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 , 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 of assertion environments and processes, and define the transition relation by if . 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 , then for all . We let the effects be the set of assertions, anddefine . 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 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] (2001-01) Mobile values, new names, and secure communication. See 1, pp. 104–115. Cited by: 6.
- [3] (1999) A calculus for cryptographic protocols: the Spi calculus. Journal of Information and Computation 148 (1), pp. 1–70. Cited by: 6.
- [4] (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] (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] (2014) Truly modular (co)datatypes for Isabelle/HOL. LNCS, Vol. 8558, pp. 93–110. External Links: Link, Document Cited by: 7.
- [7] (2007) CC-Pi: a constraint-based language for specifying service level agreements. LNCS, Vol. 4421, pp. 18–32. Cited by: 6.
- [8] (2008) Open bisimulation for the concurrent constraint pi-calculus. See 12, pp. 254–268. External Links: Link, Document Cited by: 6.
- [9] (2002) A modal logic for full LOTOS based on symbolic transition systems. The Computer Journal 45 (1), pp. 55–61. Cited by: 6.
- [10] (2012-09) Nominal SOS. Electron. Notes Theor. Comput. Sci. 286, pp. 103–116. External Links: ISSN 1571-0661, Link, Document Cited by: 6.
- [11] (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] (1997) Model checking and the mu-calculus. pp. 185–214. Cited by: 4.
- [14] (2002) Modal logics for cryptographic processes. Electr. Notes Theor. Comput. Sci. 68 (2), pp. 124–141. Cited by: 6, 6.
- [15] (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] (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] (1985) Algebraic laws for nondeterminism and concurrency. J. ACM 32 (1), pp. 137–161. Cited by: 1, 3, 6.
- [18] (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] (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] (1992) A calculus of mobile processes, I. Inf. Comput. 100 (1), pp. 1–40. External Links: Link, Document Cited by: 1, 5.
- [21] (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] (1989) Communication and concurrency. Prentice Hall. Cited by: 3, 5, 6.
- [23] (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] (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] (1998) The fusion calculus: expressiveness and symmetry in mobile processes. pp. 176–185. External Links: Link, Document Cited by: 5, 6.
- [26] (2006) Logics for the applied pi calculus. Master’s Thesis, Aalborg University. Note: BRICS RS-06-19 Cited by: 6.
- [27] (2013) Nominal sets. Cambridge University Press. Note: Cambridge Books Online External Links: ISBN 9781139084673, Link Cited by: 2, 4.
- [28] (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] (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] (2005) Explicit fusions. Theoretical Computer Science 304 (3), pp. 606–630. Cited by: 6.