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 HennessyMilner 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 CCBY.
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 higherlevel 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 psicalculi [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,\mathrm{\dots}$ 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 $\alpha ,\beta $, representing the externally observable effect of the transition. A transition $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ thus says that in state $P$ the execution can progress to ${P}^{\prime}$ while conducting the action $\alpha $, 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 valuepassing 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 picalculus [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 picalculus such an action is written $\overline{a}(\nu b)$, to mean that the local name $b$ is exported along the channel $a$. These names can be subjected to alphaconversion: if $P\stackrel{\overline{a}(\nu b)}{\to}{P}^{\prime}$ and $c$ is a fresh name then also $P\stackrel{\overline{a}(\nu c)}{\to}{P}^{\prime}\{c/b\}$, where ${P}^{\prime}\{c/b\}$ is ${P}^{\prime}$ with all $b$s replaced by $c$s. Making this idea fully formal is not entirely trivial and many papers gloss over it. In the polyadic picalculus several names can be exported in one action, and in psicalculi 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 $\alpha $ there is a finite set of names $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )$, 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 $\phi $, 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\u22a2\phi $ to mean that in state $P$ the state predicate $\phi $ holds.
A structure with states, transitions, and state predicates as discussed above we call a nominal transition system.
HennessyMilner 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 HennessyMilner Logic [17] (HML). Here the idea is that an action modality $\u27e8\alpha \u27e9$ expresses a possibility to perform an action $\alpha $. If $A$ is a formula then $\u27e8\alpha \u27e9A$ says that it is possible to perform $\alpha $ 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 alphaconversion. 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 alphaconversion. A technically important point is that we do not assume the usual name preservation principle, that if $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ then the names occurring in ${P}^{\prime}$ must be a subset of those occurring in $P$ and $\alpha $. This means that the results are applicable to a wide range of calculi. For example, the picalculus represents a trivial instance where there are no state predicates. CCS represent an even more trivial instance where $\mathrm{\U0001d5bb\U0001d5c7}$ always returns the empty set. In the fusion calculus and the applied picalculus the state contains an environmental part which tells what expressions are equal to what. In the general framework of psicalculi the states are processes with assertions describing their environments.
We define a modal logic with the $\u27e8\alpha \u27e9$ operator that binds the names in $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )$, 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 alphaequivalence 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 alphaequivalence 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 alphaequivalence 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 multisorted set of atomic identifiers or names $\mathcal{N}$ ranged over by $a,b,\mathrm{\dots}$. 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 $\pi ,{\pi}^{\prime}$. The effect of applying a permutation $\pi $ to an object $X$ is written $\pi \cdot X$. Formally, the permutation action $\cdot $ can be any operation that satisfies $\text{id}\cdot X=X$ and $\pi \cdot ({\pi}^{\prime}\cdot X)=(\pi \circ {\pi}^{\prime})\cdot X$, but a reader may comfortably think of $\pi \cdot X$ as the object obtained by permuting all names in $X$ according to $\pi $.
A set of names $N$ supports an object $X$ if for all $\pi $ that leave all members of $N$ invariant it holds $\pi \cdot 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 $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(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 alphaequivalence 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 $\pi \cdot \mathcal{N}=\mathcal{N}$ for any $\pi $.
We write $a\mathrm{\#}X$, pronounced “$a$ is fresh for $X$”, for $a\notin \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(X)$. The intuition is that if $a\mathrm{\#}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\mathrm{\#}X$ for $\forall a\in A.a\mathrm{\#}X$.
A nominal set $S$ is a set with a permutation action such that $X\in S\Rightarrow \pi \cdot X\in S$, and where each member $X\in S$ has finite support. A main point is that then each member has infinitely many fresh names available for alphaconversion. Similarly, a set of names $N$ supports a function $f$ on a nominal set if for all $\pi $ that leave $N$ invariant it holds $\pi \cdot f(X)=f(\pi \cdot 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 $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(f(X))\subseteq \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(f)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(X)$.
An object that has empty support we call equivariant. For example, a unary function $f$ is equivariant if $\pi \cdot f(X)=f(\pi \cdot X)$ for all $\pi ,X$. The intuition is that an equivariant object does not treat any name special.
3 Nominal transition systems and HennessyMilner 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 $\phi $ .

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

•
act : A nominal set of actions ranged over by $\alpha $ .

•
An equivariant function $\mathrm{\U0001d5bb\U0001d5c7}$ from act to finite sets of names, which for each $\alpha $ returns a subset of $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(\alpha )$ , called the binding names .

•
An equivariant transition relation $\to $ on states and residuals. A residual is a pair of action and state. For $\to (P,(\alpha ,{P}^{\prime}))$ we write $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ . The transition relation must satisfy alphaconversion of residuals: If $a\in \mathrm{\U0001d5bb\U0001d5c7}(\alpha )$ , $b\mathrm{\#}\alpha ,{P}^{\prime}$ and $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ then also $P\stackrel{(ab)\cdot \alpha}{\to}(ab)\cdot {P}^{\prime}$ .
Definition 2.
A bisimulation $R$ is a symmetric binary relation on states in a nominal transition system satisfying the following two criteria: $R\mathit{}\mathrm{(}P\mathrm{,}Q\mathrm{)}$ implies

1.
Static implication : $P\u22a2\phi $ implies $Q\u22a2\phi $ .

2.
Simulation : For all $\alpha ,{P}^{\prime}$ such that $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )\mathrm{\#}Q$ there exist ${Q}^{\prime}$ such that if $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ then $Q\stackrel{\mathit{\alpha}}{\to}{Q}^{\prime}$ and $R({P}^{\prime},{Q}^{\prime})$
We write $P\stackrel{\mathrm{\cdot}}{\mathrm{\sim}}Q$ to mean that there exists a bisimulation $R$ such that $R\mathit{}\mathrm{(}P\mathrm{,}Q\mathrm{)}$.
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 picalculus.
Proposition 1.
$\stackrel{\cdot}{\sim}$ is an equivariant equivalence relation.
The minimal HML for nominal transition systems is the following.
Definition 3.
The nominal set of formulas $\mathcal{A}$ ranged over by $A$ is defined by induction as follows:
$$A\mathit{\hspace{1em}}::=\mathit{\hspace{1em}}\underset{i\in I}{\bigwedge}{A}_{i}\mathit{\hspace{1em}}\mathit{\hspace{1em}}\mathrm{\neg}A\mathit{\hspace{1em}}\mathit{\hspace{1em}}\phi \mathit{\hspace{1em}}\mathit{\hspace{1em}}\u27e8\alpha \u27e9A$$ 
Support and name permutation are defined as usual (permutation distributes over all formula constructors). In ${\bigwedge}_{i\in I}{A}_{i}$ it is assumed that the indexing set $I$ has bounded cardinality, by which we mean that $\leftI\right\le \kappa $ for some fixed infinite cardinal $\kappa $ at least as large as the cardinality of states, act and pred. It is also required that the set of conjuncts $\{{A}_{i}i\in I\}$ has finite support; this is then the support of the conjunction. Alphaequivalent formulas are identified; the only binding construct is in $\u27e8\alpha \u27e9A$ where $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )$ 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 picalculus (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 $\forall x\in \mathcal{N}.A(x)$ is usually defined to mean that $A(n)$ must hold for all $n\in \mathcal{N}$. We can define this as the (infinite) conjunction of all these $A(n)$. This set of conjuncts is not uniformly bounded if $n\in \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A(n))$. But it is supported by $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$ since, for any permutation $\pi $ not affecting $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$ we have $\pi \cdot A(n)=A(\pi (n))$ which is also a conjunct; thus the set of conjuncts is unaffected by $\pi $.
The second novelty is the use of a nominal set of actions $\alpha $ with binders, and the formal definition of alphaequivalence. We define it by structural recursion over formulas. Two conjunctions ${\bigwedge}_{i\in I}{A}_{i}$ and ${\bigwedge}_{i\in I}{B}_{i}$ are alphaequivalent if for every conjunct ${A}_{i}$ there is an alphaequivalent conjunct ${B}_{j}$, and vice versa. The other cases are standard; two formulas $\u27e8\alpha \u27e9A$ and $\u27e8\beta \u27e9B$ are alphaequivalent if there exists a permutation $\pi $, renaming the binding names of $\alpha $ to those of $\beta $, such that $\pi \cdot A$ and $B$ are alphaequivalent, and $\pi \cdot \alpha =\beta $. Moreover, $\pi $ 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 $\u27e8\alpha \u27e9A$ if it is in $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(\alpha )$ or free in $A$, and not contained in $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )$. However, the free names in a conjunction are given by the support of its alphaequivalence 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 alphaequivalent formulas. The notions of free names and support then coincide.
The validity of a formula $A$ for a state $P$ is written $P\vDash A$ and is defined by recursion over $A$ as follows.
Definition 4.
$$\begin{array}{cc}P\vDash \underset{i\in I}{\bigwedge}{A}_{i}\hfill & \mathit{\text{if for all}}\text{}i\in I\text{}\mathit{\text{it holds that}}\text{}P\vDash {A}_{i}\hfill \\ P\vDash \mathrm{\neg}A\hfill & \mathit{\text{if not}}\text{}P\vDash A\hfill \\ P\vDash \phi \hfill & \mathit{\text{if}}\text{}P\u22a2\phi \hfill \\ P\vDash \u27e8\alpha \u27e9A\hfill & \mathit{\text{if there exists}}\text{}{P}^{\prime}\text{}\mathit{\text{such that}}\text{}P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}\text{}\mathit{\text{and}}\text{}{P}^{\prime}\vDash A\hfill \end{array}$$ 
In the last clause we assume that $\u27e8\alpha \u27e9A$ is a representative of its alphaequivalence class such that $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )\mathrm{\#}P$. It is easy to show that $\vDash $ is an equivariant relation.
Definition 5.
Two states $P$ and $Q$ are logically equivalent, written $P\stackrel{\mathrm{\cdot}}{\mathrm{=}}Q$, if for all $A$ it holds that $P\mathrm{\vDash}A$ iff $Q\mathrm{\vDash}A$
Theorem 1.
$P\stackrel{\cdot}{\sim}Q\u27f9P\stackrel{\cdot}{=}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 $P\mathrm{\vDash}A$ and not $Q\mathrm{\vDash}A$.
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\mathit{}\overline{)\stackrel{\mathrm{\cdot}}{\mathrm{=}}}\mathit{}Q$ then there exists a distinguishing formula $B$ for $P$ and $Q$ such that $\mathrm{supp}\mathit{}\mathrm{(}B\mathrm{)}\mathrm{\subseteq}\mathrm{supp}\mathit{}\mathrm{(}P\mathrm{)}$.
The proof is by direct construction. If $P\overline{)\stackrel{\cdot}{=}}Q$ then there exists a distinguishing formula $A$ for $P$ and $Q$. Let ${\mathrm{\Pi}}_{P}$ be the group of finite permutations that leave names in $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P)$ invariant, i.e., ${\mathrm{\Pi}}_{P}=\{\pi \forall n\in \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P).\pi (n)=n\}$. Then $\{\pi \cdot A\pi \in {\mathrm{\Pi}}_{P}\}$ is supported by $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P)$. Since $\vDash $ is equivariant we have that for all $\pi \in {\mathrm{\Pi}}_{P}$ it holds $P=\pi \cdot P\vDash \pi \cdot A$. Let $B={\bigwedge}_{\pi \in {\mathrm{\Pi}}_{P}}\pi \cdot A$, thus $P\vDash B$ but $Q\vDash \u0338B$ since the identity is in ${\mathrm{\Pi}}_{P}$ and $Q\vDash \u0338A$. Note that $B$ here uses a conjunction which is not uniformly bounded.
Theorem 2.
$P\stackrel{\cdot}{=}Q\u27f9P\stackrel{\cdot}{\sim}Q$
The main idea of the proof is to establish that $\stackrel{\cdot}{=}$ is a bisimulation. The simulation requirement is by contradiction: Assume that $\stackrel{\cdot}{=}$ does not satisfy the simulation requirement. Then there exist $P,Q,{P}^{\prime},\alpha $ such that $P\stackrel{\cdot}{=}Q$ and $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ and, letting $\mathcal{Q}=\{{Q}^{\prime}Q\stackrel{\mathit{\alpha}}{\to}{Q}^{\prime}\}$, for all ${Q}^{\prime}\in \mathcal{Q}$ it holds ${P}^{\prime}\overline{)\stackrel{\cdot}{=}}{Q}^{\prime}$. By Lemma 1 we can find a distinguishing formula ${B}_{{Q}^{\prime}}$ for ${P}^{\prime}$ and ${Q}^{\prime}$ with $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}({B}_{{Q}^{\prime}})\subseteq \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}({P}^{\prime})$. Therefore the formula $B={\bigwedge}_{{Q}^{\prime}\in \mathcal{Q}}{B}_{{Q}^{\prime}}$ is wellformed with support included in $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}({P}^{\prime})$. We thus get that $P\vDash \u27e8\alpha \u27e9B$ but not $Q\vDash \u27e8\alpha \u27e9B$, contradicting $P\stackrel{\cdot}{=}Q$.
This proof of the simulation property is different from other such proofs in the literature. For finite branching transition systems, $\mathcal{Q}$ is finite so finite conjunction is enough to define $B$. For transition systems with the name preservation property, i.e., that if $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ then $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}({P}^{\prime})\subseteq \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(\alpha )$, uniformly bounded conjunction suffices with common support $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(Q)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(\alpha )$. 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 ${\bigvee}_{i\in I}{A}_{i}$ in the usual way as $\mathrm{\neg}{\bigwedge}_{i\in I}\mathrm{\neg}{A}_{i}$, when the indexing set $I$ has bounded cardinality and $\{{A}_{i}i\in I\}$ has finite support. A special case is $I=\{1,2\}$: we then write ${A}_{1}\wedge {A}_{2}$ instead of ${\bigwedge}_{i\in I}{A}_{i}$, and dually for ${A}_{1}\vee {A}_{2}$. We write $\top $ for the empty conjunction ${\bigwedge}_{i\in \mathrm{\varnothing}}$, and $\perp $ for $\mathrm{\neg}\top $. The must modality $[\alpha ]A$ is defined as $\mathrm{\neg}\u27e8\alpha \u27e9\mathrm{\neg}A$, and requires $A$ to hold after every possible $\alpha $labelled transition from the current state. For example, $[\alpha ](A\wedge B)$ is equivalent to $[\alpha ]A\wedge [\alpha ]B$, and dually $\u27e8\alpha \u27e9(A\vee B)$ is equivalent to $\u27e8\alpha \u27e9A\vee \u27e8\alpha \u27e9B$.
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 $\forall x\in S.A$ as ${\bigwedge}_{v\in S}A\{{}^{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}\}v\in S\}$ has finite support bounded by $\{x\}\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(S)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(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 $\exists x\in S.A$ is defined as the dual $\mathrm{\neg}\forall x\in S.\mathrm{\neg}A$. When $X$ is a metavariable used to range over a nominal set $\mathcal{X}$, we simply write $X$ for “$X\in \mathcal{X}$”. As an example, $\forall a.A$ means that the formula $A\{{}^{n}/{}_{a}\}$ holds for all names $n\in \mathcal{N}$.
New name quantifier
The new name quantifier $\mathbf{N}x.A$ intuitively states that $P\vDash A\{{}^{n}/{}_{x}\}$ holds where $n$ is a fresh name for $P$. For example, suppose we have actions of the form $ab$ for input, and $\overline{a}b$ for output where $a$ and $b$ are free names, then the formula $\mathbf{N}x.[ax]\u27e8\overline{b}x\u27e9\top $ 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 $\forall x.[ax]\u27e8\overline{b}x\u27e9\top $.
To define this formally we use name permutation rather than substitution. Since $A$ and $P$ have finite support, if $P\vDash (xn)\cdot 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\mathrm{\#}\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(P)$. Therefore $\mathbf{N}x$ is often pronounced “for almost all $x$”. In other words, $P\vDash \mathbf{N}x.A$ holds if $\{xP\vDash A(x)\}$ is a cofinite set of names [27, Definition 3.8]. Letting $\mathrm{\text{cof}}=\{S\subseteq \mathcal{N}\mathcal{N}\setminus S\text{is finite}\}$ we thus encode $\mathbf{N}x.A$ as ${\bigvee}_{S\in \mathrm{\text{cof}}}{\bigwedge}_{n\in S}(xn)\cdot A$. This formula states there is a cofinite set of names such that for all of them $A$ holds. The support of ${\bigwedge}_{n\in S}(xn)\cdot A$ is bounded by $(\mathcal{N}\setminus S)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$ where $S\in \mathrm{\text{cof}}$, and the support of the encoding ${\bigvee}_{S\in \mathrm{\text{cof}}}{\bigwedge}_{n\in S}(xn)\cdot A$ is bounded by $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(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 $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )\mathrm{\#}A$ for all $\alpha \in T$, we write $\u27e8T\u27e9A$ for ${\bigvee}_{\alpha \in T}\u27e8\alpha \u27e9A$. The support of the set $\{\u27e8\alpha \u27e9A\alpha \in T\}$ is bounded by $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(T)\cup \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$ and thus finite. Dually, we write $[T]A$ for $\mathrm{\neg}\u27e8T\u27e9\mathrm{\neg}A$, denoting that $A$ holds after all transitions with actions in $T$.
To encode the nextstep modality, let ${\mathrm{\text{act}}}_{A}=\{\alpha \mathrm{\U0001d5bb\U0001d5c7}(\alpha )\mathrm{\#}A\}$. Note that $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}({\mathrm{\text{act}}}_{A})\subseteq \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$ is finite. We write $\u27e8\u27e9A$ for $\u27e8{\mathrm{\text{act}}}_{A}\u27e9A$, meaning that we can make some (noncapturing) transition to a state where $A$ holds. As an example, $\u27e8\u27e9\top $ means that the current state is not deadlocked. The dual modality $[]A=\mathrm{\neg}\u27e8\u27e9\mathrm{\neg}A$ means that $A$ holds after every transition from the current state. Larsen [19] uses the same approach to define nextstep operators in HML, though his version is less expressive since he uses a finite action set to define the nextstep 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 ($\mu X.A$) and the greatest ($\nu 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 $\mu 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 captureavoiding substitution of $B$ for $X$ in $A$, and let ${A}^{0}(B)=B$ and ${A}^{i+1}(B)=A({A}^{i}(B))$. Then the encoding of a least fixpoint $\mu X.A$ is ${\bigvee}_{i\in \mathbb{N}}{A}^{i}(\perp )$, given that fixpoints have been recursively expanded in $A$. The disjunction has finite support $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)$, since substitution is equivariant. When interpreting formulas as elements of the powerset lattice of states, this encoding yields a fixpoint of $A(\cdot )$: the sequence of formulas ${A}^{i}(\perp )$ yields an approximation from below. We define the greatest fixpoint operator $\nu X.A$ in terms of the least as $\mathrm{\neg}\mu X.\mathrm{\neg}A(\mathrm{\neg}X)$.
Using the greatest fixpoint operator we can state global invariants: $\nu X.[\alpha ]X\wedge A$ expresses that $A$ holds along all paths labelled with $\alpha $. Temporal operators such as eventually can also be encoded using the least fixpoint operator: the formula $\mu X.\u27e8\alpha \u27e9X\vee A$ states that eventually $A$ holds along some path labelled with $\alpha $. We can freely mix the fixpoint operators to obtain formulas like $\nu X.[\alpha ]X\wedge (\mu Y.\u27e8\beta \u27e9Y\vee A)$ which means that for each state along any path labelled with $\alpha $, a state where $A$ holds is reachable along a path labelled with $\beta $. Formulas with mixed fixpoint combinators are very expressive, and with the next operator they can encode the branchingtime logic ${\text{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 picalculus the effects would be the functions replacing one name by another. In a valuepassing calculus the effects would be substitutions of values for variables. In the psicalculi 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 $\mathcal{F}$. 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(\alpha ,F)$ is the set of effects that must follow the action $\alpha $ if the previous effect set was $F$. In the following let ${\mathcal{P}}_{\text{fs}}(\mathcal{F})$ ranged over by $F$ be the finitely supported subsets of $\mathcal{F}$, and $L$ range over equivariant functions from actions and ${\mathcal{P}}_{\text{fs}}(\mathcal{F})$ to ${\mathcal{P}}_{\text{fs}}(\mathcal{F})$.
Definition 7.
An Lbisimulation where $L\mathrm{:}\mathrm{\text{act}}\mathrm{\times}{\mathcal{P}}_{\text{\mathit{f}\mathit{s}}}\mathit{}\mathrm{(}\mathcal{F}\mathrm{)}\mathrm{\to}{\mathcal{P}}_{\text{\mathit{f}\mathit{s}}}\mathit{}\mathrm{(}\mathcal{F}\mathrm{)}$ is a ${\mathcal{P}}_{\text{\mathit{f}\mathit{s}}}\mathit{}\mathrm{(}\mathcal{F}\mathrm{)}$indexed family of symmetric binary relations on states satisfying the following:
If ${R}_{F}\mathit{}\mathrm{(}P\mathrm{,}Q\mathrm{)}$ then:

1.
Static implication : for all $f\in F$ it holds that $f(P)\u22a2\phi $ implies $f(Q)\u22a2\phi $ .

2.
Simulation : For all $f\in F$ and $\alpha ,{P}^{\prime}$ such that $\mathrm{\U0001d5bb\U0001d5c7}(\alpha )\mathrm{\#}f(Q)$ there exist ${Q}^{\prime}$ such that
if $f\mathit{}\mathrm{(}P\mathrm{)}\stackrel{\mathit{\alpha}}{\mathrm{\to}}{P}^{\mathrm{\prime}}$ then $f\mathit{}\mathrm{(}Q\mathrm{)}\stackrel{\mathit{\alpha}}{\mathrm{\to}}{Q}^{\mathrm{\prime}}$ and ${R}_{L\mathit{}\mathrm{(}\alpha \mathrm{,}F\mathrm{)}}\mathit{}\mathrm{(}{P}^{\mathrm{\prime}}\mathrm{,}{Q}^{\mathrm{\prime}}\mathrm{)}$
We write $P\stackrel{F\mathrm{/}L}{\mathrm{\sim}}Q$, called $F\mathrm{/}L$bisimilarity, to mean that there exists an $L$bisimulation $R$ such that ${R}_{F}\mathit{}\mathrm{(}P\mathrm{,}Q\mathrm{)}$.
Most strong bisimulation varieties can be formulated as $F/L$bismilarity. Write ${\text{id}}_{\mathrm{\text{states}}}$ for the identity function on states, ID for the singleton set $\{{\text{id}}_{\mathrm{\text{states}}}\}$ and ${\text{all}}_{\text{ID}}$ for the constant function $\lambda (\alpha ,F).\text{ID}$.

•
Early bisimilarity, precisely as defined in Definition 2, is $\text{ID}/{\text{all}}_{\text{ID}}$bisimilarity.

•
Early equivalence, i.e., early bisimilarity for all possible effects, is $\mathcal{F}/{\text{all}}_{\text{ID}}$bisimilarity.

•
Late bisimilarity is $\text{ID}/L$bisimilarity, where $L(\alpha ,F)$ yields the effects that represent substitutions for variables in input actions $\alpha $ (and ID for other actions).

•
Late equivalence is similarly $\mathcal{F}/L$bisimilarity.

•
Open bisimilarity is $\mathcal{F}/L$bisimilarity where $L(\alpha ,F)$ is the set $F$ minus all effects that change bound output names in $\alpha $.

•
Hyperbisimilarity is $\mathcal{F}/\lambda (\alpha ,F).\mathcal{F}$bisimilarity.
All of the above are generalizations of known and wellstudied definitions. The original valuepassing variant of CCS [22] uses early bisimilarity. The original bisimilarity for the picalculus 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 picalculus 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\mathrm{\in}\mathcal{F}$ the logical unary effect consequence operator $\mathrm{\u27e8}f\mathrm{\u27e9}$ has the definition
$$P\vDash \u27e8f\u27e9A\mathit{\hspace{1em}}\text{\mathit{i}\mathit{f}}\mathit{\hspace{1em}}f(P)\vDash A$$ 
Thus the formula $\u27e8f\u27e9A$ 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\vDash \mathrm{\neg}\u27e8f\u27e9A$ iff $P\vDash \u27e8f\u27e9\mathrm{\neg}A$ iff not $f(P)\vDash A$ etc. The effect consequence operator is similar in spirit to the action modalities: both $\u27e8f\u27e9A$ and $\u27e8\alpha \u27e9A$ 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 ${A}^{F/L}$, in the following way:
Definition 9.
Given $L$ as in Definition 7, for all $F\mathrm{\in}{\mathcal{P}}_{\text{\mathit{f}\mathit{s}}}\mathit{}\mathrm{(}\mathcal{F}\mathrm{)}$ define ${\mathcal{A}}^{F\mathrm{/}L}$ as the set of formulas given by the mutually recursive definitions:
$${A}^{F/L}\mathit{\hspace{1em}}::=\mathit{\hspace{1em}}\underset{i\in I}{\bigwedge}{A}_{i}^{F/L}\mathit{\hspace{1em}}\mathit{\hspace{1em}}\mathrm{\neg}{A}^{F/L}\mathit{\hspace{1em}}\mathit{\hspace{1em}}\u27e8f\u27e9\phi \mathit{\hspace{1em}}\mathit{\hspace{1em}}\u27e8f\u27e9\u27e8\alpha \u27e9{A}^{L(\alpha ,F)/L}$$ 
where we require $f\mathrm{\in}F$ and that the conjunction has bounded cardinality and finite support.
Let $P\stackrel{F/L}{=}Q$ mean that $P$ and $Q$ satisfy the same formulas in ${\mathcal{A}}^{F/L}$.
Theorem 4.
$P\stackrel{F/L}{\sim}Q\mathit{\hspace{1em}}\iff \mathit{\hspace{1em}}P\stackrel{F/L}{=}Q$
Proof: The direction $\Rightarrow $ is a generalization of Theorem 1. The other direction is a generalization of Theorem 2: we prove that $\stackrel{F/L}{=}$ is an $F/L$bisimulation. It needs a variant of Lemma 1:
Lemma 2.
If $A\mathrm{\in}{\mathcal{A}}^{F\mathrm{/}L}$ is a distinguishing formula for $P$ and $Q$, then there exists a distinguishing formula $B\mathrm{\in}{\mathcal{A}}^{F\mathrm{/}L}$ for $P$ and $Q$ such that $\mathrm{supp}\mathit{}\mathrm{(}B\mathrm{)}\mathrm{\subseteq}\mathrm{supp}\mathit{}\mathrm{(}P\mathrm{,}F\mathrm{)}$.
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}^{\prime}$ becomes $P\stackrel{\mathit{f}}{\to}{P}^{\prime}$.
Definition 10.
Assume $\mathcal{F}$ 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 $\mathrm{\text{ac}}(F,f(P))$ and $\mathrm{\text{ef}}(F,P)$ , for $f\in F\in {\mathcal{P}}_{\text{\mathit{f}\mathit{s}}}(\mathcal{F})$ 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 .

•
$\mathrm{\text{ac}}(F,P)\u22a2\phi $ if in T it holds $P\u22a2\phi $ , and $\mathrm{\text{ef}}(F,P)\u22a2\phi $ never holds.

•
The actions are the actions of T and the effects in $\mathcal{F}$ .

•
$\mathrm{\U0001d5bb\U0001d5c7}$ is as in T , and additionally $\mathrm{\U0001d5bb\U0001d5c7}(f)=\mathrm{\varnothing}$ for $f\in \mathcal{F}$ .

•
The transitions are of two kinds. If in T it holds $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ , then there is a transition $\mathrm{\text{ac}}(F,P)\stackrel{\mathit{\alpha}}{\to}\mathrm{\text{ef}}(L(\alpha ,F),{P}^{\prime})$ . And for each $f\in F$ it holds $\mathrm{\text{ef}}(F,P)\stackrel{\mathit{f}}{\to}\mathrm{\text{ac}}(F,f(P))$ .
Theorem 5.
$P\stackrel{F/L}{\sim}Q$ in T if and only if $\mathrm{\text{ef}}\mathit{}\mathrm{(}F\mathrm{,}P\mathrm{)}\stackrel{\mathrm{\cdot}}{\mathrm{\sim}}\mathrm{\text{ef}}\mathit{}\mathrm{(}F\mathrm{,}Q\mathrm{)}$ 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 $P\stackrel{F/L}{\sim}Q$ iff $\mathrm{\text{ef}}(F,P)\stackrel{\cdot}{=}\mathrm{\text{ef}}(F,Q)$ in the $L$transform of T. Here the actions in the logic would include effects $f\in \mathcal{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 imagefiniteness for ordinary CCS. The same goes for the valuepassing calculus and logic by Hennessy and Liu (1995) [16], where imagefiniteness 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 $\omega $.
Hennessy and Liu’s valuepassing 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 ${\text{id}}_{\mathrm{\text{states}}}$ and $\mathrm{?}v$, with $\mathrm{?}v((x)P)=P\{{}^{v}/{}_{x}\}$, and transitions $(v,P)\stackrel{!v}{\to}P$. Letting $L(a\mathrm{?},\mathrm{\_})=\{\mathrm{?}vv\in \text{values}\}$ and $L(\alpha ,\mathrm{\_})=\{{\text{id}}_{\mathrm{\text{states}}}\}$ otherwise, late bisimilarity is $\{{\text{id}}_{\mathrm{\text{states}}}\}/L$bisimilarity as defined in Section 5. We can then encode their universal quantifier $\forall x.A$ as ${\bigwedge}_{v}\u27e8\mathrm{?}v\u27e9A\{{}^{v}/{}_{x}\}$, which has support $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)\setminus \{x\}$, and their output modality $\u27e8c!x\u27e9A$ as $\u27e8c!\u27e9{\bigvee}_{v}\u27e8!v\u27e9A\{{}^{v}/{}_{x}\}$, with support $\{c\}\cup (\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)\setminus \{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.
Picalculus
The first HML for the picalculus 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 picalculus transition system omitting bound input actions $x(y)$, contains the logic $\mathcal{F}$ of Milner et al., or the equipotent logic $\mathcal{F}\mathcal{M}$ if we take the set of name matchings $[a=b]$ as state predicates.
Spi Calculus
Frendrup et al. (2002) [14] provide three HennessyMilner logics for the spi calculus [3]. The action modalities in Frendrup’s logic only use parts of the labels: on process output, the modality $\u27e8\overline{a}\u27e9$ tests only the channel used. On process input, the modality $\u27e8a\xi \u27e9$ describes how the observer $\sigma $ computed the received message $M=\mathbf{e}(\xi \sigma )$, where $\xi $ is an expression that may contain decryptions and projections, and $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(\xi )\setminus \mathrm{\U0001d5bd\U0001d5c8\U0001d5c6}(\sigma )$ is fresh for $P$ and $\sigma $. Simplifying the labels of the transition system to $\tau $ and the aforementioned $\overline{a}$ and $a\xi $ labels, our minimal HML applied to the particular nominal transition system of the spi calculus has the same modalities as the logic $\mathcal{F}$ of Frendrup et al., although the latter uses infinite conjunction without any mechanism to prevent formulas from exhausting all names, leaving none available for alphaconversion. Thus their notion of substitution is not formally well defined.
Their logic $\mathcal{E}\mathcal{M}$ replaces the simple input modality by an early input modality ${\u27e8\underset{\xaf}{a}(x)\u27e9}^{E}A$, which (after a minor manipulation of the input labels) can be encoded as the conjunction ${\bigwedge}_{\xi}\u27e8a\xi \u27e9A\{{}^{\xi}/{}_{x}\}$, which has support $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)\setminus \{x\}$. We do not consider their logic $\mathcal{L}\mathcal{M}$ 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 Picalculus
A more recent work is a logic by Pedersen (2006) [26] for the applied picalculus [2], where the adequacy theorem uses imagefiniteness 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 $\exists x$.
Their early input modality $\u27e8\underset{\xaf}{a}(x)\u27e9A$ can be straightforwardly encoded as the conjunction ${\bigwedge}_{M}\u27e8\underset{\xaf}{a}M\u27e9A\{{}^{M}/{}_{x}\}$, with support $\{a\}\cup (\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)\setminus \{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\in \mathcal{S}(P)$. We addactions $M/x$ with $\mathrm{\U0001d5bb\U0001d5c7}(M/x)=x$ and transitions $P\stackrel{M/x}{\to}P\mid \{{}^{M}/{}_{x}\}$ if $M\in \mathcal{S}(P)$ and $x\mathrm{\#}P$. We can then encode $\exists x.A$ as ${\bigvee}_{M}\u27e8M/x\u27e9A$, which has support $\mathrm{\U0001d5cc\U0001d5ce\U0001d5c9\U0001d5c9}(A)\setminus \{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 $\phi $. The corresponding modal operator $\u27e8\phi \u27e9A$ has the semantics that the formula $A$ must be satisfied for all substitutive effects of $\phi $ (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 imagefinite 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 (CCpi) 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 CCpi 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 $\mathcal{F}$ be the set of constraint stores $c$ different from $0$, and let $c(P)=c\mid P$. Second, when simulating a labelled transition $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$, the simulating process $Q$ can use any transition $Q\stackrel{\mathit{\beta}}{\to}{Q}^{\prime}$ with an equivalent label, as given by a state predicate $\alpha =\beta $. As an example, if $\alpha =\overline{a}\u27e8x\u27e9$ is a free output label then $P\u22a2\alpha =\beta $ iff $\beta =\overline{b}\u27e8y\u27e9$ where $P\u22a2a=b$ and $P\u22a2x=y$. To encode this, we transform the labels of the transition system by replacing them with their equivalence classes, i.e., $P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$ becomes $P\stackrel{{[\alpha ]}_{P}}{\to}{P}^{\prime}$ where $\beta \in {[\alpha ]}_{P}$ iff $P\u22a2\beta =\alpha $. Hyperbisimilarity (Definition 7) on this transition system then corresponds to open bisimilarity, and the modal logic defined in Section 5 is adequate.
Psicalculi
In psicalculi by Bengtson et al. (2011) [5], the labelled transitions take the form $\mathrm{\Psi}\u25b7P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$, where the assertion environment $\mathrm{\Psi}$ is unchanged after the step. We model this as a nominal transition system by letting the set of states be pairs $(\mathrm{\Psi},P)$ of assertion environments and processes, and define the transition relation by $(\mathrm{\Psi},P)\stackrel{\mathit{\alpha}}{\to}(\mathrm{\Psi},{P}^{\prime})$if $\mathrm{\Psi}\u25b7P\stackrel{\mathit{\alpha}}{\to}{P}^{\prime}$. The notion of bisimulation used with psicalculi also uses an assertion environment and is required to be closed under environment extension, i.e., if $\mathrm{\Psi}\u25b7P\sim Q$, then $\mathrm{\Psi}\otimes {\mathrm{\Psi}}^{\prime}\u25b7P\sim Q$ for all ${\mathrm{\Psi}}^{\prime}$. We let the effects $\mathcal{F}$ be the set of assertions, anddefine $\mathrm{\Psi}(({\mathrm{\Psi}}^{\prime},P))=(\mathrm{\Psi}\otimes {\mathrm{\Psi}}^{\prime},P)$. Hyperbisimilarity on this transition system then subsumes the standard psicalculi bisimilarity, and the modal logic defined in Section 5 is adequate.
7 Conclusion
We have given a general account of transition systems and HennessyMilner 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 nextstep 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].^{1}^{1}Our Isabelle theories are available at https://github.com/tjark/MLforNTS. Nominal Isabelle is an implementation of nominal logic in Isabelle/HOL [23], a popular interactive proof assistant for higherorder 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 higherorder logic, by defining an inductive datatype of raw formulas (where alphaequivalent 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 reimplementation of Isabelle/HOL’s datatype package [6].
We then define alphaequivalence of raw formulas. For finitely branching datatypes, alphaequivalence is based on a notion of free variables. Here, to obtain the correct notion of free variables of a conjunction, we define alphaequivalence 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 alphaequivalence, 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 $\u27e8\alpha \u27e9A$ 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 cardinalitybounded sets.
References
 [1] (200101) 28thAnnual symposium on principles of programming languages (popl)(london, uk). ACM. Cited by: 2.
 [2] (200101) 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) Psicalculi: 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) CCPi: a constraintbased language for specifying service level agreements. LNCS, Vol. 4421, pp. 18–32. Cited by: 6.
 [8] (2008) Open bisimulation for the concurrent constraint picalculus. 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] (201209) Nominal SOS. Electron. Notes Theor. Comput. Sci. 286, pp. 103–116. External Links: ISSN 15710661, Link, Document Cited by: 6.
 [11] (2008) Multiplelabelled 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 29april 6, 2008. proceedings. LNCS, Vol. 4960, Springer. External Links: ISBN 9783540787389 Cited by: 8.
 [13] (1997) Model checking and the mucalculus. 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 00015903, 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 mucalculus. 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 03043975, Link Cited by: 4.
 [19] (1988) Proof systems for HennessyMilner logic with recursion. in M. Dauchet and M. Nivat (Eds.), Proceedings of CAAP ’88, LNCS, Vol. 299, pp. 215–230. External Links: ISBN 9783540190219, 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 03043975, 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 higherorder logic. LNCS, Vol. 2283, Springer. External Links: Link, Document, ISBN 3540433767 Cited by: 7.
 [24] (201506) Modal logics for nominal transition systems. Technical report Technical Report 2015021, 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 RS0619 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 $\pi $calculus. in E. Best (Ed.), Proceedings of CONCUR ’93, LNCS, Vol. 715, pp. 127–142 (English). External Links: ISBN 9783540572084, Document, Link Cited by: 5.
 [29] (2012) General bindings and alphaequivalence 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.