As introduced in Section 3, $\textsc{LambdaUnify}(A,e)$ returns a mapping from
abstraction variables and holes to expressions $[\alpha_{i}\to
e_{i}^{\prime},\ \ldots,\ \texttt{??}_{j}\to u_{j}^{\prime},\ \ldots]$ such
that

(19) $(\lambda\alpha_{i}.\ \ldots\ \lambda\texttt{??}_{j}.\ \ldots A)\
e_{i}^{\prime}\ \ldots\ u_{j}^{\prime}\ \ldots=e$

through beta reduction. The LambdaUnify procedure is given in Fig. 4 and the
definition of beta reduction with a modified upshifting operator is given in
Fig. 5.

We can write Eq. 19 in terms of substitution as

(20) $[\alpha_{i}\to e_{i}^{\prime},\ \ldots,\ \texttt{??}_{j}\to
u_{j}^{\prime},\ \ldots]\ \circ A=e$

Which can in turn be written in terms of LambdaUnify as

(21) $\textsc{LambdaUnify}(A,e)\circ A=e$

To prove the correctness of LambdaUnify, we must show that Eq. 21 holds for
all $A$ and $e$. We do this in two ways: a written proof (below) of our
correctness theorem (Theorem B.1), and a machine-verifiable proof in Coq. The
Coq proof is given in stitch.v in the supplementary material and was proven
with CoqIDE 8.15.2. The meanings of the definitions and lemmas in the Coq
proof are commented. The Coq proof differs from the written proof in places
because encoding the proof in Coq required coming up with some representations
that worked well for Coq, though these differences are limited. For example,
the Coq proof requires fully formalizing the behavior of Merge and proofs
related to it which is more simply explained in the written proof. When lemmas
in the written proof below correspond directly to lemmas in the Coq proof, the
corresponding Coq lemma is indicated in the written proof below.

###  B.1. Well-formedness

We formalize a notion of well-formedness to capture the set of expressions
that are accessible starting from an expression with no $\&i$ variables then
applying any series of upshifts and downshifts. We define $\text{WF}_{d}(e)$,
the well-formedness of an expression $e$ at a depth $d$, as follows:

$\displaystyle\text{WF}_{d}\ \lambda.b=\text{WF}_{d+1}\ b$
$\displaystyle\text{WF}_{d}\ (fx)=\text{WF}_{d}\ f\land\text{WF}_{d}\ x$
$\displaystyle\text{WF}_{d}\ \$i=\top$ $\displaystyle\text{WF}_{d}\
\&i=\begin{cases}\top,&\text{if }i<d\\\ \bot,&\text{if }i\geq d\\\
\end{cases}$ $\displaystyle\text{WF}_{d}\ t=\top,\ \text{for
$t\in\mathcal{G}_{\texttt{sym}}$}$

Note that trivially any expression $e$ without any $\&i$ variables is well
formed, as $\&i$ variables are the only source of $\bot$ in this definition.

If every expression in a mapping $l$ is well-formed, we say that the mapping
itself is well-formed, written $(\text{WFMap}\ l)$.

###  B.2. Relevant Lemmas

The following two lemmas show that upshifting and downshifting preserve well-
formedness. In Coq these lemmas are upshift_wf and downshift_wf.

###### Lemma 3.

$\forall e.\ \forall d.\ \text{WF}_{d}\ e\implies\text{WF}_{d}\ \uparrow_{d}e$

###### Proof.

We proceed by induction on e.

Case $e=\lambda.\ b$. Our goal is

$\text{WF}_{d}\ \uparrow_{d}\lambda.b$

We can move $\uparrow_{d}$ and $\text{WF}_{d}$ into the lambda by unfolding
their definitions to get

$\text{WF}_{d+1}\ \uparrow_{d+1}b$

We also have the premise $\text{WF}_{d}\ \lambda.b$, where we can likewise
move the $\text{WF}_{d}$ into the lambda to get $\text{WF}_{d+1}\ b$. The
inductive hypothesis $\forall d.\ \text{WF}_{d}\ b\implies\text{WF}_{d}\
\uparrow_{d}b$ can be instantiated with $d$ as $d+1$ to get $\text{WF}_{d+1}\
b\implies\text{WF}_{d+1}\ \uparrow_{d+1}b$, the conclusion of which is
precisely our goal and the premise of which is precisely our other premise.

Case $e=f\ x$. Our goal is

$\text{WF}_{d}\ \uparrow_{d}(f\ x)$

We can move $\uparrow_{d}$ and $\text{WF}_{d}$ into the application by
unfolding their definitions to get

$(\text{WF}_{d}\ \uparrow_{d}f)\ \land(\text{WF}_{d}\ \uparrow_{d}x)$

We can use our inductive hypotheses $\text{WF}_{d}\ f\implies\text{WF}_{d}\
\uparrow_{d}f$ to prove the left side of this conjunction if we can prove
$\text{WF}_{d}\ f$. We have the premise that $\text{WF}_{d}\ (f\ x)$ from this
overall induction case, which by definition of $\text{WF}_{d}$ can only be
true if $\text{WF}_{d}\ f\land\text{WF}_{d}\ d$. Thus we can prove the left
side of the conjunction, and the proof of the right side is identical with $f$
replaced by $x$ using the other inductive hypothesis.

Case $e=\$i$. Our goal is

$\text{WF}_{d}\ \uparrow_{d}\$i$

We will handle this in 2 cases:

  * •

Case $i<d$.

$\text{WF}_{d}\ \uparrow_{d}\$i$ $=\text{WF}_{d}\ \$i$

This is true because $i indices are always well-formed.

  * •

Case $i\geq d$.

$\text{WF}_{d}\ \uparrow_{d}\$i$ $=\text{WF}_{d}\ \$(i+1)$

This is true because $i indices are always well-formed.

Case $e=\&i$. Our goal is

$\text{WF}_{d}\ \uparrow_{d}\&i$

We will handle our goal in 2 cases:

  * •

Case $i+1\neq d$.

$\text{WF}_{d}\ \uparrow_{d}\$i$ $=\text{WF}_{d}\ \&(i+1)$

We know from our premise that $\text{WF}_{d}\ \&i$ which means $i<d$, so
$i+1\leq d$. Combining this with our knowledge from the case branch that
$i+1\neq d$, we know that $i+1<d$ which means that $\&(i+1)$ is well formed.

  * •

Case $i+1=d$.

$\text{WF}_{d}\ \uparrow_{d}\&i$ $=\text{WF}_{d}\ \$(i+1)$

This is true because $i indices are always well-formed.

Case $e=t$. Our goal is $\text{WF}_{d}\ \uparrow_{d}t$ which simplifies by
definition of $\uparrow_{d}$ to $\text{WF}_{d}\ t$ which is true by definition
of $\text{WF}_{d}$.

∎

###### Lemma 4.

$\forall e.\ \forall d.\ \text{WF}_{d}\ e\implies\text{WF}_{d}\
\downarrow_{d}e$

###### Proof.

We proceed by induction on e. The cases $e=t$, $e=(f\ x)$ and $e=\lambda.b$
are identical to those in Lemma 3 but with $\uparrow$ replaced with
$\downarrow$ so they will be omitted.

Case $e=\$i$. Our goal is

$\text{WF}_{d}\ \downarrow_{d}\$i$

We will handle this in 3 cases:

  * •

Case $i<d$.

$\text{WF}_{d}\ \downarrow_{d}\$i$ $=\text{WF}_{d}\ \$i$

This is true because $i indices are always well-formed.

  * •

Case $i>d$.

$\text{WF}_{d}\ \downarrow_{d}\$i$ $=\text{WF}_{d}\ \$(i-1)$

This is true because $i indices are always well-formed.

  * •

Case $i=d$.

$\text{WF}_{d}\ \downarrow_{d}\$i$ $=\text{WF}_{d}\ \&(i-1)$

Since $i=d$ we know that $i-1<d$ which means $\&(i-1)$ is well-formed.

Case $e=\&i$. Our goal is

$\text{WF}_{d}\ \downarrow_{d}\&i$

which simplifies to

$\text{WF}_{d}\ \&(i-1)$

We know from our premise that $\text{WF}_{d}\ \&i$ so $i<d$ which means
$i-1<d$ so $\&(i-1)$ is well-formed.

∎

The following lemma shows that upshifting is an inverse of downshifting. In
Coq this lemma is upshift_downshift.

###### Lemma 5.

$\forall e.\ \forall d.\ \text{WF}_{d}\
e\implies\uparrow_{d}\downarrow_{d}e=e$

###### Proof.

We proceed by induction on $e$.

Case $e=\lambda.\ b$. Our goal is

$\uparrow_{d}\downarrow_{d}\lambda.\ b=\lambda.\ b$

By the definitions of $\uparrow_{d}$ and $\downarrow_{d}$ we can propagate
them into the body of a lambda while incrementing $d$:

$\lambda.\ \uparrow_{d+1}\downarrow_{d+1}b=\lambda.\ b$

We also have the additional premise $\text{WF}_{d}\ \lambda.b$ which
simplifies to $\text{WF}_{d+1}\ b$.

Since our inductive hypothesis $\forall d.\ \text{WF}_{d}\
b\implies\uparrow_{d}\downarrow_{d}b=b$ is universally quantified over $d$ we
can instantiate it with $d+1$ in place of $d$ and discharge its precondition
with our other premise $\text{WF}_{d+1}\ b$ to get
$\uparrow_{d+1}\downarrow_{d+1}b=b$ and apply this to our goal to get

$\lambda.\ b=\lambda.\ b$

which is trivially true.

Case $e=f\ x$. Our goal is

$\uparrow_{d}\downarrow_{d}(f\ x)=f\ x$

By the definitions of $\uparrow_{d}$ and $\downarrow_{d}$ we can propagate
them into both sides of the application:

$(\uparrow_{d}\downarrow_{d}f)(\uparrow_{d}\downarrow_{d}x)=f\ x$

We also have the additional premise $\text{WF}_{d}\ (f\ x)$ can be broken into
the two premises $\text{WF}_{d}\ f$ and $\text{WF}_{d}\ x$.

We can then apply our inductive hypotheses $\forall d.\ \text{WF}_{d}\
f\implies\uparrow_{d}\downarrow_{d}f=f$ and $\forall d.\ \text{WF}_{d}\
x\implies\uparrow_{d}\downarrow_{d}x=x$ with these premises to rewrite our
goal to

$f\ x=f\ x$

which is trivially true.

Case $e=\$i$. Our goal is

$\uparrow_{d}\downarrow_{d}\$i=\$i$

We will handle this in 3 cases:

  * •

Case $i<d$.

$\uparrow_{d}\downarrow_{d}\$i=\$i$

Unfold definition of $\downarrow_{d}$

$\uparrow_{d}\$i=\$i$

Unfold definition of $\uparrow_{d}$

$\$i=\$i$

  * •

Case $i>d$.

$\uparrow_{d}\downarrow_{d}\$i=\$i$

Unfold definition of $\downarrow_{d}$

$\uparrow_{d}\$(i-1)=\$i$

Unfold definition of $\uparrow_{d}$ noting that $(i-1)\geq d$

$\$((i-1)+1)=\$i$

Simplify

$\$i=\$i$

  * •

Case $i=d$.

$\uparrow_{d}\downarrow_{d}\$i=\$i$

Unfold definition of $\downarrow_{d}$

$\uparrow_{d}\&(i-1)=\$i$

Unfold definition of $\uparrow_{d}$ noting that $(i-1)+1=d$

$\$((i-1)+1)=\$i$

Simplify

$\$i=\$i$

Case $e=\&i$. Our goal is

$\uparrow_{d}\downarrow_{d}\&i=\&i$

Unfolding the definition of $\downarrow_{d}$ yields

$\uparrow_{d}\&(i-1)=\&i$

Since we know that $\text{WF}_{d}\ \&i$ by our premise, we know that $i<d$ so
$(i-1)+1<d$ so $(i-1)+1\neq d$ so $\uparrow_{d}$ unfolds to:

$\&((i-1)+1)=\&i$

which simplifies to

$\&i=\&i$

which is trivially true.

Case $e=t$. Our goal is

$\uparrow_{d}\downarrow_{d}t=t$

Neither $\uparrow_{d}$ nor $\downarrow_{d}$ have any effect on a grammar
primitive $t$, so this is trivially true.

∎

The following lemma shows that any result of LambdaUnify is a well-formed
mapping. In Coq this lemma is called lu_wf.

###### Lemma 6.

$\forall A.\ \forall e.\text{WFMap}\ \textsc{LambdaUnify}(A,e)$

###### Proof.

This is a straightforward proof by induction. In the $\alpha_{i}$ and and
$\texttt{??}_{i}$ cases LambdaUnify adds expressions from the original
expression to the mapping, which are well-formed as they can’t contain $\&i$
variables. In the lambda case DownshiftAll shifts variables using $\downarrow$
which is guaranteed to preserve well-formedness by Lemma 4. In the application
case merge simply combines mappings from the function and argument calls to
LambdaUnify which are well-formed by induction, resulting in an overall well-
formed mapping. ∎

The following lemma follows from Lemma 5 and shows that UpshiftAll is an
inverse of DownshiftAll. In Coq this lemma is upshift_all_downshift_all.

###### Lemma 7.

$\text{WFMap}\ l\implies\textsc{UpshiftAll}(\textsc{DownshiftAll}(l))=l$

###### Proof.

Writing $l$ as $[\alpha_{i}\to\ e_{i}^{\prime},\ \texttt{??}_{j}\to\
u_{j}^{\prime},\ ...]$ and unfolding the definitions of UpshiftAll
DownshiftAll we get:

$[\alpha_{i}\to\ \uparrow_{0}\downarrow_{0}e_{i}^{\prime},\
\texttt{??}_{j}\to\ \uparrow_{0}\downarrow_{0}u_{j}^{\prime},\
...]=[\alpha_{i}\to\ e_{i}^{\prime},\ \texttt{??}_{j}\to\ u_{j}^{\prime},\
...]$

This equality will hold if
$\uparrow_{0}\downarrow_{0}u_{j}^{\prime}=u_{j}^{\prime}$ and
$\uparrow_{0}\downarrow_{0}e_{i}^{\prime}=e_{i}^{\prime}$ for all
$u_{j}^{\prime}$ and $e_{i}^{\prime}$. $\text{WFMap}\ l$ tells us that all
expressions $u_{j}^{\prime}$ and $e_{i}^{\prime}$ are well-formed and thus
satisfy the precondition of Lemma 5, which proves these equalities true.

∎

The following two lemmas allow us to ”forget” one side of a merge when it
won’t have any effect on the substitution. In Coq the first lemma is
merge_forget3 and the second is captured by the definition Compatible.

###### Lemma 8.

If $l_{1}$ is a mapping that binds every abstraction variable and hole in $A$,
then $\textsc{merge}(l_{1},l_{2})\circ A=l_{1}\circ A$.

###### Proof.

$l_{1}$ already assigns to every abstraction variable and hole, and merging in
$l_{2}$ can’t overwrite these assignments since merge fails when the same
variable or hole is assigned to two different expressions. Thus merging in
$l_{2}$ has no effect on the resulting expression from substitution. ∎

###### Lemma 9.

If $l_{2}$ is a mapping that binds every abstraction variable and hole in $A$,
then $\textsc{merge}(l_{1},l_{2})\circ A=l_{2}\circ A$.

###### Proof.

This proof is identical in structure to Lemma 8. $l_{2}$ already assigns to
every abstraction variable and hole, and merging in $l_{1}$ can’t overwrite
these assignments since merge fails when the same variable or hole is assigned
to two different expressions. Thus merging in $l_{1}$ has no effect on the
resulting expression from substitution. ∎

The following lemma shows that any result of LambdaUnify satisfies the
precondition of Lemma 9 and Lemma 8.

###### Lemma 10.

$\textsc{LambdaUnify}(A,e)$ returns a mapping that binds all abstraction
variables $\alpha_{i}$ and all holes $\texttt{??}_{i}$ in $A$.

###### Proof.

This is a straightforward proof by induction. In the $\alpha_{i}$ and and
$\texttt{??}_{i}$ cases LambdaUnify binds the variable and hole respectively,
in the lambda case DownshiftAll has no effect on which abstraction variables
are bound (and it binds all the variables in the body by induction), and in
the application case merge results in combining the function and argument
mappings (which bind all variables by induction) to result in a mapping which
binds all variables that appear in both the function and argument. ∎

###  B.3. Correctness Theorem

In Coq this theorem is called correctness.

###### Theorem B.1.

$\forall A.\ \forall e.\ \textsc{LambdaUnify}(A,e)\circ A=e$

###### Proof.

We proceed by induction over the proof tree of $\textsc{LambdaUnify}(A,e)$.

Case U-AbsVar. Our goal is $\textsc{LambdaUnify}(A,\alpha)\circ\alpha=e$ which
simplifies by definition of LambdaUnify to $[\alpha\to e]\circ\alpha=e$ which
is true by the definition of substitution.

Case U-Hole. Our goal is
$\textsc{LambdaUnify}(A,\texttt{??})\circ\texttt{??}=e$ which simplifies by
definition of LambdaUnify to $[\texttt{??}\to e]\circ\texttt{??}=e$ which is
true by the definition of substitution.

Case U-App. Our goal is

$\textsc{LambdaUnify}(A_{1}\ A_{2},\ e_{1}\ e_{2})\circ(A_{1}\ A_{2})=e_{1}\
e_{2}$

This simplifies by definition of LambdaUnify to

$\textsc{merge}(\textsc{LambdaUnify}(A_{1},e_{1}),\textsc{LambdaUnify}(A_{2},e_{2}))\circ(A_{1}\
A_{2})=e_{1}\ e_{2}$

We can distribute the substitution over the application (by definition of
substitution in Fig. 5 (Left)) to get

$\displaystyle($
$\displaystyle(\textsc{merge}(\textsc{LambdaUnify}(A_{1},e_{1}),\textsc{LambdaUnify}(A_{2},e_{2}))\circ
A_{1})$
$\displaystyle(\textsc{merge}(\textsc{LambdaUnify}(A_{1},e_{1}),\textsc{LambdaUnify}(A_{2},e_{2}))\circ
A_{2}))$ $\displaystyle=e_{1}\ e_{2}$

We can then forget the irrelevant part of each merge using Lemma 9 and Lemma 8
where the precondition (binding all abstraction variables and holes) is
satisfied by Lemma 10:

$\displaystyle($ $\displaystyle(\textsc{LambdaUnify}(A_{1},e_{1})\circ A_{1})$
$\displaystyle(\textsc{LambdaUnify}(A_{2},e_{2})\circ A_{2}))$
$\displaystyle=e_{1}\ e_{2}$

We can then finish the proof by directly applying our inductive hypotheses
$\textsc{LambdaUnify}(A_{1},e_{1})\circ A_{1}=e_{1}$ and
$\textsc{LambdaUnify}(A_{2},e_{2})\circ A_{2}=e_{2}$.

Case U-Lam. Our goal is

$\textsc{LambdaUnify}(\lambda.\ A,\lambda.\ e)\circ\lambda.\ A=\lambda.\ e$

This simplifies by definition of LambdaUnify to

$\textsc{DownshiftAll}(\textsc{LambdaUnify}(A,e))\circ\lambda.\ A=\lambda.\ e$

We can move the substitution under the lambda while inserting UpshiftAll as
per the definition of substitution

$\lambda.\
\textsc{UpshiftAll}(\textsc{DownshiftAll}(\textsc{LambdaUnify}(A,e)))\circ
A=\lambda.\ e$

Since we know that any result of LambdaUnify is well-formed by Lemma 6 we can
apply Lemma 7 to get

$\lambda.\ \textsc{LambdaUnify}(A,e)\circ A=\lambda.\ e$

We can then apply our inductive hypothesis $\textsc{LambdaUnify}(A,e)\circ
A=e$ to get

$\lambda.\ e=\lambda.\ e$

and we are done.

Case U-Same. Our goal is $\textsc{LambdaUnify}(e,e)\circ e=e$ which simplifies
by definition of LambdaUnify to $[]\circ e=e$ which is trivially true as the
empty substitution has no effect.

∎


Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}Q^{\prime}\\}$, for all
$Q^{\prime}\in{\mathcal{Q}}$ it holds that
$P^{\prime}\not\stackrel{{\scriptstyle\cdot}}{{\equiv}}Q^{\prime}$. Assume
$\operatorname{bn}(\alpha)\\#P$, otherwise just find an alpha-variant of the
transition satisfying this. By
$P^{\prime}\not\stackrel{{\scriptstyle\cdot}}{{\equiv}}Q^{\prime}$, for all
$Q^{\prime}\in{\mathcal{Q}}$ there exists a weak distinguishing formula for
$P^{\prime}$ and $Q^{\prime}$. The formula may depend on $Q^{\prime}$, and by
Lemma 34 we can find such a distinguishing formula $B_{Q^{\prime}}$ for
$P^{\prime}$ and $Q^{\prime}$ with
$\operatorname{supp}(B_{Q^{\prime}})\subseteq\operatorname{supp}(P^{\prime})$.
Let $B$ be the conjunction of all $B_{Q^{\prime}}$. We thus get that
$P\nobreak\,\models\nobreak\,\langle\\!\langle\alpha\rangle\\!\rangle B$ but
not $Q\nobreak\,\models\nobreak\,\langle\\!\langle\alpha\rangle\\!\rangle B$,
contradicting $P\stackrel{{\scriptstyle\cdot}}{{\equiv}}Q$.

We omit the proofs of the following results (which have also been formalised
in Isabelle), as they are similar to the corresponding proofs for the full
logic in Section 3.3. In addition, we need to verify that the constructions
used below yield weak formulas. This is immediate from Definition 32.

######  Lemma 36.

If $P\not\stackrel{{\scriptstyle\cdot}}{{\equiv}}Q$, write $B_{P,Q}$ for a
distinguishing weak formula for $P$ and $Q$ such that
$\operatorname{supp}(B_{P,Q})\subseteq\operatorname{supp}(P)$. Then

$D(P,Q):=\bigwedge_{\pi}\pi^{-1}\cdot B_{\pi\cdot P,\pi\cdot Q}$

defines a distinguishing weak formula for $P$ and $Q$ with support included in
$\operatorname{supp}(P)$. Moreover, the function $D$ is equivariant.

A _characteristic weak formula_ for $P$ is a weak formula $A$ such that for
all $Q$, $P\stackrel{{\scriptstyle\cdot}}{{\approx}}Q$ iff
$Q\nobreak\,\models\nobreak\,A$.

######  Lemma 37.

Let $D$ be defined as in Lemma 36. The formula
$\mathrm{Char}(P):=\bigwedge_{P\not\stackrel{{\scriptstyle\cdot}}{{\equiv}}Q}D(P,Q)$
is a characteristic weak formula for $P$.

######  Lemma 38.

Let $\mathrm{Char(P)}$ be defined as in Lemma 37. The function
$\mathrm{Char}\colon P\mapsto\mathrm{Char}(P)$ is equivariant.

######  Theorem 39 (Weak Expressive Completeness).

Let $S$ be a finitely supported set of states that is closed under weak
bisimilarity, i.e., for all $P\in S$ and $Q$,
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}Q$ implies $Q\in S$. Then $P\in S$
iff $P\nobreak\,\models\nobreak\,\bigvee_{P^{\prime}\in
S}\mathrm{Char}(P^{\prime})$.

###  7.4. Disjunction elimination

As defined in Section 4, disjunction is a derived logical operator, expressed
through conjunction and negation. This is still true in the weak modal logic,
but there is a twist in that neither general conjunctions nor negations may be
applied to unguarded state predicates. The examples in Section 7.1 demonstrate
why this restriction is necessary: negated or conjoined state predicates in
formulas would mean that adequacy no longer holds. Interestingly, we can allow
disjunctions of unguarded predicates while maintaining adequacy; in fact,
adding disjunction would not increase the expressive power of the logic. In
this section we demonstrate this claim. An uninterested reader may skip this
section without loss of continuity.

The extended weak logic is as follows, where a simultaneous induction defines
both extended weak formulas (ranged over by $E$) and preformulas (ranged over
by $B$) corresponding to subformulas with unguarded state predicates.

[Extended weak formulas $E$ and preformulas $B$]

$\begin{array}[]{l}E\quad::=\quad\bigwedge_{i\in I}E_{i}\quad|\quad\neg
E\quad|\quad\langle\\!\langle\alpha\rangle\\!\rangle
E\quad|\quad\langle\\!\langle\tau\rangle\\!\rangle B\\\ \\\ B\quad::=\quad
E\wedge B\quad|\quad\varphi\quad|\quad\bigvee_{i\in I}B_{i}\end{array}$

The last clause in the definition of preformulas is what distinguishes this
logic from the logic in Definition 32. (Thus an extended weak formula is also
an ordinary weak formula if it does not contain a disjunction of unguarded
state predicates.) For instance,
$\langle\\!\langle\tau\rangle\\!\rangle(\varphi_{0}\vee\varphi_{1})$ is an
extended weak formula, as is

$\langle\\!\langle\tau\rangle\\!\rangle(((\langle\\!\langle\beta\rangle\\!\rangle\top)\wedge\varphi_{0})\vee((\langle\\!\langle\gamma\rangle\\!\rangle\top)\wedge\varphi_{1}))$

saying that it is possible to do a sequence of unobservable actions such that
either continuing with $\beta$ and satisfying $\varphi_{0}$ hold, or
continuing with $\gamma$ and satisfying $\varphi_{1}$ hold.

######  Lemma 40.

$\langle\\!\langle\tau\rangle\\!\rangle\bigvee_{i\in I}B_{i}$ is a formula iff
$\bigvee_{i\in I}\langle\\!\langle\tau\rangle\\!\rangle B_{i}$ is, and in this
case

$\langle\\!\langle\tau\rangle\\!\rangle\bigvee_{i\in
I}B_{i}\stackrel{{\scriptstyle\cdot}}{{\equiv}}\bigvee_{i\in
I}\langle\\!\langle\tau\rangle\\!\rangle B_{i}$

######  Proof 7.6.

The proof is by directly expanding definitions, noting that
$\operatorname{supp}(\\{\langle\\!\langle\tau\rangle\\!\rangle B_{i}\mid i\in
I\\})$ is equal to $\operatorname{supp}(\\{B_{i}\mid i\in I\\})$.

######  Theorem 41.

For any extended weak formula $E$ there is an (ordinary) weak formula
$\Delta(E)$ such that $E\stackrel{{\scriptstyle\cdot}}{{\equiv}}\Delta(E)$.

######  Proof 7.7.

The idea is to push disjunctions in preformulas to top level using the fact
that (finite) conjunction distributes over disjunction, and then use Lemma 40.
Say that a preformula is in normal form if it either is $A\wedge\varphi$ where
$A$ here and in the following stands for an ordinary weak formula, or is a
disjunction of normal forms. We let $C$ range over normal preformulas, thus

$C\quad::=\quad A\wedge\varphi\quad|\quad\bigvee_{i\in I}C_{i}$

The intuition is that in a normal preformula no conjunction can contain a
disjunction of preformulas.

Define a function $\delta$ from normal preformulas to (ordinary) weak formulas
by

$\begin{array}[]{l@{\hspace{0.5em}}c@{\hspace{1em}}l}\delta(A\wedge\varphi)\hfil\hskip
5.0pt&=\hfil\hskip
10.00002pt&\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\varphi)\\\\[5.0pt]
\delta(\bigvee_{i\in I}C_{i})\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\bigvee_{i\in I}\delta(C_{i})\end{array}$

By induction $\delta$ is equivariant, hence the disjunction in the above
definition is finitely supported. Moreover,
$\delta(C)\stackrel{{\scriptstyle\cdot}}{{\equiv}}\langle\\!\langle\tau\rangle\\!\rangle
C$ by Lemma 40 and induction.

Next, define a binary function $\varepsilon$ from pairs consisting of an
(ordinary) weak formula and a normal preformula, to normal preformulas, by

$\begin{array}[]{l@{\hspace{0.5em}}c@{\hspace{1em}}l}\varepsilon(A,A^{\prime}\wedge\varphi)\hfil\hskip
5.0pt&=\hfil\hskip 10.00002pt&(A\wedge A^{\prime})\wedge\varphi\\\\[5.0pt]
\varepsilon(A,\bigvee_{i\in I}C_{i})\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\bigvee_{i\in I}\varepsilon(A,C_{i})\end{array}$

Also $\varepsilon$ is equivariant, and
$\varepsilon(A,C)\stackrel{{\scriptstyle\cdot}}{{\equiv}}A\wedge C$ by
induction and distributivity of conjunction.

We now provide an explicit transformation $\Delta$ from extended weak formulas
to (ordinary) weak formulas. We also provide a transformation
$\Delta_{\mathrm{pre}}$ that maps preformulas to normal preformulas. The
transformations $\Delta$ and $\Delta_{\mathrm{pre}}$ are defined by mutual
recursion:

$\begin{array}[]{l@{\hspace{0.5em}}c@{\hspace{1em}}l}\Delta(\bigwedge_{i\in
I}E_{i})\hfil\hskip 5.0pt&=\hfil\hskip 10.00002pt&\bigwedge_{i\in
I}\Delta(E_{i})\\\\[5.0pt] \Delta(\neg E)\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\neg\Delta(E)\\\\[5.0pt]
\Delta(\langle\\!\langle\alpha\rangle\\!\rangle E)\hfil\hskip
5.0pt&=\hfil\hskip
10.00002pt&\langle\\!\langle\alpha\rangle\\!\rangle\Delta(E)\\\\[5.0pt]
\Delta(\langle\\!\langle\tau\rangle\\!\rangle B)\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\delta(\Delta_{\mathrm{pre}}(B))\\\\[10.00002pt]
\Delta_{\mathrm{pre}}(E\wedge B)\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\varepsilon(\Delta(E),\Delta_{\mathrm{pre}}(B))\\\\[5.0pt]
\Delta_{\mathrm{pre}}(\varphi)\hfil\hskip 5.0pt&=\hfil\hskip
10.00002pt&\top\wedge\varphi\\\\[5.0pt] \Delta_{\mathrm{pre}}(\bigvee_{i\in
I}B_{i})\hfil\hskip 5.0pt&=\hfil\hskip 10.00002pt&\bigvee_{i\in
I}\Delta_{\mathrm{pre}}(B_{i})\end{array}$

By simultaneous induction over extended weak formulas and preformulas it is
easy to prove that both $\Delta$ and $\Delta_{\mathrm{pre}}$ are equivariant.
Therefore, all conjunctions and disjunctions that appear on the right-hand
side in the above definition are finitely supported.

We now prove, again by simultaneous induction over extended weak formulas $E$
and preformulas $B$, that $\Delta(E)\stackrel{{\scriptstyle\cdot}}{{\equiv}}E$
and $\Delta_{\mathrm{pre}}(B)\stackrel{{\scriptstyle\cdot}}{{\equiv}}B$. The
cases $\Delta(\bigwedge_{i\in I}E_{i})$ and $\Delta(\neg E)$ and
$\Delta(\langle\\!\langle\alpha\rangle\\!\rangle E)$ are immediate by
induction. For the case $\Delta(\langle\\!\langle\tau\rangle\\!\rangle B)$ we
have

$\Delta(\langle\\!\langle\tau\rangle\\!\rangle
B)=\delta(\Delta_{\mathrm{pre}}(B))\stackrel{{\scriptstyle\cdot}}{{\equiv}}\langle\\!\langle\tau\rangle\\!\rangle\Delta_{\mathrm{pre}}(B)\stackrel{{\scriptstyle\cdot}}{{\equiv}}\langle\\!\langle\tau\rangle\\!\rangle
B$

by induction. Likewise, for the case $\Delta_{\mathrm{pre}}(E\wedge B)$ we
have

$\Delta_{\mathrm{pre}}(E\wedge
B)=\varepsilon(\Delta(E),\Delta_{\mathrm{pre}}(B))\stackrel{{\scriptstyle\cdot}}{{\equiv}}\Delta(E)\wedge\Delta_{\mathrm{pre}}(B)\stackrel{{\scriptstyle\cdot}}{{\equiv}}E\wedge
B$

by induction. The case $\Delta_{\mathrm{pre}}(\varphi)$ is trivial, and the
case $\Delta_{\mathrm{pre}}(\bigvee_{i\in I}B_{i})$ is again immediate by
induction.

##  8\. State predicates versus actions

Transition system formalisms differ in how much information is considered to
reside in states and how much is considered to reside in actions. One extreme
is Lamport’s TLA [Lam02] where all information is in the states. On the other
extreme are most process algebras such as the pi-calculus, where states
contain no information apart from the outgoing transitions. Advanced process
algebras such as psi-calculi use both state predicates and actions. Clearly,
many ways are possible and the choice is more dependent on the traditions and
modelling convenience in different areas than on hard theoretical results.

The question if state information can be encoded as actions and vice versa is
old. Already in 1989 Jonsson et al. [JKP90] provided a translation from a
labelled transition system into an (unlabelled) Kripke structure, in order to
use a model checker for CTL. With nominal transition systems it is hard to see
how such a translation could work. The actions can contain binding names and
encoding that into the states would require a substantial extension of our
definitions.

In the other direction, it has long been a folklore fact in process algebra
that a state predicate can be represented as an action on a transition leading
back to the same state. In this section we make this idea fully formal: for
the purposes of checking bisimilarity this transformation is indeed sound, and
there is a companion transformation on modal logic formulas. This is
straightforward for strong bisimulation and modal logic, and a little more
involved for weak modal formulas.

###  8.1. Strong bisimulation and logic

Our idea is that for any transition system $\mathbf{T}$ there is another
transition system ${\mathcal{S}(\mathbf{T})}$ where state predicates are
replaced by self-loops. To formulate this idea we again use the notation
$\mbox{\sc states}_{\mathbf{T}}$ to mean the states in the transition system
$\mathbf{T}$, and similarly for actions, $\operatorname{bn}$, transitions,
bisimilarity, etc.

The function $\mathcal{S}$ from transition systems to transition systems is
defined as follows:

  * •

$\mbox{\sc states}_{\mathcal{S}(\mathbf{T})}=\mbox{\sc states}_{\mathbf{T}}$

  * •

$\mbox{\sc act}_{\mathcal{S}(\mathbf{T})}=\mbox{\sc
act}_{\mathbf{T}}\uplus\mbox{\sc pred}_{\mathbf{T}}$

  * •

$\operatorname{bn}_{\mathcal{S}(\mathbf{T})}(\alpha)=\operatorname{bn}_{\mathbf{T}}(\alpha)$
if $\alpha\in\mbox{\sc act}_{\mathbf{T}}$;
$\operatorname{bn}_{\mathcal{S}(\mathbf{T})}(\varphi)=\emptyset$ if
$\varphi\in\mbox{\sc pred}_{\mathbf{T}}$

  * •

$\mbox{\sc
pred}_{\mathcal{S}(\mathbf{T})}=\;\vdash_{\mathcal{S}(\mathbf{T})}\;=\emptyset$

  * •

$P\xrightarrow{\alpha}_{\mathcal{S}(\mathbf{T})}P^{\prime}$ if
$P\xrightarrow{\alpha}_{\mathbf{T}}P^{\prime}$ (for $\alpha\in\mbox{\sc
act}_{\mathbf{T}}$); $P\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}P$ if
$P\vdash_{\mathbf{T}}\varphi$ (for $\varphi\in\mbox{\sc pred}_{\mathbf{T}}$)

It is easy to see that if $\mathbf{T}$ is a transition system then so is
${\mathcal{S}(\mathbf{T})}$. In particular equivariance of
$\rightarrow_{\mathcal{S}(\mathbf{T})}$ follows from equivariance of
$\rightarrow_{\mathbf{T}}$ and $\vdash_{\mathbf{T}}$ and the fact that the
union of equivariant relations is equivariant.222Nominal Isabelle does not
admit empty types. Therefore, the type $\mbox{\sc
pred}_{\mathcal{S}(\mathbf{T})}$ is given by the unit type in our Isabelle
formalisation. We still define $\vdash_{\mathcal{S}(\mathbf{T})}$ to be false
everywhere, so that this minor difference has no further significance.

######  Theorem 42.

$P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathbf{T}}Q\ \implies\
P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathcal{S}(\mathbf{T})}Q$

######  Proof 8.1.

The proof has been formalised in Isabelle. We show that
$\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathbf{T}}$ is a
${\mathcal{S}(\mathbf{T})}$-bisimulation. Obviously it is symmetric. Static
implication is trivial since $\vdash_{\mathcal{S}(\mathbf{T})}$ is false
everywhere. For simulation, assume
$P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathbf{T}}Q$ and that $P$ has a
transition in ${\mathcal{S}(\mathbf{T})}$. If the transition has an action in
$\mathbf{T}$, then $P$ has the same transition in $\mathbf{T}$. If the action
is a state predicate in $\mathbf{T}$ then the transition must be
$P\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}P$ where
$P\vdash_{\mathbf{T}}\varphi$, hence by static implication
$Q\vdash_{\mathbf{T}}\varphi$, thus also
$Q\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}Q$. In both cases we
therefore have a simulating transition from $Q$ in
${\mathcal{S}(\mathbf{T})}$.

######  Theorem 43.

$P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathcal{S}(\mathbf{T})}Q\ \implies\
P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathbf{T}}Q$

######  Proof 8.2.

The proof has been formalised in Isabelle. We show that
$\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathcal{S}(\mathbf{T})}$ is a
$\mathbf{T}$-bisimulation. Obviously it is symmetric. Assume
$P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathcal{S}(\mathbf{T})}Q$. For
static implication, if $P\vdash_{\mathbf{T}}\varphi$ then $P$ has a transition
with action $\varphi$ in ${\mathcal{S}(\mathbf{T})}$, thus $Q$ has a
transition with the same action, hence $Q\vdash_{\mathbf{T}}\varphi$. For
simulation, any transition in $\mathbf{T}$ is also a transition in
${\mathcal{S}(\mathbf{T})}$.

Modal logic formulas over ${\mathcal{S}(\mathbf{T})}$ use predicates as
actions. We extend $\mathcal{S}$ to formulas as follows. The function
$\mathcal{S}$ from formulas over the transition system $\mathbf{T}$ to
formulas over the transition system ${\mathcal{S}(\mathbf{T})}$ is defined by

$\mathcal{S}(\varphi)=\langle{}\varphi\rangle\top$

and is homomorphic on the other cases in Definition 3.1.

######  Theorem 44.

$P\models_{\mathbf{T}}A\quad\mbox{iff}\quad
P\models_{\mathcal{S}(\mathbf{T})}\mathcal{S}(A)$

######  Proof 8.3.

The proof has been formalised in Isabelle. It is by induction over formulas
$A$, for arbitrary $P$. If $A=\varphi$ then clearly
$P\models_{\mathbf{T}}\varphi$ iff
$P\models_{\mathcal{S}(\mathbf{T})}\langle{}\varphi\rangle\top$. For the case
$A=\langle{}\alpha\rangle A^{\prime}$ we assume without loss of generality
$\operatorname{bn}(\alpha)\\#P$, otherwise just find an alpha-variant where
this holds. This and the other cases are then immediate by induction.

This provides an alternative proof of Theorem 43. If
$P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathcal{S}(\mathbf{T})}Q$ then by
Theorem 3 for any $A$ it holds that $P\models\mathcal{S}(A)$ iff
$Q\models\mathcal{S}(A)$, and thus $P\models A$ iff $Q\models A$, therefore by
Theorem 5 $P\stackrel{{\scriptstyle\cdot}}{{\sim}}_{\mathbf{T}}Q$. The
converse does not follow since $\mathcal{S}$ is not surjective on formulas.

###  8.2. Weak bisimulation

For weak bisimulation the corresponding proofs are only a little bit more
complicated.

######  Theorem 45.

$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q\ \implies\
P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q$

######  Proof 8.4.

The proof has been formalised in Isabelle. We show that
$\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}$ is a weak
${\mathcal{S}(\mathbf{T})}$-bisimulation. Obviously it is symmetric. Weak
static implication is trivial since $\vdash_{\mathcal{S}(\mathbf{T})}$ is
false everywhere. For weak simulation, assume
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q$. There are two
cases.

  1. (1)

$P\xrightarrow{\alpha}_{\mathcal{S}(\mathbf{T})}P^{\prime}$ where
$\alpha\in\mbox{\sc act}_{\mathbf{T}}$. Then
$P\xrightarrow{\alpha}_{\mathbf{T}}P^{\prime}$ and by
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q$ we get
$Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}_{\mathbf{T}}Q^{\prime}$,
which implies
$Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$,
with
$P^{\prime}\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q^{\prime}$.

  2. (2)

$P\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}P$ where $\varphi\in\mbox{\sc
pred}_{\mathbf{T}}$ and $P\vdash_{\mathbf{T}}\varphi$. By weak static
implication $Q\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}Q^{\prime}$
and $Q^{\prime}\vdash_{\mathbf{T}}\varphi$ and
$Q^{\prime}\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}P$. Thus
$Q\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$
and $Q^{\prime}\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$,
hence
$Q\stackrel{{\scriptstyle\hat{\varphi}}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$.

The converse uses the following lemma, which is familiar in many process
algebras and interesting in its own right.

######  Lemma 46.

If
$P\stackrel{{\scriptstyle}}{{\Rightarrow}}Q\stackrel{{\scriptstyle}}{{\Rightarrow}}R$
and $P\stackrel{{\scriptstyle\cdot}}{{\approx}}R$ then
$Q\stackrel{{\scriptstyle\cdot}}{{\approx}}R$.

######  Proof 8.5.

The proof has been formalised in Isabelle. We establish that
$\\{(Q,R),(R,Q)\\}\;\cup\stackrel{{\scriptstyle\cdot}}{{\approx}}$ is a weak
bisimulation. Obviously it is symmetric.

For weak static implication, clearly if $R\vdash\varphi$ then
$Q\stackrel{{\scriptstyle}}{{\Rightarrow}}R\vdash\varphi$; and if
$Q\vdash\varphi$ then
$P\stackrel{{\scriptstyle}}{{\Rightarrow}}Q\vdash\varphi$, so by
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}R$, Lemma 30, and weak static
implication we obtain $R^{\prime}$ with
$R\stackrel{{\scriptstyle}}{{\Rightarrow}}R^{\prime}\vdash\varphi$ as
required.

For weak simulation, clearly if $R\xrightarrow{\alpha}R^{\prime}$ then
$Q\stackrel{{\scriptstyle}}{{\Rightarrow}}R\xrightarrow{\alpha}R^{\prime}$,
hence $Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}R^{\prime}$ (and
obviously $R^{\prime}\stackrel{{\scriptstyle\cdot}}{{\approx}}R^{\prime}$);
and if $Q\xrightarrow{\alpha}Q^{\prime}$ then
$P\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}Q^{\prime}$, so again by
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}R$ and Lemma 30 we obtain
$R^{\prime}$ with
$R\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}R^{\prime}$ and
$Q^{\prime}\stackrel{{\scriptstyle\cdot}}{{\approx}}R^{\prime}$.

######  Theorem 47.

$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q\
\implies\ P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q$

######  Proof 8.6.

The proof has been formalised in Isabelle. We show that
$\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}$ is a
weak $\mathbf{T}$-bisimulation. Obviously it is symmetric.

For weak static implication, assume
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q$ and
$P\vdash_{\mathbf{T}}\varphi$. Thus
$P\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}P$. By weak simulation we
obtain $Q^{\prime}$ with
$Q\stackrel{{\scriptstyle\hat{\varphi}}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$
and
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$.
By construction of ${\mathcal{S}(\mathbf{T})}$ this means that there is a
$Q^{\prime\prime}$ such that
$Q\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime\prime}\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}Q^{\prime\prime}\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}{Q^{\prime}}$.
Thus $Q\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}Q^{\prime\prime}$
and $Q^{\prime\prime}\vdash_{\mathbf{T}}\varphi$. Moreover, by applying Lemma
46 to
$Q\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime\prime}\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}{Q^{\prime}}$
and
$Q\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$
we get
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q^{\prime\prime}$
as required.

For weak simulation, assume
$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q$ and
$P\xrightarrow{\alpha}_{\mathbf{T}}P^{\prime}$. This implies
$P\xrightarrow{\alpha}_{\mathcal{S}(\mathbf{T})}P^{\prime}$, and thus by weak
simulation
$Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$,
which implies
$Q\stackrel{{\scriptstyle\hat{\alpha}}}{{\Rightarrow}}_{\mathbf{T}}Q^{\prime}$,
with
$P^{\prime}\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q^{\prime}$
as required.

###  8.3. Weak logic

For the weak logic, the correspondence between state predicates and actions is
less obvious, and there appear to be more than one alternative. The
transformation $\mathcal{S}$ of formulas does not preserve the property of
being a weak formula since

$\mathcal{S}(\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\varphi))=\langle\\!\langle\tau\rangle\\!\rangle(\mathcal{S}(A)\wedge\langle{}\varphi\rangle\top)$

and the subformula $\langle{}\varphi\rangle\top$ is not weak. For the
transition system ${\mathcal{S}(\mathbf{T})}$ we thus get an alternative logic
adequate for weak bisimilarity by taking the formulas
$\\{\mathcal{S}(A)\mid\mbox{$A$ is a weak formula}\\}$, i.e., with the last
clause of Definition 32 replaced by formulas of kind
$\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\langle{}\varphi\rangle\top)$.

######  Corollary 48.

$P\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q$ iff
for all weak formulas $A$: $P\models_{\mathcal{S}(\mathbf{T})}\mathcal{S}(A)$
iff $Q\models_{\mathcal{S}(\mathbf{T})}\mathcal{S}(A)$

######  Proof 8.7.

The proof has been formalised in Isabelle. It is immediate by Theorems 33, 35
and 44–47.

For this corollary to hold it is critical that the transition system is an
image of $\mathcal{S}$, i.e., that the transitions involving actions $\varphi$
only occur in loops. If this is not the case, there may be formulas in the
image of $\mathcal{S}$ that can distinguish between weakly bisimilar states.
An example is the following:

Here $P$ and $Q$ are weakly bisimilar. Let $A$ be the weak formula
$\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\alpha\rangle\\!\rangle\top\wedge\varphi)$.
Then
$\mathcal{S}(A)=\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\alpha\rangle\\!\rangle\top\wedge\langle{}\varphi\rangle\top)$,
and $P\models\mathcal{S}(A)$ but not $Q\models\mathcal{S}(A)$.

Ideally, we would want an alternative transformation onto weak formulas, but
it seems difficult to formulate this in a succinct way. Through expressive
completeness (Section 7.3) we get the following:

######  Theorem 49.

Let $A$ be a weak formula over $\mathbf{T}$. Then there exists a weak formula
$A^{\prime}$ over ${\mathcal{S}(\mathbf{T})}$ such that

$P\models_{\mathbf{T}}A\quad\mbox{iff}\quad
P\models_{\mathcal{S}(\mathbf{T})}A^{\prime}$

for all states $P$.

######  Proof 8.8.

The proof has been formalised in Isabelle. Note that $\\{Q\mid
Q\models_{\mathbf{T}}A\\}$ is finitely supported (with support included in
$\operatorname{supp}(A)$), and moreover closed under
$\mathop{\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}}$
by Theorems 33 and 47. It then follows from Theorem 39 that
$A^{\prime}=\bigvee_{Q\models_{\mathbf{T}}A}\mathrm{Char}(Q)$ has the desired
properties.

Inherent in this proof is a construction of the weak formula $A^{\prime}$ from
the weak formula $A$, but the construction depends implicitly on
distinguishing formulas (cf. Theorem 5) and thus on the entire transition
system.

We have failed to find a transformation of weak formulas that yields
equivalent weak formulas over ${\mathcal{S}(\mathbf{T})}$ and is defined by
induction over formulas, or, at the very least, is independent of the
transition system. We have also failed to prove that such a transformation
cannot exist, and thus have to leave this problem open. The following
counterexamples shed light on the difficulties:

#### Counterexample

Define the transformation $\mathcal{S}$ on weak formulas by

$\mathcal{S}(\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\varphi))=\langle\\!\langle\varphi\rangle\\!\rangle\mathcal{S}(A)$

With this definition, the counterpart of Theorem 44 fails. A counterexample is
$A=\neg\langle\\!\langle\alpha\rangle\\!\rangle\top$,
$P\vdash_{\mathbf{T}}{\varphi}$ with $P\xrightarrow{\tau}_{\mathbf{T}}Q$ and
$P\xrightarrow{\alpha}_{\mathbf{T}}Q$ for some $\alpha\neq\tau$, where $Q$ has
no outgoing transitions, cf. the diagrams below:

Since
$P\stackrel{{\scriptstyle\varphi}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q$
and $Q$ has no $\langle\\!\langle\alpha\rangle\\!\rangle$ action, we have that

$P\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,\langle\\!\langle\varphi\rangle\\!\rangle\neg\langle\\!\langle\alpha\rangle\\!\rangle\top$

The only state in T that satisfies $\varphi$ also has an
$\langle\\!\langle\alpha\rangle\\!\rangle$ action, thus it does not hold that

$P\nobreak\,\models_{\mathbf{T}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle(\neg\langle\\!\langle\alpha\rangle\\!\rangle\top\wedge\varphi)$

#### Counterexample

Define the transformation $\mathcal{S}$ on weak formulas by

$\mathcal{S}(\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\varphi))=\langle\\!\langle\tau\rangle\\!\rangle(\mathcal{S}(A)\wedge\langle\\!\langle\varphi\rangle\\!\rangle\top)$

Then again the counterpart of Theorem 44 fails. A counterexample here is
$A=\langle\\!\langle\alpha\rangle\\!\rangle\top$, with
$P\xrightarrow{\tau}_{\mathbf{T}}Q$ and $Q\vdash_{\mathbf{T}}{\varphi}$,
$P\xrightarrow{\alpha}_{\mathbf{T}}Q$ for some $\alpha\neq\tau$, cf. the
diagrams below:

Here it holds that

$P\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\alpha\rangle\\!\rangle\top\wedge\langle\\!\langle\varphi\rangle\\!\rangle\top)$

and it does not hold that

$P\nobreak\,\models_{\mathbf{T}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\alpha\rangle\\!\rangle\top\wedge\varphi)$

Finally, consider the partial transformation $\mathcal{S}^{\prime}$ on weak
formulas by

$\mathcal{S}^{\prime}(\langle\\!\langle\tau\rangle\\!\rangle((\langle\\!\langle\tau\rangle\\!\rangle
A)\wedge\varphi))=\langle\\!\langle\varphi\rangle\\!\rangle\mathcal{S}^{\prime}(A)$

where $\mathcal{S}^{\prime}$ is homomorphic on the first three cases in
Definition 32.

$\mathcal{S}^{\prime}$ is not total since a formula
$\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\varphi)$ is in its domain only
when $A=\langle\\!\langle\tau\rangle\\!\rangle A^{\prime}$ for some
$A^{\prime}$. It is easy to see that $\mathcal{S}^{\prime}$ is injective and
surjective, i.e., every weak formula $A$ on ${\mathcal{S}(\mathbf{T})}$ has a
unique formula $B$ on $\mathbf{T}$ such that $\mathcal{S}^{\prime}(B)=A$. We
write $\mathcal{S}^{\prime-1}$ for the inverse of $\mathcal{S}^{\prime}$. Thus

$\mathcal{S}^{\prime-1}(\langle\\!\langle\varphi\rangle\\!\rangle
A)=\langle\\!\langle\tau\rangle\\!\rangle((\langle\\!\langle\tau\rangle\\!\rangle\mathcal{S}^{\prime-1}(A))\wedge\varphi)$

and $\mathcal{S}^{\prime-1}$ is homomorphic on all other operators.

######  Theorem 50.

$P\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,A\quad\mbox{iff}\quad
P\nobreak\,\models_{\mathbf{T}}\nobreak\,\mathcal{S}^{\prime-1}(A)$

######  Proof 8.9.

By induction over weak formulas on ${\mathcal{S}(\mathbf{T})}$. All cases are
trivial by induction except for the case
$\langle\\!\langle\varphi\rangle\\!\rangle A$ with $\varphi\in\mbox{\sc
pred}_{\mathbf{T}}$. Suppose
$P\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,\langle\\!\langle\varphi\rangle\\!\rangle
A$. Then
$P\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}P^{\prime}\xrightarrow{\varphi}_{\mathcal{S}(\mathbf{T})}P^{\prime\prime}\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathcal{S}(\mathbf{T})}Q$
with $Q\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,A$. By
construction of ${\mathcal{S}(\mathbf{T})}$ we get
$P^{\prime}=P^{\prime\prime}$, and
$P\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}P^{\prime}\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}Q$
with $P^{\prime}\vdash_{\mathbf{T}}\varphi$. By induction
$Q\nobreak\,\models_{\mathbf{T}}\nobreak\,\mathcal{S}^{\prime-1}(A)$. This
establishes that
$P^{\prime}\nobreak\,\models_{\mathbf{T}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle\mathcal{S}^{\prime-1}(A)\wedge\varphi$
and thus
$P\nobreak\,\models_{\mathbf{T}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\tau\rangle\\!\rangle\mathcal{S}^{\prime-1}(A)\wedge\varphi)$
as required. Conversely, if
$P\nobreak\,\models_{\mathbf{T}}\nobreak\,\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\tau\rangle\\!\rangle\mathcal{S}^{\prime-1}A\wedge\varphi)$
then
$P\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}P^{\prime}\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\mathbf{T}}Q$,
and by construction of ${\mathcal{S}(\mathbf{T})}$ and induction we get
$P\nobreak\,\models_{{\mathcal{S}(\mathbf{T})}}\nobreak\,\langle\\!\langle\varphi\rangle\\!\rangle
A$.

An interesting consequence is that to express the distinguishing formulas
guaranteed by Theorem 35, it is enough to consider formulas in
$\mbox{dom}(\mathcal{S}^{\prime})$, i.e., in the last clause of Definition 32,
it is enough to consider $A=\langle\\!\langle\tau\rangle\\!\rangle
A^{\prime}$. The reason is that if
$P\not\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathbf{T}}Q$ then by Theorem
47 also
$P\not\stackrel{{\scriptstyle\cdot}}{{\approx}}_{\mathcal{S}(\mathbf{T})}Q$,
which by Theorem 35 means there is a distinguishing formula $B$ for $P$ and
$Q$ in ${\mathcal{S}(\mathbf{T})}$, which by Theorem 50 means that
$\mathcal{S}^{\prime-1}(B)$ is a distinguishing formula in $\mathbf{T}$.

In conclusion, the results in this section show that the transformation
$\mathcal{S}$ indicates an alternative weak logic with formulas
$\langle\\!\langle\tau\rangle\\!\rangle(A\wedge\langle{}\varphi\rangle\top)$,
which is appropriate if $\varphi$ only occurs in self-loops. The
transformation $\mathcal{S}^{\prime}$, on the other hand, indicates that a
sublogic with formulas
$\langle\\!\langle\tau\rangle\\!\rangle(\langle\\!\langle\tau\rangle\\!\rangle
A\wedge\varphi)$ is expressively equivalent. It admits a smooth transformation
of predicates into actions at the cost of a more complicated definition of a
weak logic.

Through expressive completeness we obtain a transformation on our original
weak logic, but it does not really shed light on the nature of state
predicates and actions. Certainly, it means that any impossibility result for
a transformation onto weak formulas must be qualified with a notion of
independence from the transition system. This would require a proper
definition of the set of transition systems that act as models for a given
logic. One difficulty here is that the disjoint union of a set of transition
systems is itself a transition system. By expressive completeness we get a
transformation (dependent on this union); that same transformation thus
applies to all the members in the set. Consider the set of all transition
systems of cardinality at most $\kappa$; this set may have a cardinality
higher than $\kappa$. Thus an impossibility result may actually depend on the
cardinality limit in Definition 3.1.

##  9\. Applications

In this section we consider standard process calculi and their accompanying
labelled bisimilarities, and investigate how to obtain an adequate modal logic
using our framework. In each of the final two examples, no HML has to our
knowledge yet been proposed, and we immediately obtain one by instantiating
the logic in the present paper.

Pi-calculus. The pi-calculus by Milner et al. [MPW92] has a labelled
transition system with early input, defined using a structural operational
semantics. This transition system satisfies the axioms of a nominal transition
system, and the logic of Section 3 (with an empty set of state predicates) is
adequate for early bisimilarity. Other variants of bisimilarity can be
obtained by instead using the original transition system (with late input) and
one of the variants of our logic described in Section 6.

The pi-calculus already has several notions of weak bisimulation, and
Definition 7.1 corresponds to the early weak bisimulation. In the pi-calculus
there are no state predicates, thus the weak static implication is
unimportant. The weak logic of Definition 32 is adequate for early weak
bisimulation.

Applied pi-calculus. The applied pi-calculus by Abadi and Fournet (2001)
[AF01] comes equipped with a labelled transition system and a notion of weak
labelled bisimulation. States contain a record of emitted messages; this
record has a domain and can be used to equate open terms $M$ and $N$ modulo
some rewrite system. The definition of bisimulation requires bisimilar
processes to have the same domain and equate the same open terms, i.e., to be
strongly statically equivalent. We model these requirements using state
predicates “$x\in\operatorname{dom}$” and “$M\equiv N$”. Since satisfaction is
invariant under silent transitions, weak and strong static implication
coincide, and our weak HML is adequate for Abadi and Fournet’s early weak
labelled bisimilarity.

Spi-calculus. The spi-calculus by Abadi and Gordon (1999) [AG99] has a
formulation as an environment-sensitive labelled transition system by Boreale
et al. (2001) [BDNP01] equipped with state formulae (predicates) $\phi$.
Adding state predicates “$x\in\operatorname{dom}$” to the state predicates
makes our weak HML adequate with respect to Boreale’s early weak bisimilarity.

Concurrent constraint pi calculus. The concurrent constraint pi calculus (CC-
pi) by Buscemi and Montanari (2007) [BM07] extends the explicit fusion
calculus [WG05] with a more general notion of constraint stores $c$. Using the
labelled transition system of CC-pi and the associated bisimulation
(Definition 3.1), we immediately get an adequate modal logic.

The reference equivalence for CC-pi is open bisimulation [BM08] (closely
corresponding to hyperbisimulation in the fusion calculus [PV98]), 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\xrightarrow{\alpha}P^{\prime}$, the simulating process $Q$ can
use any transition $Q\xrightarrow{\beta}Q^{\prime}$ with an equivalent label,
as given by a state predicate $\alpha=\beta$. As an example, if
$\alpha=\overline{a}\langle{x}\rangle$ is a free output label then
$P\vdash\alpha=\beta$ iff $\beta=\overline{b}\langle{y}\rangle$ where $P\vdash
a=b$ and $P\vdash x=y$. To encode this, we transform the labels of the
transition system by replacing them with their equivalence classes, i.e.,
$P\xrightarrow{\alpha}P^{\prime}$ becomes
$P\xrightarrow{[\alpha]_{P}}P^{\prime}$ where $\beta\in[\alpha]_{P}$ iff
$P\vdash\beta=\alpha$. Hyperbisimilarity (Definition 6.1) on this transition
system then corresponds to open bisimilarity, and the modal logic defined in
Section 6 is adequate.

Psi-calculi. In psi-calculi by Bengtson et al. (2011) [BJPV11], the labelled
transitions take the form
$\Psi\mathrel{\triangleright}P\xrightarrow{\alpha}P^{\prime}$, where the
assertion environment $\Psi$ is unchanged after the step. We model this as a
nominal transition system by letting the set of states be pairs $(\Psi,P)$ of
assertion environments and processes, and define the transition relation by
$(\Psi,P)\xrightarrow{\alpha}(\Psi,P^{\prime})$if
$\Psi\mathrel{\triangleright}P\xrightarrow{\alpha}P^{\prime}$. 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
$\Psi\mathrel{\triangleright}P\sim Q$, then
$\Psi\otimes\Psi^{\prime}\mathrel{\triangleright}P\sim Q$ for all
$\Psi^{\prime}$. We let the effects $\mathcal{F}$ be the set of assertions,
anddefine $\Psi((\Psi^{\prime},P))=(\Psi\otimes\Psi^{\prime},P)$.
Hyperbisimilarity on this transition system then subsumes the standard psi-
calculi bisimilarity, and the modal logic defined in Section 6 is adequate.

Weak bisimilarity for CC-pi and psi. Both CC-pi and psi-calculi has a special
unobservable action $\tau$, but until now only psi-calculi have a notion of
weak labelled bisimulation (as remarked in Section 7.1), and neither has a
weak HML. Through this paper they both gain both weak bisimulation and logic,
although more work is needed to establish how compatible the bisimulation
equivalence is with their respective syntactic constructs. A complication is
that the natural formulation of bisimulation makes use of effects (store or
assertion extensions) which are bisimulation requirements on neither
predicates nor actions. In order to map them into our framework these would
need to be cast as actions. Their interactions with the silent action could be
an interesting topic for further research.

##  10\. Related work

We here 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: formal correspondence
fails to hold due to differences in the conjunction operator of the logic
(finite, uniformly bounded or unbounded vs. bounded support).

HML for CCS. The first published HML is Hennessy and Milner (1980–1985) [HM80,
Mil81, HM85]. They work with image-finite CCS processes, where finite (binary)
conjunction suffices for adequacy, and define both strong and weak versions of
the logic. The logic by Hennessy and Liu (1995) [HL95] for a value-passing
calculus also uses binary conjunction, 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) [CMS02],
though that paper only considers stratified bisimilarity up to $\omega$.

Hennessy and Liu’s value-passing calculus is based on ordinary CCS. In this
calculus, a receiving process $a(x).P$ can participate in a synchronisation on
$a$, becoming an abstraction $(x)P$ where $v$ is a bound variable. Dually, a
sending process $\overline{a}\,v.Q$ becomes a concretion $(v,Q)$ where $v$ is
a value. The abstraction and concretion above react as part of the
synchronisation on $a$, yielding $P\\{{}^{v}\\!/\\!{}_{x}\\}\mid Q$. To
capture the operations of abstractions and concretions in our framework, we
add effects id and $?v$, with $?v((x)P)=P\\{{}^{v}\\!/\\!{}_{x}\\}$, and
transitions $(v,P)\xrightarrow{!v}P$. Letting $L(a?,\\_)=\\{?v\mid
v\in\text{values}\\}$ and $L(\alpha,\\_)=\\{\mbox{\tt id}\\}$ otherwise, late
bisimilarity is $\\{\mbox{\tt id}\\}/L$-bisimilarity as defined in Section 6.
We can then encode their universal quantifier $\forall x.A$ as
$\bigwedge_{v}\langle{}?v\rangle A\\{{}^{v}\\!/\\!{}_{x}\\}$, which has
support $\operatorname{supp}(A)\setminus\\{x\\}$, and their output modality
$\langle{}c!x\rangle A$ as $\langle{}c!\rangle\bigvee_{v}\langle{}!v\rangle
A\\{{}^{v}\\!/\\!{}_{x}\\}$, with support
$\\{c\\}\cup(\operatorname{supp}(A)\setminus\\{x\\})$.

An infinitary HML for CCS is discussed in Milner’s book (1989) [Mil89], 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 5, though without any
consideration of finite support. A more rigorous treatment of the same ideas
is by Abramsky (1991) [Abr91] where uniformly bounded conjunction is used
throughout.

Koutavas et al. (2018) [KGH18] study a transactional CCS, extending the
natural transition system in order to provide three equivalent adequate HMLs.
Neither processes nor actions contain bound names, which is a stark difference
from the problem treated in the present paper. Formulas contain countably
infinite conjunction and thus may contain an infinite number of variable
names, which are “interpreted nominally”. The paper does not define alpha-
equivalence for formulas, and states that variable instantiation ”does not
require any notion of alpha-equivalence, as in [PBE+15]”. In order to find a
fresh variable name, the adequacy proof instead uses an unspecified notion of
renaming (Prop. 4.5).

Simpson (2004) [Sim04] gives a sequent calculus for proving HML properties of
process calculi in GSOS format, using binary conjunction and assuming finite
branching and a finite number of actions.

$\mu$-calculus. Kozen’s modal $\mu$-calculus (1983) [Koz83] subsumes several
other weak temporal logics including CTL* (Cranen et al. 2011) [CGR11], and
can encode weak transitions using least fixed points. Dam (1996) [Dam96] gives
a modal $\mu$-calculus for the pi-calculus, treating bound names using
abstractions and concretions, and provides a model checking algorithm.
Bradford and Stevens (1999) [BS99] give a generic framework for parameterising
the $\mu$-calculus on data environments, state predicates, and action
expressions. The logic defined in the present paper can encode the least
fixpoint operator of $\mu$-calculi by a disjunction of its finite unrollings,
as seen in Section 5.2. We can immediately encode the atomic $\mu$-calculus by
Klin and Łełyk (2017) [KL17].

Pi-calculus. The first HML for the pi-calculus is by Milner et al. (1993)
[MPW93], where infinite conjunction is used in the early semantics and
conjunctions are restricted to use a finite set of free names. The adequacy
proof has the same structure as in this paper. The logic of Section 3, applied
to the pi-calculus transition system from which bound input actions $x(y)$
have been removed, contains the logic $\mathcal{F}$ of Milner et al., or the
equipotent logic $\mathcal{FM}$ if we take the set of name matchings $[a=b]$
as state predicates. Gabbay [Gab03] gives the first nominal syntax and
operational semantics for the pi-calculus, in Fraenkel-Mostowski set theory.

Koutavas and Hennessy (2012) [KH12] give a weak HML for a higher-order pi-
calculus with both higher-order and first-order communication using an
environment-sensitive LTS. Xu and Long (2015) [XL15] define a weak HML with
countable conjunction for a purely higher-order pi-calculus. The adequacy
proof uses stratification.

Ahn et al. (2017)[AHT17] give an innovative intuitionistic logic
characterising open bisimilarity. In their setting, substitution effects are
only employed inside the definition of the logical implication operator. Their
soundness proof is standard; for the completeness proof the distinguishing
formula for $P$ wrt. $Q$ is constructed in parallel with one for $Q$ wrt. $P$.

There are several extensions of HML with spatial modalities. The one most
closely related to our logic is by Berger et al. (2008) [BHY08]. They define
an HML with both strong and weak action modalities, fixpoints, spatial
conjunction and adjunction, and a scope extrusion modality, to study a typed
value-passing pi-calculus with selection and recursion. The logic has three
(may, must, and mixed) proof systems that are sound and relatively complete.

Spi Calculus. Frendrup et al. (2002) [FHNJ02] provide three Hennessy-Milner
logics for the spi calculus [AG99]. All three logics use infinite
quantification without any consideration of finite support. The transition
system used is a variant of the one by Boreale et al. (2001) [BDNP01], where a
state is a pair $\sigma\mathrel{\triangleright}P$ of a process $P$ and its
environment $\sigma$: a substitution that maps environment variables to public
names and messages received from the process. This version of the spi calculus
has expressions $\xi$, that are terms constructed from names and environment
variables using encryption and decryption operators, and messages $M$, that
only contain names and encryption. Substitution $\xi\sigma$ replaces
environment variables in $\xi$ with their values in $\sigma$, and evaluation
$\mathbf{e}(\xi)$ is a partial function that attempts to perform the
decryptions in $\xi$, yielding a message $M$ if all decryptions are
successful.

As usual for the spi calculus, the bisimulation (and logic) is defined in
terms of the environment actions, rather than the process actions. In
Frendrup’s version of Boreale’s environment-sensitive transition system, the
transition labels are related to the process actions in the following way:
when a process $P$ receives message $M$ on channel $a$, the label of a
corresponding environment-sensitive transition
$\sigma\mathrel{\triangleright}P\xrightarrow{a\,\xi}\sigma^{\prime}\mathrel{\triangleright}P^{\prime}$
describes how the environment $\sigma$ computed the message
$M=\mathbf{e}(\xi\sigma)$. For process output of message $M$ on channel $a$,
the corresponding environment-sensitive transition is simply
$\sigma\mathrel{\triangleright}P\xrightarrow{\overline{a}}\sigma^{\prime}\mathrel{\triangleright}P^{\prime}$;
the message $M$ can be recovered from the updated environment
$\sigma^{\prime}$.

The logics of Frendrup et al. include a matching modality $[M=N]A$ that is
defined using implication: $\sigma\mathrel{\triangleright}P\models[M=N]A$ iff
$\mathbf{e}(M\sigma)=\mathbf{e}(N\sigma)$ implies
$\sigma\mathrel{\triangleright}P\models A$. This is equipotent to having
matching as a state predicate, since we can rewrite all non-trivial guards by
$[M=N]A\iff A\lor\neg[M=N]\top$.

The logic of Section 3, applied to the nominal transition system with the
environment labels $\tau$, $\overline{a}$ and $a\,\xi$ above has the same
modalities as the logic $\mathcal{F}$ of Frendrup et al.

The logic $\mathcal{EM}$ by Frendrup et al. replaces the simple input modality
by an early input modality $\langle{}\underline{a}\,(x)\rangle^{E}A$, which
(after a minor manipulation of the input labels) can be encoded as the
conjunction $\bigwedge_{\xi}\langle{}{a}\,\xi\rangle
A\\{{}^{\xi}\\!/\\!{}_{x}\\}$ with support
$\operatorname{supp}(A)\setminus\\{x\\}$. We do not consider their logic
$\mathcal{LM}$ that uses a late input modality, since its application relies
on sets that do not have finite support [FHNJ02, Theorem 6.12], which are not
meaningful in nominal logic.

Frendrup et al. claim to “characterize early and late versions of the
environment sensitive bisimilarity of [BDNP01]”, but this claim only holds
with some modification. First the definition of static equivalence [FNJ01,
Definition 22] that is used in the adequacy proofs is strictly stronger than
the one that appears in the published paper [FHNJ02, Definition 3.4]. Thus,
the adequacy results [FHNJ02, Theorems 6.3, 6.4, and 6.14] are false as
stated, but can be repaired by substituting the stronger notion of static
equivalence. Then Frendrup’s logics and bisimilarities become sound, but not
complete, with respect to the bisimilarity of [BDNP01], since the latter uses
the weaker notion of static equivalence (Definition 3.4). In Section 9 we
sketched an instance of our logic, for Boreale’s labelled transition system,
that is adequate for early bisimilarity.

Applied Pi-calculus. A more recent work is a weak HML by Hüttel and Pedersen
(2007) [HP07] for the applied pi-calculus by Abadi and Fournet (2001) [AF01],
where completeness relies on an assumption of image-finiteness of the weak
transitions. Similarly to the spi calculus, there is a requirement that terms
$M$ received by a process $P$ can be computed from the current knowledge
available to an observer of the process, which we here write
$M\in\mathcal{S}(P)$.

The logic contains atomic formulae for term equality (indistinguishability) in
the frame of a process, corresponding to our state predicates. However, Hüttel
and Pedersen use a notion of equality (and thus static equivalence) that is
stronger than the corresponding relation by Abadi and Fournet, and that is
_not_ well-defined modulo alpha-renaming [Ped06, p. 20]. Since our framework
is based on nominal sets, we must identify alpha-equivalent processes, and
instead use Abadi and Fournet’s notion of term equality.

Hüttel and Pedersen’s logic includes an early input modality and an
existential quantifier. The early input modality
$\langle{}\underline{a}\,(x)\rangle A$ can be straightforwardly encoded as the
conjunction $\bigwedge_{M}\langle{}\underline{a}\,M\rangle
A\\{{}^{M}\\!/\\!{}_{x}\\}$, with support
$\\{a\\}\cup(\operatorname{supp}(A)\setminus\\{x\\})$. The definition of the
existential quantifier takes the observer knowledge into account: $P$
satisfies $\exists x.A$ if $x\\#P$ and there is $M\in\mathcal{S}(P)$ such that
$\\{{}^{M}\\!/\\!{}_{x}\\}\mid P$ satisfies $A$. The condition
$M\in\mathcal{S}(P)$ makes the quantifier difficult to encode using effects,
since there is no corresponding state predicate (for good reason: the main
property modelled by cryptographic process calculi is that different cipher
texts $\operatorname{E}(M,k)$ and $\operatorname{E}(N,k)$ are
indistinguishable unless the key $k$ is known). To treat the existential
quantifier, we instead add an action $(x)$ with $\operatorname{bn}((x))=x$ and
transitions $P\xrightarrow{(x)}\\{{}^{M}\\!/\\!{}_{x}\\}\mid P$ if
$M\in\mathcal{S}(P)$ and $x\\#P$. We can then encode $\exists x.A$ as
$\langle{}(x)\rangle A$.

Fusion calculus. In an HML for the fusion calculus by Haugstad et al. (2006)
[HTV06] the fusions (i.e., equality relations on names) are action labels
$\varphi$. The corresponding modal operator $\langle{}\varphi\rangle A$ has
the semantics that the formula $A$ must be satisfied for all substitutive
effects of $\varphi$ (intuitively, substitutions that map each name to a fixed
representative for its equivalence class). In order to represent fusion
actions in the logics in this paper, we add substitution effects $\sigma$ such
that $\sigma(P^{\prime})=P^{\prime}\sigma$. The fusion modality
$\langle{}\varphi\rangle A$ can then be encoded in our framework as
$\langle{}\varphi\rangle\bigvee_{\\!\sigma}\sigma@A\sigma$, where the
parameter $\sigma$ of the disjunction ranges over the (finite set of)
substitutive effects of $\varphi$. 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) [DL08] define a
general format for multiple-labelled transition systems with labels for name
revelation and resource management, and an associated modal logic with name
equality predicates, name quantification ($\exists$ and  $\mathsf{N}$ ), and a
fixed-point modality. In contrast, we seek a small and expressive HML for
general nominal transition systems. Indeed, the logic of De Nicola and Loreti
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)
[CMRG12] is also a special case of our nominal transition systems. Aceto et
al. (2017) [AFGP+17] give conditions on rule formats for transitions from
processes to residuals so that they generate nominal transition systems.

##  11\. Formalisation

We have formalised results of Sections 3 and 6–8. We use Nominal Isabelle
[UK12], an implementation of nominal logic in Isabelle/HOL [NPW02]. This is a
popular interactive proof assistant for higher-order logic with convenient
specification mechanisms for, and automation to reason about, data types with
binders. Our Isabelle theories are available from the Archive of Formal Proofs
[WEP+16]. We here comment on some of the interesting aspects, and the
difficulties involved for the results yet without a formal proof.

The main challenge, and perhaps most prominent contribution from the
perspective of formalisation, is the definition of formulas (Definitions 3.1
and 6.2). Nominal Isabelle does not directly support infinitely branching data
types. We therefore construct formulas from first principles in higher-order
logic, by defining an inductive data type of _raw_ formulas (where alpha-
equivalent raw formulas are _not_ identified). The 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 data type
package [BHL+14].

The set of raw formulas $\mathcal{R}$ ranged over by $R$ is defined by
induction as follows:

$R\quad::=\quad\bigwedge_{i\in I}R_{i}\quad|\quad\neg
R\quad|\quad\varphi\quad|\quad\alpha.R$

In $\bigwedge_{i\in I}R_{i}$ it is required that $\lvert I\rvert<\kappa$.

There are no name abstractions or binders in raw formulas: $\alpha.R$, unlike
$\langle{}\alpha\rangle A$, is _not_ an abbreviation for an equivalence class,
and $\operatorname{bn}(\alpha)$ plays no role in the definition of raw
formulas. Name permutation distributes over all raw constructors. Raw formulas
need not have finite support: for instance, consider the raw formula
$\bigwedge_{a\in S}\varphi_{a}$ where
$\operatorname{supp}(\varphi_{a})=\\{a\\}$ and $S\subset\mathcal{N}$ is not
finitely supported.

We then define the _concrete_ alpha-equivalence of raw formulas (not to be
confused with nominal alpha-equivalence as defined in Section 2), in the
following just called alpha-equivalence, by well-founded recursion.

Two raw formulas $\bigwedge_{i\in I}R_{i}$ and $\bigwedge_{i\in I}S_{i}$ are
_alpha-equivalent_ ($\mathop{\approx_{\alpha}}$) if for every conjunct $R_{i}$
there is an alpha-equivalent conjunct $S_{j}$, and vice versa. Two raw
formulas $\alpha.R$ and $\beta.S$ are alpha-equivalent if there exists a
permutation $\pi$ with $\pi\cdot\alpha=\beta$ such that $\pi\cdot
R\approx_{\alpha}S$. Moreover, $\pi$ must leave names that are in
$(\operatorname{supp}(\alpha)\cup N)\setminus\operatorname{bn}(\alpha)$
invariant, for some set of names $N$ that supports $[R]_{\approx_{\alpha}}$.
The other cases in the definition of alpha-equivalence are standard.

We note that alpha-equivalence is equivariant, i.e., $R\approx_{\alpha}S$ iff
$\pi\cdot R\approx_{\alpha}\pi\cdot S$. Moreover, all raw constructors respect
alpha-equivalence. 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.

An alpha-equivalence class $[R]_{\approx_{\alpha}}$ is _hereditarily finitely
supported (h.f.s.)_ if, for each subformula $S$ of $R$,
$[S]_{\approx_{\alpha}}$ has finite support.

Definitions 11–11 have been formalised in Isabelle. To our knowledge, this is
the first mechanisation of infinitely branching nominal data types in a proof
assistant. Fortunately, we need not keep the details of this construction in
mind, since the formulas obtained in this way agree with those obtained from
Definition 3.1. We give an explicit bijection.

If $R$ is a raw formula, the corresponding formula $A_{R}$ is defined
homomorphically except for the case $R=\alpha.S$ where
$A_{\alpha.S}=\langle{}\alpha\rangle A_{S}$.

This defines a partial function
$\Gamma\colon\mathcal{R}\hookrightarrow\mathcal{A}$, $R\mapsto A_{R}$.
$\Gamma$ is partial because $\Gamma(\bigwedge_{i\in I}R_{i})=\bigwedge_{i\in
I}\Gamma(R_{i})$ is well-formed only when $\\{\Gamma(R_{i})\mid i\in I\\}$ is
finitely supported.

######  Lemma 51.

The partial function $\Gamma$ is equivariant on its domain:
$R\in\operatorname{dom}(\Gamma)$ iff $\pi\cdot
R\in\operatorname{dom}(\Gamma)$, and in this case
$\pi\cdot\Gamma(R)=\Gamma(\pi\cdot R)$.

######  Proof 11.1.

By structural induction on $R$, using the fact that all constructors of (raw)
formulas are equivariant.

######  Theorem 52.

For all $R$, $S\in\operatorname{dom}(\Gamma)$, we have $R\approx_{\alpha}S$
iff $\Gamma(R)=\Gamma(S)$.

######  Proof 11.2.

By structural induction on $R$, for arbitrary
$S\in\operatorname{dom}(\Gamma)$. The case $R=\varphi$ is trivial. The cases
$R=\neg R^{\prime}$ and $R=\bigwedge_{i\in I}R_{i}$ follow from the induction
hypothesis. Finally consider $R=\alpha.R^{\prime}$.

$\Longrightarrow$: From $R\approx_{\alpha}S$ we obtain $S=\beta.S^{\prime}$
and a permutation $\pi$ with $\pi\cdot\alpha=\beta$ and $\pi\cdot
R^{\prime}\approx_{\alpha}S^{\prime}$. Equivariance of $\approx_{\alpha}$
implies $R^{\prime}\approx_{\alpha}\pi^{-1}\cdot S^{\prime}$, hence
$\pi\cdot\Gamma(R^{\prime})=\Gamma(S^{\prime})$ by induction and Lemma 51.
Moreover, $\pi$ must leave names in $(\operatorname{supp}(\alpha)\cup
N)\setminus\operatorname{bn}(\alpha)$ invariant, where $N$ supports
$[R^{\prime}]_{\approx_{\alpha}}$. The induction hypothesis implies
$\operatorname{supp}([R^{\prime}]_{\approx_{\alpha}})=\operatorname{supp}(\Gamma(R^{\prime}))$.
Since $\operatorname{supp}([R^{\prime}]_{\approx_{\alpha}})$ is the smallest
set that supports $[R^{\prime}]_{\approx_{\alpha}}$ we have
$\operatorname{supp}([R^{\prime}]_{\approx_{\alpha}})\subseteq N$. Hence $\pi$
witnesses
$\langle{}\alpha\rangle\Gamma(R^{\prime})=\langle{}\beta\rangle\Gamma(S^{\prime})$.

$\Longleftarrow$: From $\Gamma(R)=\Gamma(S)$ we obtain $S=\beta.S^{\prime}$
and a permutation $\pi$ with $\pi\cdot\alpha=\beta$ and
$\pi\cdot\Gamma(R^{\prime})=\Gamma(S^{\prime})$. Lemma 51 implies
$\Gamma(R^{\prime})=\Gamma(\pi^{-1}\cdot S^{\prime})$, hence $\pi\cdot
R^{\prime}\approx_{\alpha}S^{\prime}$ by induction and equivariance of
$\approx_{\alpha}$. Moreover, $\pi$ must leave names in
$(\operatorname{supp}(\alpha)\cup\operatorname{supp}(\Gamma(R^{\prime})))\setminus\operatorname{bn}(\alpha)$
invariant. The induction hypothesis implies
$\operatorname{supp}([R^{\prime}]_{\approx_{\alpha}})=\operatorname{supp}(\Gamma(R^{\prime}))$.
Hence $\pi$ witnesses $\alpha.R^{\prime}\approx_{\alpha}\beta.S^{\prime}$.

Theorem 52 implies that $\Gamma$ can be lifted to a partial function on alpha-
equivalence classes,
$\hat{\Gamma}\colon\mathcal{R}/_{\approx_{\alpha}}\hookrightarrow\mathcal{A}$,
$[R]_{\approx_{\alpha}}\mapsto A_{R}$ for $R\in\operatorname{dom}(\Gamma)$.
The following lemma shows that this function is defined on all alpha-
equivalence classes that are h.f.s.

######  Lemma 53.

If $[R]_{\approx_{\alpha}}$ is h.f.s, then $R\approx_{\alpha}S$ for some
$S\in\operatorname{dom}(\Gamma)$.

######  Proof 11.3.

By structural induction on $R$.

To prove that $\hat{\Gamma}$ is a bijection between h.f.s. alpha-equivalence
classes and formulas, it remains to show that every formula is the image of
some h.f.s alpha-equivalence class.

######  Theorem 54.

For any formula $A$, there is h.f.s $[R]_{\approx_{\alpha}}$ such that
$\hat{\Gamma}([R]_{\approx_{\alpha}})=A$.

######  Proof 11.4.

By Theorem 52, $\hat{\Gamma}$ is injective. It follows that the inverse
function
$\hat{\Gamma}^{-1}\colon\mathcal{A}\hookrightarrow\mathcal{R}/_{\approx_{\alpha}}$
is well-defined on $\hat{\Gamma}(\mathcal{R}/_{\approx_{\alpha}})$.
Equivariance of $\Gamma$ (Lemma 51) implies that $\hat{\Gamma}^{-1}$ is
equivariant on its domain. We show by induction on $A$ that
$A\in\operatorname{dom}(\hat{\Gamma}^{-1})$ and that $\hat{\Gamma}^{-1}(A)$ is
h.f.s.

In order to conveniently work with formulas in Isabelle we have proved
important lemmas; for instance, a strong induction principle for formulas that
allows the bound names in $\langle{}\alpha\rangle A$ to be chosen fresh for
any finitely supported context. This is why we prefer the logic for weak
bisimulation (Definition 32) to be a sublogic: that way we do not have to re-
do these proofs. Armed with these definitions and induction principles, most
of the proof mechanisation proceeded smoothly. The formal proofs follow
closely the sketches provided in this paper, and often helped clarify points
and correct minor errors. Our development currently amounts to approximately
8800 lines of Isar proof scripts; this is divided according to Table 2.

Topic | Section | LOC
---|---|---
Basics | 3 | 3062
L-bisimilarity | 6 | 3215
Unobservables | 7 | 1730
Predicates vs actions | 8 | 817
Table 2. Size (lines of code) of the Isabelle formalisation.

Some parts of this paper lack formal proofs. Among them are the definitions
and results in Section 5 on fixpoint operators. Here proof mechanisation would
be tedious, since Isabelle does not provide enough support for transfinite
induction: explicit reasoning about ordinals and cardinals would require
further library development [BPT14]. The results of Sections 9 and 10, on
applications and comparisons with related work, lack proofs for two reasons.
First, the correspondences are not exact since we allow arbitrary finitely
supported conjunctions, and second, any formal proof must begin by
constructing a formal model of the related work under study, which would
require a large effort including resolving any ambiguities in that work.

Finally, the result on disjunction elimination (Section 7.4, Theorem 41) is
challenging for a different reason. The proof uses a case analysis and
induction over derived operators. While we believe that our proof is correct,
to formalise it we would need to prove that this is well-defined, despite the
ranges of the derived operators not being disjoint (recall that
$\langle\\!\langle\alpha\rangle\\!\rangle A$ is shorthand for a disjunction,
which in turn is shorthand for a negation). This turned out to be more
difficult than first anticipated, and at the time of writing, we have not
finished the formal proofs.

##  12\. 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. Our main results have been formalised in
the interactive proof assistant Isabelle.

There are many interesting avenues for further research. Many process algebras
can be given a semantics where the operators of the algebra correspond to
functions on nominal transition systems with designated initial states. There
may be interesting classes of such functions, for example finitely supported
bisimilarity preserving functions, that merit study. For particular such
functions it would be interesting to explore compositionality of $\models$.
Similar work abounds for ordinary transition systems and modal logics; for
nominal transition systems in general this area is very much open.

## Acknowledgements

We thank Andrew Pitts for enlightening discussions on nominal data types with
infinitary constructors, and Dmitriy Traytel for providing an Isabelle/HOL
formalisation of cardinality-bounded sets. We also thank Ross Horne for
discussions on modal logics for open bisimilarity, and for pointing out an
inadequacy of an earlier version of $F/L$-bisimilarity. We are very grateful
to the anonymous referees for many constructive comments.

## References

  * [Abr91] Samson Abramsky.  A domain equation for bisimulation.  Information and Computation, 92(2):161–218, 1991.
  * [AF01] Martín Abadi and Cédric Fournet.  Mobile values, new names, and secure communication.  In Chris Hankin and Dave Schmidt, editors, Proceedings of POPL ’01, pages 104–115. ACM, January 2001.
  * [AFGP+17] Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén.  Rule formats for nominal process calculi.  In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1–10:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
  * [AG99] Martín Abadi and Andrew D. Gordon.  A calculus for cryptographic protocols: the Spi calculus.  Information and Computation, 148(1):1–70, 1999.
  * [AHT17] Ki Yung Ahn, Ross Horne, and Alwen Tiu.  A characterisation of open bisimilarity using an intuitionistic modal logic.  In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1–7:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
  * [BDNP01] Michele Boreale, Rocco De Nicola, and Rosario Pugliese.  Proof techniques for cryptographic processes.  SIAM Journal on Computing, 31(3):947–986, 2001.
  * [BHL+14] Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel.  Truly modular (co)datatypes for Isabelle/HOL.  In Gerwin Klein and Ruben Gamboa, editors, Proceedings of ITP 2014, volume 8558 of LNCS, pages 93–110. Springer, 2014.
  * [BHY08] Martin Berger, Kohei Honda, and Nobuko Yoshida.  Completeness and logical full abstraction in modal logics for typed mobile processes.  In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming: 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, part II, volume 5126 of LNCS, pages 99–111. Springer Berlin Heidelberg, 2008.
  * [BJPV11] Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor.  Psi-calculi: a framework for mobile processes with nominal data and logic.  Logical Methods in Computer Science, 7(1), 2011.
  * [BM07] Maria Grazia Buscemi and Ugo Montanari.  CC-Pi: A constraint-based language for specifying service level agreements.  In Rocco De Nicola, editor, Proceedings of ESOP 2007, volume 4421 of LNCS, pages 18–32. Springer, 2007.
  * [BM08] Maria Grazia Buscemi and Ugo Montanari.  Open bisimulation for the concurrent constraint pi-calculus.  In Sophia Drossopoulou, editor, Proceedings of ESOP 2008, volume 4960 of LNCS, pages 254–268. Springer, 2008.
  * [BPT14] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel.  Cardinals in Isabelle/HOL.  In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of LNCS, pages 111–127. Springer, 2014.
  * [BS99] Julian C. Bradfield and Perdita Stevens.  Observational mu-calculus.  Technical Report RS-99-5, BRICS, 1999.
  * [CE82] Edmund M. Clarke and E. Allen Emerson.  Design and synthesis of synchronization skeletons using branching-time temporal logic.  In Dexter Kozen, editor, Logic of Programs, Workshop, volume 131 of LNCS, pages 52–71. Springer, 1982.
  * [CGR11] Sjoerd Cranen, Jan Friso Groote, and Michel Reniers.  A linear translation from CTL* to the first-order modal $\mu$-calculus.  Theoretical Computer Science, 412(28):3129 – 3139, 2011.  Festschrift in Honour of Jan Bergstra.
  * [CMRG12] Matteo Cimini, Mohammad Reza Mousavi, Michel A. Reniers, and Murdoch J. Gabbay.  Nominal SOS.  Electronic Notes in Theoretical Computer Science, 286:103–116, September 2012.  Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII).
  * [CMS02] Muffy Calder, Savi Maharaj, and Carron Shankland.  A modal logic for full LOTOS based on symbolic transition systems.  The Computer Journal, 45(1):55–61, 2002.
  * [Dam96] Mads Dam.  Model checking mobile processes.  Information and Computation, 129(1):35 – 51, 1996.
  * [DL08] Rocco De Nicola and Michele Loreti.  Multiple-labelled transition systems for nominal calculi and their logics.  Mathematical Structures in Computer Science, 18(1):107–143, 2008\.
  * [Eme96] E. Allen Emerson.  Model checking and the Mu-calculus.  In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 185–214. American Mathematical Society, 1996.
  * [FHNJ02] Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen.  Modal logics for cryptographic processes.  Electronic Notes in Theoretical Computer Science, 68(2):124–141, 2002.  Proceedings of EXPRESS’02, 9th International Workshop on Expressiveness in Concurrency.
  * [FNJ01] Ulrik Frendrup and Jesper Nyholm Jensen.  Bisimilarity in the spi-calculus.  Master’s thesis, Aalborg University, 2001.  http://projekter.aau.dk/projekter/en/studentthesis/bisimilarity-in-the-spicalculus(f1636334-8677-4fdf-aaa8-66f9d8e0fbf7).html.
  * [Gab03] Murdoch J. Gabbay.  The $\pi$-calculus in FM.  In Fairouz D. Kamareddine, editor, Thirty Five Years of Automating Mathematics, pages 247–269. Springer Netherlands, Dordrecht, 2003\.
  * [HL95] Matthew Hennessy and Xinxin Liu.  A modal logic for message passing processes.  Acta Informatica, 32(4):375–393, 1995.
  * [HM80] Matthew Hennessy and Robin Milner.  On observing nondeterminism and concurrency.  In J. W. de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, 7th Colloquium, volume 85 of Lecture Notes in Computer Science, pages 299–309. Springer, 1980.
  * [HM85] Matthew Hennessy and Robin Milner.  Algebraic laws for nondeterminism and concurrency.  Journal of the ACM, 32(1):137–161, 1985.
  * [HP07] Hans Hüttel and Michael D. Pedersen.  A logical characterisation of static equivalence.  Electronic Notes in Theoretical Computer Science, 173:139–157, 2007\.  Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII).
  * [HTV06] Arild Martin Møller Haugstad, Anders Franz Terkelsen, and Thomas Vindum.  A modal logic for the fusion calculus.  Unpublished, Aalborg University, http://vbn.aau.dk/ws/files/61067487/1149104946.pdf, 2006.
  * [JBPV10] Magnus Johansson, Jesper Bengtson, Joachim Parrow, and Björn Victor.  Weak equivalences in psi-calculi.  In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 322–331, 2010.
  * [JKP90] Bengt Jonsson, Ahmed Hussain Khan, and Joachim Parrow.  Implementing a model checking algorithm by adapting existing automated tools.  In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems: International Workshop, Grenoble, France June 12–14, 1989 Proceedings, volume 407 of LNCS, pages 179–188. Springer Berlin Heidelberg, Berlin, Heidelberg, 1990.
  * [KGH18] Vasileios Koutavas, Maciej Gazda, and Matthew Hennessy.  Distinguishing between communicating transactions.  Information and Computation, 259:1 – 30, 2018.
  * [KH12] Vasileios Koutavas and Matthew Hennessy.  First-order reasoning for higher-order concurrency.  Computer Languages, Systems & Structures, 38(3):242–277, 2012\.
  * [KL17] Bartek Klin and Mateusz Lelyk.  Modal mu-calculus with atoms.  In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:21, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
  * [Koz83] Dexter Kozen.  Results on the propositional mu-calculus.  Theoretical Computer Science, 27(3):333 – 354, 1983.  Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982.
  * [Kur22] Casimir Kuratowski.  Une méthode d’élimination des nombres transfinis des raisonnements mathématiques.  Fundamenta Mathematicae, 3(1):76–108, 1922.
  * [Lam02] Leslie Lamport.  Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.  Addison-Wesley, June 2002.
  * [Lar88] Kim Guldstrand Larsen.  Proof system for hennessy-milner logic with recursion.  In Max Dauchet and Maurice Nivat, editors, CAAP ’88, 13th Colloquium on Trees in Algebra and Programming, Nancy, France, March 21-24, 1988, Proceedings, volume 299 of Lecture Notes in Computer Science, pages 215–230. Springer, 1988.
  * [Mil81] Robin Milner.  A modal characterisation of observable machine-behaviour.  In Egidio Astesiano and Corrado Böhm, editors, CAAP ’81, Trees in Algebra and Programming, 6th Colloquium, Genoa, Italy, March 5-7, 1981, Proceedings, volume 112 of Lecture Notes in Computer Science, pages 25–34. Springer, 1981.
  * [Mil89] Robin Milner.  Communication and Concurrency.  Prentice Hall, 1989.
  * [MPW92] Robin Milner, Joachim Parrow, and David Walker.  A calculus of mobile processes, I.  Information and Computation, 100(1):1–40, 1992.
  * [MPW93] Robin Milner, Joachim Parrow, and David Walker.  Modal logics for mobile processes.  Theoretical Computer Science, 114(1):149 – 171, 1993.
  * [NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.  Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS.  Springer, 2002.
  * [PBE+15] Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber.  Modal logics for nominal transition systems.  In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 198–211. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [Ped06] Michael Pedersen.  Logics for the applied pi calculus.  Master’s thesis, Aalborg University, 2006.  BRICS RS-06-19.
  * [Pit03] Andrew M. Pitts.  Nominal logic, a first order theory of names and binding.  Information and Computation, 186(2):165–193, 2003.
  * [Pit13] Andrew M. Pitts.  Nominal Sets.  Cambridge University Press, 2013.  Cambridge Books Online.
  * [Pit15] Andrew M. Pitts, 2015.  Personal communication.
  * [PV98] Joachim Parrow and Björn Victor.  The fusion calculus: Expressiveness and symmetry in mobile processes.  In Proceedings of LICS 1998, pages 176–185. IEEE Computer Society Press, 1998.
  * [PWBE17] Joachim Parrow, Tjark Weber, Johannes Borgström, and Lars-Henrik Eriksson.  Weak nominal modal logic.  In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings, pages 179–193, 2017.
  * [San93] Davide Sangiorgi.  A theory of bisimulation for the $\pi$-calculus.  In Eike Best, editor, Proceedings of CONCUR ’93, volume 715 of LNCS, pages 127–142. Springer, 1993.
  * [Sim04] Alex Simpson.  Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS.  The Journal of Logic and Algebraic Programming, 60-61:287–322, 2004\.
  * [Tar55] Alfred Tarski.  A lattice-theoretical fixpoint theorem and its applications.  Pacific Journal of Mathematics, 5(2):285–309, 1955.
  * [UK12] Christian Urban and Cezary Kaliszyk.  General bindings and alpha-equivalence in Nominal Isabelle.  Logical Methods in Computer Science, 8(2), 2012.
  * [vB85] Johan van Benthem.  Modal Logic and Classical Logic.  Bibliopolis, Naples, 1985.
  * [WEP+16] Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, and Ramūnas Gutkovas.  Modal logics for nominal transition systems.  Archive of Formal Proofs, October 2016.  http://isa-afp.org/entries/Modal_Logics_for_NTS.shtml, Formal proof development.
  * [WG05] Lucian Wischik and Philippa Gardner.  Explicit fusions.  Theoretical Computer Science, 304(3):606–630, 2005.
  * [XL15] Xian Xu and Huan Long.  A logical characterization for linear higher-order processes.  Journal of Shanghai Jiaotong University (Science), 20(2):185–194, 2015.