# A Characterisation of Open Bisimilarity
using an Intuitionistic Modal Logic

Ki Yung Ahn  Department of Computer Engineering Hannam University, Daejeon,
Korea<EMAIL_ADDRESS>,  Ross Horne  School of Computer Science and Engineering,
Nanyang Technological University, Singapore<EMAIL_ADDRESS>and  Alwen Tiu
Research School of Computer Science, Australian National University, Canberra,
Australia<EMAIL_ADDRESS>
###### Abstract.

Open bisimilarity is the original notion of bisimilarity to be introduced for
the $\pi$-calculus that is a congruence. In open bisimilarity, free names in
processes are treated as variables that may be instantiated lazily; in
contrast to early and late bisimilarity where free names are constants. We
build on the established line of work, due to Milner, Parrow, and Walker, on
classical modal logics characterising early and late bisimilarity for the
$\pi$-calculus. The important insight is, to characterise open bisimilarity,
we move to the setting of intuitionistic modal logics. The intuitionistic
modal logic introduced, called $\mathcal{OM}$, is such that modalities are
closed under (respectful) substitutions, inducing a property known as
intuitionistic hereditary. Intuitionistic hereditary reflects the lazy
instantiation of names in open bisimilarity. The soundness proof for open
bisimilarity with respect to the modal logic is mechanised in Abella. The
constructive content of the completeness proof provides an algorithm for
generating distinguishing formulae, where such formulae are useful as a
certificate explaining why two processes are not open bisimilar. We draw
attention to the fact that open bisimilarity is not the only notion of
bisimilarity that is a congruence: for name-passing calculi there is a
classical/intuitionistic spectrum of bisimilarities.

###### Key words and phrases:

bisimulation, modal logic, intuitionistic logic

##  1\. Introduction

This work provides insight into the logical nature of open bisimilarity
[San96], but firstly we recall why open bisimilarity itself is important. The
problem open bisimilarity addressed was that the original notions of
bisimilarity proposed for the $\pi$-calculus (early and late bisimilarity
[MPW92, MPW93]) do not directly define congruence relations. That is, if we
show two processes are bisimilar, it is not necessarily the case that they are
bisimilar in any context. Having an equivalence relation that is not a
congruence is problematic for compositional reasoning, since, having
established an algebraic property, it cannot, be applied with confidence,
anywhere inside a process. By addressing this problem, by providing a notion
of bisimilarity that is a congruence, open bisimilarity allows the
$\pi$-calculus to stays true to this desirable property of a processes
algebra.

Besides improved algebraic properties, open bisimilarity can be used to
improve the efficiency of equivalence checking. Open bisimilarity is the
notion of bisimilarity implemented in the Mobility Workbench [VM94] — the
first toolkit for the $\pi$-calculus. A reason open bisimilarity is efficient
to implement is that it takes a lazy approach to instantiating names. When we
consider an input action, we are not required to explore all possible inputs,
but instead can leave the input name in the action as a variable, symbolically
representing all possible inputs. This can avoid unnecessarily exploring
exponentially many inputs; instead, exploring only the state space necessary.
This lazy “call-by-need” approach to input transitions is particularly useful
when checking bisimilarity for extensions of the $\pi$-calculus, where
infinitely many messages may be received for a single input action [TD10].
Thus open bisimilarity has impact beyond the setting of the $\pi$-calculus.

The trick for ensuring open bisimilarity is a congruence, and also for
permitting a lazy approach to inputs is as follows: an open bisimulation is
closed under all permitted substitutions at every step in the bisimulation
game. When we move to the setting of logic, closure under substitutions
corresponds to a concept called intuitionistic hereditary, which can be used
to induce an intuitionistic logic [Kri65]. This observation leads us to the
intuitionistic modal logic in this work.

To understand why closing under substitutions results in an intuitionistic
modal logic, firstly consider the setting of a classical modal logic. In a
classical setting, the law of excluded middle holds, hence we expect that
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$
is a tautology. That is, any process can either perform a $\tau$-transition or
it cannot perform a $\tau$-transition.

In contrast, now consider the setting of an intuitionistic modal logic. In the
intuitionistic setting we close under all substitutions, so
$P\models\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ now reads,
under any substitution $\sigma$, process $P\sigma$ cannot perform a
$\tau$-transition. Under this interpretation we have the following.

$\overline{a}b\mathrel{\|}c(x)\not\models\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

To see why the above is not satisfiable, observe that, by applying
substitution
$\mathclose{\\{^{c\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!a}\\}}$ to
the above process, we reach process $\overline{c}b\mathrel{\|}c(x)$, which is
a $\pi$-calculus process for which a communication is enabled on channel $c$.
Since we have demonstrated there is a substitution under which a
$\tau$-transition can be performed, process $\overline{a}b\mathrel{\|}c(x)$
cannot satisfy formula
$\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ in the
intuitionistic setting.

As in the classical case, in the intuitionistic case we have the following,
since there is a substitution under which no communication can be performed
(the identity substitution).

$\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

Putting the above together, we have the following in our intuitionistic modal
logic, since we have just shown that neither branch of the disjunction is
satisfiable.

$\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

Notice the above we claimed was a tautology in the classical case, since it is
an instance of the law of excluded middle. Hence the above example
demonstrates that, by closing operators of the modal logic under
substitutions, the law of excluded middle does not hold. The absence of the
law of excluded middle is a key criteria for any intuitionistic logic.

Intuitively, the absence of the law of excluded middle for the example above
can be interpreted as follows. For $\overline{a}b\mathrel{\|}c(x)$, we have
not yet decided whether the process can perform a $\tau$-transition or not
perform a $\tau$-transition. It is possible that $a$ and $c$ could be the same
channel but, since they are variables, we have not yet decided whether this is
the case.

So, inducing the key feature of an open bisimulation, closure under
substitutions, in a modal logic gives rise to an intuitionistic modal logic.
Furthermore, we establish in this work that such an intuitionistic modal
logic, called $\mathcal{OM}$, characterises open bisimilarity. In the
tradition pioneered by Hennessy and Milner [HM85], a modal logic characterises
a bisimilarity whenever: given two processes, they are bisimilar if and only
if there is no distinguishing formula separating the two. A distinguishing
formula is a formulae that holds for one process but does not hold for the
other process. Such distinguishing formulae are useful for explaining why two
processes are not bisimilar, since when processes are not bisimilar we can
always exhibit a distinguishing formula in a characteristic logic.

As an example of a distinguishing formula, consider the following two
processes.

$R\triangleq\mathopen{\tau.}\left(\overline{a}{b}.{{a}{(x)}}+{a}{(x)}.{\overline{a}{b}}+\tau\right)+\mathopen{\tau.}\left(\overline{a}{b}.{{c}{(x)}}+{c}{(x)}.{\overline{a}{b}}\right)\qquad\qquad
S\triangleq
R+\mathopen{\tau.}\left(\overline{a}{b}\mathrel{\|}{c}{(x)}\right)$

The above processes are not open bisimilar. Process $R$ satisfies
$\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$,
where the box modality ranges over all $\tau$-transitions. However, process
$S$ does not satisfy
$\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$,
since there is a $\tau$-transition to process $\overline{a}b\mathrel{\|}c(x)$
that we just agreed does not satisfy
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$.
In this example, the absence of the law of excluded middle is necessary for
the existence of a formula distinguishing these processes in
$\mathcal{O\\!M}$.

Modal logics characterising late bisimilarity and early bisimilarity were
developed early in the literature on the $\pi$-calculus, by Milner, Parrow and
Walker [MPW93], as part of the motivation for the $\pi$-calculus itself.
However, proving that a modal logic can characterise open bisimilarity was an
open problem until a solution was provided in the conference version of this
paper [AHT17a]. This extended version includes more details on proofs, new
examples, details on the mechanisation of soundness, and further insight into
the classical/intuitionistic spectrum.

A key novelty of this work is the constructive proof of completeness of this
logical characterisation. Due to the intuitionistic nature of the modal logic,
the completeness proof cannot appeal to certain classical principals, such as
de Morgan dualities. This forces the proof to follow a strategy quite
different to corresponding completeness proofs for classical modal logics. The
proof directly constructs a pair of distinguishing formulae for every pair of
processes that are not open bisimilar.

##### Outline

Section 2 introduces the semantics of intuitionistic modal logic
$\mathcal{O\\!M}$. Section 3 recalls open bisimilarity and states the
soundness and completeness results. Section 4 presents the proof of the
correctness of an algorithm for generating distinguishing formulae, which is
used to establish completeness of $\mathcal{O\\!M}$ with respect to open
bisimilarity. Section 5 describes how the proof assistant Abella [BCG+14] was
used to mechanically prove soundness of $\mathcal{O\\!M}$ with respect to open
bisimulation. Section 6 situates $\mathcal{O\\!M}$ with respect to other modal
logics in the classical/intuitionistic spectrum. The soundness theorem
(Section 5) and selected examples (Section 2 and Section 4) have been
mechanised in the Abella theorem prover, and are available online.111Via
https://github.com/alwentiu/abella/tree/master/pic

##  2\. Introducing the intuitionistic modal logic $\mathcal{O\\!M}$

$\begin{tabular}[]{l@{\hspace{1ex}}r@{\hspace{1ex}}l@{\hspace{1ex}}r}$\pi$\hfil\hskip
3.87498pt&$\Coloneqq$\hskip 3.87498pt&$\tau$\hfil\hskip
3.87498pt&(progress)\\\ \hfil\hskip 3.87498pt&\hskip
3.87498pt&$\overline{x}{z}$\hfil\hskip 3.87498pt&(free out)\\\ \hfil\hskip
3.87498pt&\hskip 3.87498pt&$\mathopen{\overline{x}}\left(z\right)$\hfil\hskip
3.87498pt&(bound out)\\\ \hfil\hskip 3.87498pt&\hskip
3.87498pt&$x(z)$\hfil\hskip 3.87498pt&(input)\\\ \hfil\hskip 3.87498pt\\\
$P$\hfil\hskip 3.87498pt&$\Coloneqq$\hskip 3.87498pt&$0$\hfil\hskip
3.87498pt&(deadlock)\\\ \hfil\hskip 3.87498pt&\hskip 3.87498pt&$\nu
x.P$\hfil\hskip 3.87498pt&(nu)\\\ \hfil\hskip 3.87498pt&\hskip
3.87498pt&$\pi.P$\hfil\hskip 3.87498pt&(action)\\\ \hfil\hskip
3.87498pt&\hskip 3.87498pt&$\mathopen{\left[x=y\right]}P$\hfil\hskip
3.87498pt&\quad(match)\\\ \hfil\hskip 3.87498pt&\hskip
3.87498pt&$P\mathrel{\|}P$\hfil\hskip 3.87498pt&(par)\\\ \hfil\hskip
3.87498pt&\hskip 3.87498pt&$P+P$\hfil\hskip 3.87498pt&(choice)\\\
\end{tabular}\qquad\quad\begin{gathered}\pi.P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P\\\\[5.0pt]
\nu z.P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.10698pt}{0.62pt}}\limits^{{\mathopen{\overline{x}}\left(z\right)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}QP\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\overline{x}z}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\\\\[5.0pt]
P+Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}RP\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}R\\\\[5.0pt]
[x=x]P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}RP\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}R\end{gathered}\qquad\quad\begin{gathered}\nu
x.P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\nu
x.QP\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\\\\[5.0pt]
P\mathrel{\|}R\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\mathrel{\|}RP\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\\\\[5.0pt]
P\mathrel{\|}Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\mathopen{\nu
z.}\left(P^{\prime}\mathrel{\|}Q^{\prime}\right)P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.10698pt}{0.62pt}}\limits^{{\mathopen{\overline{x}}\left(z\right)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}\quad
Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{14.70758pt}{0.62pt}}\limits^{{x(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}\\\\[5.0pt]
P\mathrel{\|}Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}\mathrel{\|}Q^{\prime}\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!z}\\}}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\overline{x}{y}}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}\quad
Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{14.70758pt}{0.62pt}}\limits^{{x(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}\end{gathered}$
Figure 1. Syntax and semantics of the $\pi$-calculus, plus symmetric rules for
choice and parallel composition, where
$\mathopen{\mathrm{n}}\left(x(y)\right)=\mathopen{\mathrm{n}}\left(\mathopen{\overline{x}}\left(y\right)\right)=\mathopen{\mathrm{n}}\left(\overline{x}y\right)=\left\\{x,y\right\\}$,
$\mathopen{\mathrm{bn}}\left(x(y)\right)=\mathopen{\mathrm{bn}}\left(\mathopen{\overline{x}}\left(y\right)\right)=\left\\{y\right\\}$
and
$\mathopen{\mathrm{n}}\left(\tau\right)=\mathopen{\mathrm{bn}}\left(\tau\right)=\mathopen{\mathrm{bn}}\left(\overline{x}{y}\right)=\emptyset$.
Processes $\nu x.P$, $z(x).P$ and $\bar{z}(x).P$ bind $x$ in $P$.

We recall the syntax and labelled transition semantics for the finite
$\pi$-calculus (Fig. 1). All features are standard: the deadlocked process
that can do nothing, the $\nu$ quantifier that binds private names, the output
prefix that outputs a name on a channel, the input prefix that binds the name
received on a channel, the silent progress action $\tau$, the name match
guard, parallel composition, and non-deterministic choice. There are four
types of action ranged over by $\pi$, where a free output sends a free name,
whereas a bound output extrudes a $\nu$-bounded private name. We employ the
late labelled transition system for the $\pi$-calculus, where the name on the
input channel is a symbolic place holder for a name that is not chosen until
after an input transition. We use the notations
$\mathopen{\mathrm{bn}}\left(E\right)$ and
$\mathopen{\mathrm{fn}}\left(E\right)$ to represent the bound names and,
respectively, free names in a given expression (processes, actions, formulae,
etc) $E.$

Histories are used in the definitions of both the intuitionistic modal logic
and open bisimilarity. Histories are lists (separated using a dot)
representing what is known about free variables due to how they have been
communicated previously to the environment. There are two types of information
about names recorded in a history: fresh private names that have been output,
using action $\overline{a}(x)$, denoted by $x^{o}$; and variables
(symbolically) representing inputs, using action $a(z)$, denoted by $z^{i}$.
What matters is the alternation between the bound outputs and symbolic inputs,
since an input variable can only be instantiated with private names that were
output earlier in the history. This is reflected in the following definition
of a respectful substitution.

######  Definition 2.1 ($\sigma\mathrel{\textrm{respects}}h$).

A history is a (dot separated) list of variables annotated with $o$ or $i$.
Substitution $\sigma$ respects history $h$ whenever, for all $h^{\prime}$ and
$h^{\prime\prime}$ such that $h=h^{\prime}\cdot x^{o}\cdot h^{\prime\prime}$,
$x\sigma=x$, and for all $y\in\mathopen{\mathrm{fn}}\left(h^{\prime}\right)$,
we have $y\sigma\not=x$.

For example, substitution
$\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!z}\\}}$
respects history $x^{i}\cdot y^{o}\cdot z^{i}$, since input variable $z$
appears after $y$ was output, hence $y$ was known to the environment at the
time $z$ was input. In contrast, substitution
$\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$ does
not respect history $x^{i}\cdot y^{o}\cdot z^{i}$, since variable $x$ was
input before private name $y$ was output.

Note that histories fulfil the role of sets of inequality constraints called
distinctions in the original work on open bisimilarity [San96]. Although
distinctions are more general than histories, it is shown in [TM10] that given
a history $h$ and its corresponding distinction $D$, the corresponding
definitions of open bisimilarity coincide.

###  2.1. The semantics of the intuitionistic modal logic $\mathcal{O\\!M}$

The syntax for modal logic $\mathcal{O\\!M}$ is defined by the following
grammar, extending intuitionistic logic with equality and modalities.

$\begin{array}[t]{lr}\left.\begin{array}[]{rlr}\phi\Coloneqq&\mathtt{tt}&\mbox{top}\\\
\mid&\mathtt{ff}&\mbox{bottom}\\\ \mid&\phi\wedge\phi&\mbox{and}\\\
\mid&\phi\vee\phi&\mbox{or}\\\ \mid&\phi\supset\phi&\qquad\mbox{implies}\\\
\mid&x=y&\mbox{equality}\end{array}\qquad\right\\}\qquad\mbox{intuitionistic
logic}\\\
\qquad\\!\\!\left.\begin{array}[]{rlr}\mid&\mathopen{\big{\langle}\pi\big{\rangle}}\phi&\qquad\\!\mbox{diamond}\\\
\mid&\mathopen{\big{[}\pi\big{]}}\phi&\mbox{box}\end{array}\qquad\right\\}\qquad\mbox{modalities}\end{array}$

$\begin{array}[]{lcl}P\models^{h}\mathtt{tt}&\mbox{and}&P\models^{h}x=x\qquad\mbox{always
hold.}\\\
P\models^{h}\phi_{1}\land\phi_{2}&\mbox{iff}&P\models^{h}\phi_{1}~{}\mbox{and}~{}P\models^{h}\phi_{2}.\\\
P\models^{h}\phi_{1}\lor\phi_{1}&\mbox{iff}&P\models^{h}\phi_{1}~{}\mbox{or}~{}P\models^{h}\phi_{2}.\\\
P\models^{h}\phi_{1}\supset\phi_{1}&\mbox{iff}&\forall\sigma\mathrel{\textrm{respecting}}h,P\sigma\models^{h\sigma}\phi_{1}\sigma~{}\mbox{
implies }~{}P\sigma\models^{h\sigma}\phi_{2}\sigma.\\\
P\models^{h}\mathopen{\big{\langle}\alpha\big{\rangle}}\phi&\mbox{iff}&\exists\,Q,~{}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q~{}\mbox{and}~{}Q\models^{h}\phi.\\\
P\models^{h}\mathopen{\big{\langle}\overline{a}(z)\big{\rangle}}\phi&\mbox{iff}&\exists\,Q,~{}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.34111pt}{0.62pt}}\limits^{{\overline{a}(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q~{}\mbox{and}~{}Q\models^{h\cdot
z^{o}}\phi.\\\
P\models^{h}\mathopen{\big{\langle}{a}(z)\big{\rangle}}\phi&\mbox{iff}&\exists\,Q,~{}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.04121pt}{0.62pt}}\limits^{{{a}(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q~{}\mbox{and}~{}Q\models^{h\cdot
z^{i}}\phi.\\\
P\models^{h}\mathopen{\big{[}\alpha\big{]}}\phi&\mbox{iff}&\forall\sigma\mathrel{\textrm{respecting}}h,\forall
Q,\,P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\;\mbox{
implies }\;Q\models^{h\sigma}\phi\sigma.\\\
P\models^{h}\mathopen{\big{[}\overline{a}(z)\big{]}}\phi&\mbox{iff}&\forall\sigma\mathrel{\textrm{respecting}}h,~{}\forall
Q,P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.34111pt}{0.62pt}}\limits^{{\overline{a\sigma}(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\mbox{
implies }Q\models^{h\sigma\cdot z^{o}}\phi\sigma.\\\
P\models^{h}\mathopen{\big{[}{a}(z)\big{]}}\phi&\mbox{iff}&\forall\sigma\mathrel{\textrm{respecting}}h,\forall
Q,P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.0411pt}{0.62pt}}\limits^{{a\sigma(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\mbox{
implies }Q\models^{h\sigma\cdot z^{i}}\phi\sigma.\end{array}$
Figure 2. Semantics of the modal logic $\mathcal{O\\!M}$, where $\alpha$ is
$\tau$ or $\overline{a}b$; and $z$ is fresh for $P$, $h$, and $\sigma$.

The semantics of intuitionistic modal logic $\mathcal{O\\!M}$, presented in
Fig. 2, is defined in terms of the late labelled transitions system in Fig. 1
and history respecting substitutions (Definition 2.1). Satisfaction is defined
as follows, by treating all free variables as inputs in the past.

######  Definition 2.2 (satisfaction).

Satisfaction, written $P\models\phi$, holds whenever
$P\models^{x_{0}^{i}\cdot\ldots\cdot x_{n}^{i}}\phi$ according to the
inductive definition in Fig. 2, where
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(\phi\right)\subseteq\left\\{x_{0},\ldots,x_{n}\right\\}$.

Observe the semantics for connectives of intuitionistic logic can be obtained
from a suitable Kripke semantics. Take worlds to be pairs of processes and
histories. Now define a relation over worlds $\leq$ as follows.

> $P,h~{}\leq_{\sigma}Q,h^{\prime}$ whenever $\sigma$ respects $h$,
> $P\sigma=Q$ and $h\sigma=h^{\prime}$.

As standard for such an intuitionistic semantics, implication is closed under
all worlds reachable according to such a relation. Thus satisfaction
$P\models^{h}\phi\supset\psi$, involving an implication, is defined such that
under all $Q$, $h^{\prime}$ and $\sigma$, whenever
$P,h\leq_{\sigma}Q,h^{\prime}$ we have $Q\models^{h^{\prime}}\phi\sigma\supset
Q\models^{h^{\prime}}\psi\sigma$. This Kripke semantics gives rise to the
definition of implication provided in Fig. 2.

Modalities must also be closed under all respectful substitutions. There is an
asymmetry in the definition of these modalities. Unlike the box modality, for
the diamond modality we need not close the definition under all reachable
worlds.

To explain this asymmetry between the box and diamond modalities in the
definitions, observe, for the diamond modality, a transition must be possible
regardless of the substitution. Thus it is sufficient to check the identity
substitution. For example, the following is not satisfiable.

$\mathopen{\left[x=y\right]}\tau\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

To check the above does not hold, it is sufficient to check that
$\mathopen{\left[x=y\right]}\tau$ cannot perform a $\tau$-transition. This is
reflected in the semantics of the diamond modalities.

In contrast, for the box modality there may exist substitutions other than the
identity substitution enabling a transition, hence we should consider all
respectful substitutions. Perhaps the simplest interesting example, requiring
closure of box under respectful substitutions, is the following:

$\mathopen{\left[x=y\right]}\tau\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$

The above satisfaction holds since for any substitution $\sigma$ such that
$\left(\mathopen{\left[x=y\right]}\tau\right)\mathclose{\sigma}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
it must be case that $x\sigma=y\sigma$. Thus for all such substitutions we
have $0\models x\sigma=y\sigma$ holds, as required. In contrast, observe the
above process does not satisfy $\mathopen{\big{[}\tau\big{]}}\mathtt{ff}$.

###  2.2. Checking the law of excluded middle is invalidated.

Given the semantics we can now formally check the example from the
introduction. Recall that we claimed
$\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$,
where $\neg\phi$, as standard, is defined as $\phi\supset\mathtt{ff}$. This
example demonstrates the law of excluded middle is invalid. Appealing to the
rule for disjunction, observe that we have the following.

$\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\qquad\mbox{and}\qquad\overline{a}b\mathrel{\|}c(x)\not\models\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

The former can hold only if $\overline{a}b\mathrel{\|}c(x)$ is guaranteed to
make a $\tau$-transition; but such a transition is only possible under a
substitution $\sigma$ such that $a\sigma=c\sigma$, hence
$\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$.
For the latter, we should consider all substitutions which enable a
$\tau$-transition; and, since such a substitution
$\mathclose{\\{^{c\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!a}\\}}$
exists,
$\overline{a}b\mathrel{\|}c(x)\not\models\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$.

Critically for this work, the above example illustrates that a property
typically used to establish the completeness of open bisimilarity with respect
to a classical modal logic breaks down. In the classical setting, we expect
$P\not\models\phi$ if and only if $P\models\neg\phi$. However, as the above
example demonstrates, there are processes, such as
$\overline{a}b\mathrel{\|}c(x)$, that do not satisfy
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$, but also do not
satisfy $\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$. Hence in
the intuitionistic setting we cannot appeal to this principal of classical
modal logic.

As a further example of this principal, observe the following are both
unsatisfiable.

$\tau\not\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\qquad\mbox{and}\qquad\tau\not\models\neg\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$

The former is unsatisfiable since, under the identity substitution,
$\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$,
but $0\not\models x=y$. The latter is also unsatisfiable since, there is a
substitution
$\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$ such
that
$\tau\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
still holds and $0\models
x\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}=y\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$
holds; but clearly
$0\models\mathtt{ff}\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$
can never hold; hence
$\tau\not\models\neg\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$.

As expected for an intuitionistic logic, further classical dualities break, as
witnessed by the following examples of unsatisfiable formulae.

$\mathopen{\left[x=y\right]}\tau\not\models\neg\neg\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\qquad\mbox{and}\qquad
0\not\models\neg\neg\mathopen{\neg}\left(x=y\right)\supset\neg\left(x=y\right)$

Also de Morgan dualities cannot be applied. For example, classically we have
$P\models\mathopen{\neg}\left(\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\wedge\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
if and only if
$P\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}$.
However in the intuitionistic setting we have the following.

$\overline{a}b\mathrel{\|}c(x)\models\mathopen{\neg}\left(\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\wedge\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\qquad\mbox{but}\qquad\overline{a}b\mathrel{\|}c(x)\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}$

##  3\. Open bisimilarity, soundness and completeness

We recall the definition of open bisimilarity. Open bisimilarity is the
greatest symmetric relation closed under all respectful substitutions and
labelled transitions actions at every step. Notice we use the history to
record whenever a (symbolic) input or private output occurs.

######  Definition 3.1 (open bisimilarity).

An open bisimulation $\mathcal{R}$ is a symmetric relation on processes,
indexed by a history $h$, such that: if $P\mathrel{\mathcal{R}^{h}}Q$ then,
the following hold:

  * •

For all substitutions $\sigma$ respecting $h$, we have
$P\sigma\mathrel{\mathcal{R}^{h\sigma}}Q\sigma$.

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
then there exists $Q^{\prime}$ such that $Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}^{h}}Q^{\prime}$, where $\alpha$ is a
$\tau$ or $\overline{a}b$.

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
for $x$ fresh for $P$, $Q$ and $h$, there exists $Q^{\prime}$ such that
$Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}^{h\cdot x^{o}}}Q^{\prime}$.

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.4787pt}{0.62pt}}\limits^{{{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
for $x$ is fresh for $P$, $Q$ and $h$, there exists $Q^{\prime}$ such that
$Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.4787pt}{0.62pt}}\limits^{{a(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}^{h\cdot x^{i}}}Q^{\prime}$.

Open bisimilarity, written $P\sim Q$, is defined whenever there exists an open
bisimulation $\mathcal{R}$ such that
$P\mathrel{\mathcal{R}^{x_{0}^{i}\cdot\ldots\cdot x_{n}^{i}}}Q$, where
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\subseteq\left\\{x_{0},\ldots,x_{n}\right\\}$.

The main result of this paper is that, for finite $\pi$-calculus processes
open bisimilarity is characterised by $\mathcal{OM}$ formulae. This result is
broken into soundness and completeness of the intuitionistic modal logic
characterisation.

######  Theorem 3.2 (soundness).

For $\pi$-calculus processes $P$ and $Q$ (including replication), If $P\sim Q$
then for all $\mathcal{OM}$ formulae $\phi$, $P\models\phi$ iff
$Q\models\phi$.

######  Theorem 3.3 (completeness).

For finite $\pi$-calculus processes $P$ and $Q$, if we have that for all
$\mathcal{OM}$ formulae $\phi$, $P\models\phi$ iff $Q\models\phi$, then $P\sim
Q$.

The proof of soundness has been mechanically checked in the proof assistant
Abella [BCG+14] using the two-level logic approach [GMN12] to reason about the
$\pi$-calculus semantics specified in $\lambda$Prolog [NM88]. The proof of
soundness proceeds by induction on the structure of the logical formulae in
the definition of logical equivalence. An explanation of the soundness proof
and mechanisation we defer until Section 5.

The proof of completeness is explained in detail in Section 4. Before
providing proofs, we provide examples demonstrating the implications of
Theorems 3.2 and 3.3. Due to soundness, if two processes are bisimilar, we
cannot find a distinguishing formula that holds for one process but does not
hold for the other process. Due to completeness, if it is impossible to prove
that two process are open bisimilar, then we can construct a distinguishing
formula that holds for one process but does not hold for the other process.
Thus $\mathcal{O\\!M}$ formulae can be used to certify when two processes are
not open bisimilar.

###  3.1. Sketch of algorithm for generating distinguishing formulae

The completeness proof, explained later in Section 4, contains an algorithm
for generating distinguishing formulae for non-bisimilar processes. Here, we
provide a sketch of the algorithm executed on key examples.

####  3.1.1. Example requiring intuitionistic assumptions

The algorithm proceeds over the structure of a tree of moves that show two
processes are not open bisimilar — the distinguishing strategy. In the base
case, we have a pair of processes where, under a substitution, one process can
make a transition, but the other process cannot match the transition. We
provide two examples of applying the base case to obtain formulae.

$\mathopen{\left[x=y\right]}\tau\not\sim\tau$:

The distinguishing strategy for these processes is the process $\tau$ leads
with transition $\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$,
but $\mathopen{\left[x\theta=y\theta\right]}\tau$ can make a $\tau$-transition
only when $x\theta=y\theta$. From this distinguishing strategy we generate two
formulae, one biased to each process. Since process $\tau$ leads in the
distinguishing strategy,
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ is a distinguishing
formula biased to process $\tau$, as follows.

$\tau\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\qquad\mbox{and}\qquad\mathopen{\left[x=y\right]}\tau\not\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

As remarked in the previous section, negating formula
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ does not provide a
formula biased to $\mathopen{\left[x=y\right]}\tau$. To construct a formula
biased towards $\mathopen{\left[x=y\right]}\tau$, write down a box modality
$\mathopen{\big{[}\tau\big{]}}$ followed by the strongest post-condition that
holds after a $\tau$-transition is enabled, i.e. $x=y$. This gives rise to the
following distinguishing formula, as required.

$\mathopen{\left[x=y\right]}\tau\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\qquad\mbox{and}\qquad\tau\not\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$

$\mathopen{\left[x=y\right]}\tau\not\sim 0$:

For these processes the distinguishing strategy is
$\left(\mathopen{\left[x=y\right]}\tau\right)\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$,
but $0$ cannot make a $\tau$-transition, under any substitution. To construct
a distinguishing formula biased to $\mathopen{\left[x=y\right]}\tau$, we write
down $x=y$ as the weakest pre-condition under which a $\tau$-transition is
enabled, expressed as follows.

$\mathopen{\left[x=y\right]}\tau\models\left(x=y\right)\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\qquad\mbox{and}\qquad
0\not\models\left(x=y\right)\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

To construct a formula biased to $0$, write $\mathopen{\big{[}\tau\big{]}}$
followed by $\mathtt{ff}$, which, vacuously, is the strongest post-condition
guaranteed after $0$ performs a $\tau$-transition, since no $\tau$-transition
is enabled under any substitution. This gives us the following distinguishing
formula.

$0\models\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\qquad\mbox{and}\qquad\mathopen{\left[x=y\right]}\tau\not\models\mathopen{\big{[}\tau\big{]}}\mathtt{ff}$

Now consider the inductive case of an algorithm for constructing
distinguishing formulae. In an inductive case, two processes cannot be
distinguished by an immediate transition. However, under some substitution,
one process can make a $\pi$ transition to a state, say $P^{\prime}$, but,
under the same substitution the other process can only make a corresponding
$\pi$ transition to reach states $Q_{i}$ that are non-bisimilar to
$P^{\prime}$. This allows a distinguishing formula to be inductively
constructed from the distinguishing formulae for $P^{\prime}$ paired with each
$Q_{i}$.

For example, consider how to construct distinguishing formulae for processes
$P$ and $Q$ below.

>
> $\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau}$$\textstyle{\\!\\!\\!\\!\triangleq\tau.\mathopen{\left[x=y\right]}\tau+\tau+\tau.\tau}$$\textstyle{\qquad\nsim\qquad}$$\textstyle{\tau+\tau.\tau\triangleq\\!\\!\\!\\!\\!}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau}$$\scriptstyle{\tau}$$\textstyle{\mathopen{\left[x=y\right]}\tau}$
> $\textstyle{0}$$\textstyle{\tau}$

Observe from the above transitions, that the process $P$ can perform a
$\tau$-transition to a state $\mathopen{\left[x=y\right]}\tau$ that is not
bisimilar to any state reachable by a $\tau$-transition from process $Q$.
Process $Q$ may perform $\tau$-transitions either to $\tau$ or $0$. However we
have just seen above that $\mathopen{\left[x=y\right]}\tau\not\sim 0$ and
$\mathopen{\left[x=y\right]}\tau\not\sim\tau$; hence we have a distinguishing
strategy.

The distinguishing strategies and distinguishing formulae for the above base
cases, enable us to construct distinguishing formulae for this inductive case.
The distinguishing formula satisfied by $P$ is a diamond modality followed by
the conjunction of the distinguishing formulae biased to
$\mathopen{\left[x=y\right]}\tau$ in each base case above, as follows.

$P\models\mathopen{\mathopen{\big{\langle}\tau\big{\rangle}}}\left(\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\right)\qquad\mbox{and}\qquad
Q\not\models\mathopen{\mathopen{\big{\langle}\tau\big{\rangle}}}\left(\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\right)\right)$

The distinguishing formula satisfied by $Q$ is a box followed by the
disjunction of the formulae not satisfied by $\mathopen{\left[x=y\right]}\tau$
in each of the base cases above, as follows:

$P\not\models\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\qquad\mbox{and}\qquad
Q\models\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)$

To confirm that the above are indeed distinguishing formulae for $P$ and $Q$,
assume for contradiction that
$Q\models\mathopen{\mathopen{\big{\langle}\tau\big{\rangle}}}\left(\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\right)$
holds. By definition of diamond modalities, this holds iff either
$0\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
or
$\tau\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
holds. Observe that $0\models
x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ holds iff we
make the additional assumption that $x$ and $y$ are persistently distinct,
i.e., we have additional assumption $\mathopen{\neg}\left(x=y\right)$. In
addition, observe that
$\tau\models\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$ holds iff we make
the additional assumption that $x=y$.

Indeed, by these observations know that the following hold:

$\tau+\tau.\tau\models\left(x=y\vee\mathopen{\neg}\left(x=y\right)\right)\supset\mathopen{\mathopen{\big{\langle}\tau\big{\rangle}}}\left(\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\right)$
$\tau+\tau.\tau\models\mathopen{\mathopen{\big{\langle}\tau\big{\rangle}}}\left(\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\right)\supset\left(x=y\vee\mathopen{\neg}\left(x=y\right)\right)$

Notice that $x=y\vee\mathopen{\neg}\left(x=y\right)$ is an instance of the law
of excluded middle for name equality; hence, in the classical setting,
assuming the law of excluded middle, the formula above biased to $Q$ is also
satisfied by $P$; and vice versa. Indeed there would be no distinguishing
formulae for processes $P$ and $Q$; and hence in a classical framework the
modal logic would be incomplete for open bisimilarity.

Similarly, in the intuitionistic setting, we can mechanically prove the
following.

$\tau+\tau.\tau+\tau.\mathopen{\left[x=y\right]}\tau\models\left(x=y\vee\mathopen{\neg}\left(x=y\right)\right)\supset\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)$
$\tau+\tau.\tau+\tau.\mathopen{\left[x=y\right]}\tau\models\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\supset\left(x=y\vee\mathopen{\neg}\left(x=y\right)\right)$

Since intuitionistic logics do not assume the law of excluded middle, as long
as we evaluate the semantics of $\mathcal{OM}$ in an intuitionistic framework,
we have distinguishing formulae. We have formalised in Abella the above four
examples of satisfaction involving excluded middle.

####  3.1.2. Example involving private names that are distinguishable

Respectful substitutions ensure that a private name can never be input earlier
than it was output. Consider the following processes.

$P\triangleq\nu x.\overline{a}x.a(y).\tau\quad\nsim\quad\nu
x.\overline{a}x.a(y).\mathopen{\left[x=y\right]}\tau\triangleq Q$

These processes are not open bisimilar because $P$ can make the following
three transition steps: $\nu x.\overline{a}x.a(y).\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}a(y).\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.16112pt}{0.62pt}}\limits^{{a(y)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$.
However, $Q$ can only match the first two steps. At the third step, a base
case of the distinguishing formula algorithm for $\tau\not\sim^{a^{i}\cdot
x^{o}\cdot y^{i}}\mathopen{\left[x=y\right]}\tau$ applies. In this case, any
substitution $\theta$ respecting $a^{i}\cdot x^{o}\cdot y^{i}$ enabling
transition $\mathopen{\left[x=y\right]}\tau\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
is such that $y\theta=x$ and $x\theta=x$; hence $x\theta=y\theta$. Hence we
have the following formulae biased to each process.

$\mathopen{\left[x=y\right]}\tau\models^{a^{i}\cdot x^{o}\cdot
y^{i}}\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\qquad\mbox{and}\qquad\tau\models^{a^{i}\cdot
x^{o}\cdot y^{i}}\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$

By applying inductive cases, to the input and output actions we obtain the
following two distinguishing formulae.

$\nu
x.\overline{a}x.a(y).\tau\models\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\mathopen{\big{\langle}a(y)\big{\rangle}}\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\qquad\mbox{and}\qquad\nu
x.\overline{a}x.a(y).\mathopen{\left[x=y\right]}\tau\models\mathopen{\big{[}\overline{a}(x)\big{]}}\mathopen{\big{[}a(y)\big{]}}\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$

####  3.1.3. Example involving private names that are indistinguishable

In contrast to the previous example, consider the following processes where a
fresh name is output and compared to a name already known.

$\nu x.\overline{a}x\quad\sim\quad\nu
x.\overline{a}x.\mathopen{\left[x=a\right]}\tau$

These processes are open bisimilar, hence by Theorem 3.2 there is no
distinguishing formula. The existence of a distinguishing formula of the form
$\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
is _prevented_ by the history. For example, both $\nu
x.\overline{a}x.\mathopen{\left[x=a\right]}\tau\models\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
and $\nu
x.\overline{a}x\models\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
hold.

To see why, observe $\nu
x.\overline{a}x\models^{a^{i}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
holds if and only if $\nu x.\overline{a}x\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
and $0\models^{a^{i}\cdot
x^{o}}x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$. By
definition of implication, this holds if only if, for all $\theta$ respecting
$a^{i}\cdot x^{o}$ and such that $x\theta=a\theta$, we have
$0\models^{a^{i}\cdot
x^{o}}\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$. However, there is
no substitution $\theta$ respecting $a^{i}\cdot x^{o}$ such that
$x\theta=a\theta$. By the definition of a respectful substitution, $\theta$
must satisfy $x\theta=x$ and $x\not=a\theta$, contradicting constraint
$x\theta=a\theta$. Thereby $0\models^{a^{i}\cdot
x^{o}}x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ holds
vacuously; hence we have that $\nu
x.\overline{a}x\models^{a^{i}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)$
holds as required.

##  4\. Completeness of open bisimilarity with respect to $\mathcal{O\\!M}$

In order to prove completeness we first provide a direct definition of what it
means for two processes to be not open bisimilar, referred to as non-
bisimilarity. Since open bisimilarity is defined in terms of a greatest fixed
point of relations satisfying a certain closure property, non-bisimilarity is
defined in terms of a least fixed point satisfying the dual property. This
leads to the direct definition of non-bisimilarity in this section.

Since non-bisimilarity is defined in terms of a least fixed point, there is a
winning strategy, consisting of a finite tree of moves. We inductively define
non-bisimilarity in terms of a family of relations on processes indexed by a
history $\not\sim_{n}$, for $n\in\mathbb{N}$. The base case is when, for some
respectful substitution one player can make a move, that cannot be matched by
the other player without assuming a stronger substitution. We then define
inductively, the family of relations $P\not\sim_{n}^{h}Q$ containing all
processes that can be distinguished by a strategy with depth at most $n$,
i.e., at most $n$ moves are required to reach a pair of processes in
$\not\sim_{0}$, at which point there is an accessible world in which a process
can make a move that the other process cannot match.

######  Definition 4.1 (non-bisimilarity).

Relation $\not\sim_{0}$ is the least relation such that $P\not\sim^{h}_{0}Q$
holds whenever there exist action $\pi$ and substitution $\sigma$ respecting
$h$ such that one of the following holds:

  * •

there exists process $P^{\prime}$ such that $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
and there is no $Q^{\prime}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$,
or

  * •

there exist process $Q^{\prime}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and there is no $P^{\prime}$ such that $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$.

In both case, we require that if $x\in\mathopen{\mathrm{bn}}\left(\pi\right)$,
then $x$ is fresh for $P\sigma$, $Q\sigma$ and $h\sigma$.

Inductively, $\not\sim_{n+1}$ is the least relation extending $\not\sim_{n}$
such that $P\not\sim^{h}_{n+1}Q$ whenever for some substitution $\sigma$
respecting $h$, one of the following holds, where, in the following, $\alpha$
is $\tau$ or $\overline{a}b$ and $x$ is fresh for $P\sigma$, $Q\sigma$ and
$h\sigma$:

  * •

$\exists P^{\prime}.~{}P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
and $\forall Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma}_{n}Q_{i}$.

  * •

$\exists P^{\prime}.~{}P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
and, $\forall Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma\cdot x^{o}}_{n}Q_{i}$.

  * •

$\exists P^{\prime}.~{}P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
and, $\forall Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma\cdot x^{i}}_{n}Q_{i}$.

  * •

$\exists Q^{\prime}.~{}Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $\forall P_{i}$ such that $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P_{i}$,
$P_{i}\not\sim^{h\sigma}_{n}Q^{\prime}$.

  * •

$\exists Q^{\prime}.~{}Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$,
and, $\forall P_{i}$ such that $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P_{i}$,
$Q^{\prime}\not\sim^{h\sigma\cdot x^{o}}_{n}P_{i}$.

  * •

$\exists Q^{\prime}.~{}Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$,
and, $\forall P_{i}$ such that $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P_{i}$,
$Q^{\prime}\not\sim^{h\sigma\cdot x^{i}}_{n}P_{i}$.

The relation $\not\sim$, pronounced non-bisimilarity, is defined to be the
least relation containing $\not\sim_{n}$ for all $n\in\mathbb{N}$, i.e.
$\bigcup_{n\in\mathbb{N}}\not\sim_{n}$. Define $P\not\sim Q$ whenever
$P\not\sim^{x_{1}^{i}\cdot\ldots x_{m}^{i}}Q$ where
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\subseteq\left\\{x_{1},\ldots
x_{m}\right\\}$.

######  Lemma 4.2.

The relations $\not\sim$ and $\not\sim_{n}$, for all $n\geq 0$, are symmetric.

###  4.1. Preliminaries

For the completeness proof that follows, we require the following terminology
for substitutions, and abbreviations for formulae. These are mainly standard.

######  Definition 4.3.

Composition of substitutions $\sigma$ and $\theta$ is defined such that
$x\left(\sigma\cdot\theta\right)=\left(x\sigma\right)\theta$, for all $x$. For
substitutions $\sigma$ and $\theta$, $\sigma\leq\theta$ whenever there exists
$\sigma^{\prime}$ such that $\sigma\cdot\sigma^{\prime}=\theta$. For a finite
substitution
$\sigma={\mathclose{\\{^{z_{1}\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x_{1}}\\}}\cdots\,\mathclose{\\{^{z_{n}\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x_{n}}\\}}}$
the formula $\mathopen{\big{[}\sigma\big{]}}\phi$ abbreviates the formula
$\left(x_{n}=z_{n}\right)\supset\ldots\left(x_{1}=z_{1}\right)\supset\phi$.
For finite set of formulae $\phi_{i}$, formula $\bigvee_{i}\phi_{i}$
abbreviates $\phi_{1}\vee\\!\ldots\\!\vee\phi_{n}$, where the empty
disjunction is $\mathtt{ff}$. Similarly $\bigwedge_{i}\phi_{i}$ abbreviates
$\phi_{1}\wedge\ldots\wedge\phi_{n}$, where the empty conjunction is
$\mathtt{tt}$.

We require the following technical lemmas. The first, image finiteness,
ensures that there are finitely many reachable states in one step, up to
renaming. The second unfolds the definition of box substitution abbreviation,
defined above. The third is required in inductive cases involving bound output
and input. The fourth is a monotonicity property for satisfaction. The fifth
is a monotonicity property for transitions, assuming names bound by labels are
not changed by a substitution.

######  Lemma 4.4.

For process $P$ and action $\pi$ there are finitely many $P_{i}$ such that
$P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P_{i}$.

######  Lemma 4.5.

If for all $\theta$ respecting $h$ and $\sigma\leq\theta$, it holds that
$P\theta\models^{h\theta}\phi\theta$, then
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\phi$ holds.

######  Lemma 4.6.

If $\sigma\cdot\theta$ respects $h$, then $\theta$ respects $h\sigma$.

######  Lemma 4.7.

If $P\models^{h}\phi$ holds then $P\theta\models^{h\theta}\phi\theta$ holds
for any $\theta$ respecting $h$.

######  Lemma 4.8.

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q$
then $P\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q\theta$,
for all $\theta$ such that if $x\in\mathopen{\mathrm{bn}}\left(\pi\right)$ and
$y\theta=x$ then $x=y$.

###  4.2. Algorithm for distinguishing formulae

The direct definition of non-bisimilarity gives a tree of substitutions and
actions forming a strategy showing that two processes are not open bisimilar.
The following proposition shows that $\mathcal{O\\!M}$ formulae are sufficient
to capture such strategies. For any strategy that distinguishes two processes,
we can construct distinguishing $\mathcal{O\\!M}$ formulae. A distinguishing
formula holds for one process but not for the other process. Furthermore,
there are always at least two distinguishing formulae, one biased to the left
and another biased to the right, as in the construction of the proof for the
following proposition. As discussed in Section 2, the left biased formula
cannot be simply obtained by negating the right biased formula and vice versa;
both must be constructed simultaneously and may be unrelated by negation.

######  Proposition 4.9.

If $P\not\sim Q$ then there exists $\phi_{L}$ such that $P\models\phi_{L}$ and
$Q\not\models\phi_{L}$, and also there exists $\phi_{R}$ such that
$Q\models\phi_{R}$ and $P\not\models\phi_{R}$.

###### Proof.

Since $\not\sim$ is defined by a least fixed point over a family of relations
$\not\sim_{n}$, if $P\not\sim^{h}Q$, there exists $n$ such that
$P\not\sim_{n}^{h}Q$, so we can proceed by induction on the depth of a winning
strategy.

In the base case, assume $P\not\sim_{0}^{h}Q$, hence by definition, for
substitution $\sigma$ respecting $h$, $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
for $x\in\mathopen{\mathrm{bn}}\left(\pi\right)$, $x$ is fresh for $P\sigma$,
$Q\sigma$ and $h\sigma$, such that there is no $Q^{\prime}$ such that
$Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$,
up to symmetry of $\not\sim_{n}^{h}$.

We require the following property concerning substitutions enabling
$\pi\theta$-transitions from $Q\theta$, exploiting the observation that
necessarily each such $\theta$ must induce an additional equality that was not
yet enabled by $\sigma$. There exist finitely many pairs of variables $x_{j}$
and $y_{j}$ in
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\mathopen{\mathrm{fn}}\left(\pi\right)$
such that $x_{j}\sigma$ and $y_{j}\sigma$ are distinct, and, for any $R$ and
substitution $\theta$ respecting $h$, if $Q\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}R$
there exists $j$ such that $x_{j}\theta=y_{j}\theta$. To see why, assume for
contradiction that there is some $\theta$ respecting $h$ such that
$Q\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}R$
but there is no $x$ and $y$ in
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\mathopen{\mathrm{fn}}\left(\pi\right)$
such that $x\sigma$ and $y\sigma$ are distinct, and $x\theta=y\theta$. Stated
otherwise, for all $x$ and $y$ in
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\mathopen{\mathrm{fn}}\left(\pi\right)$
if $x\theta=y\theta$ then $x\sigma=y\sigma$, which is precisely the definition
of a function, i.e., substitution, say $\theta^{\prime}$, defined on the range
of $\theta$ such that $\theta^{\prime}$ maps $z\theta$ to $z\sigma$. In that
case, $\theta\cdot\theta^{\prime}=\sigma$ on
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\mathopen{\mathrm{fn}}\left(\pi\right)$;
and hence, by Lemma 4.8, $Q\theta\theta^{\prime}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{14.99582pt}{0.62pt}}\limits^{{\pi\theta\theta^{\prime}}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}R\theta^{\prime}$
contradicting the initial assumption for the base case that no transition
$Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
exists for any $Q^{\prime}$.

In this case, there are two distinguishing formulae
$\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$
and $\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)$ biased
to $P$ and $Q$ respectively. There are four cases to check to confirm that
these are distinguishing formulae.

Case
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}\,$:

Consider all $\theta$ respecting $h$ such that $\sigma\leq\theta$. By
definition there exists $\theta^{\prime}$ such that
$\sigma\cdot\theta^{\prime}=\theta$, so since $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
by Lemma 4.8, $P\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}\theta^{\prime}$.
Thereby, since $P^{\prime}\theta^{\prime}\models^{h^{\prime}}\mathtt{tt}$
holds,
$P\theta\models^{h\theta}\mathopen{\big{\langle}\pi\theta\big{\rangle}}\mathtt{tt}$.
Hence, by Lemma 4.5,
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$.

Case
$Q\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}\,$:

For contradiction, assume
$Q\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$.
Since $\sigma$ respects $h$ and $\sigma\leq\sigma$, by Lemma 4.5,
$Q\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$
holds only if
$Q\sigma\models^{h\sigma}\mathopen{\big{\langle}\pi\sigma\big{\rangle}}\mathtt{tt}$
holds; which holds only if there exists $Q^{\prime}$ such that
$Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$,
contradicting the assumption no such $Q^{\prime}$ exists. Thereby
$Q\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$.

Case
$Q\models^{h}\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)\,$:

Consider substitutions $\theta$ respecting $h$ and $Q^{\prime}$ such that
$Q\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$.
It must be the case that there exists $j$ such that $x_{j}\theta=y_{j}\theta$,
thereby $Q^{\prime}\models^{h\theta}x_{j}\theta=y_{j}\theta$ holds; hence
clearly
$Q^{\prime}\models^{h\theta}\bigvee_{j}\left(x_{j}=y_{j}\right)\mathclose{\theta}$
holds. Hence
$Q\models^{h}\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)$.

Case
$P\not\models^{h}\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)\,$:

Assume for contradiction
$P\models^{h}\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)$.
This holds iff for all processes $S$ and substitutions $\theta$ respecting
$h$, $P\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\theta}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}S$
implies
$S\models^{h^{\prime}}\bigvee_{j}\left(x_{j}=y_{j}\right)\mathclose{\theta}$.
Since we know that $\sigma$ respects $h$ and $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\pi\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
for some $h^{\prime\prime}$, we have
$P^{\prime}\models^{h^{\prime\prime}}\bigvee_{j}\left(x_{j}=y_{j}\right)\mathclose{\sigma}$.
This holds only if for some $j$,
$P^{\prime}\models^{h^{\prime\prime}}x_{j}\sigma=y_{j}\sigma$; hence,
$x_{j}\sigma=y_{j}\sigma$ for some $j$, which contradicts the assumption that
$x_{j}\sigma$ and $y_{j}\sigma$ are distinct. Thereby
$P\not\models^{h}\mathopen{\big{[}\pi\big{]}}\bigvee_{j}\left(x_{j}=y_{j}\right)$.

Now consider the inductive cases. Given $P$, $Q$, if $P\not\sim_{n+1}^{h}Q$,
up to symmetry of $\not\sim_{n+1}^{h}$, there are three cases to consider, for
some substitution $\sigma$ respecting $h$, where $\alpha$ is either $\tau$ or
$\overline{a}b$, where $x$ is fresh for $P\sigma$, $Q\sigma$ and $h\sigma$:

  * •

$P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
and for all $Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha\sigma}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma}_{n}Q_{i}$.

  * •

$P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
and, for all $Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma\cdot x^{o}}_{n}Q_{i}$.

  * •

$P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
and, for all $Q_{i}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$,
$P^{\prime}\not\sim^{h\sigma\cdot x^{i}}_{n}Q_{i}$.

We consider the second case above involving bound output only, the other two
cases are similar — differing only in the accounting for respectful
substitutions according to Def. 2.1.

For $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
by Lemma 4.4, there exist finitely many $Q_{i}$ such that
$Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}$.
For each $i$, since $P^{\prime}\not\sim^{h\sigma\cdot x^{o}}_{n}Q_{i}$, by the
induction hypothesis, there exist $\phi^{L}_{i}$ and $\phi^{R}_{i}$ such that
$P^{\prime}\models^{h\sigma\cdot x^{o}}\phi^{L}_{i}\sigma$ and
$Q_{i}\not\models^{h\sigma\cdot x^{o}}\phi^{L}_{i}\sigma$ and
$P^{\prime}\not\models^{h\sigma\cdot x^{o}}\phi^{R}_{i}\sigma$ and
$Q_{i}\models^{h\sigma\cdot x^{o}}\phi^{R}_{i}\sigma$.

We require the following property, referred to later using $\dagger$. There
are finitely many pairs of variables $x_{j}$ and $y_{j}$ selected from
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\left\\{a\right\\}$
such that $x_{j}\sigma$ and $y_{j}\sigma$ are distinct, and, for any
substitution $\theta$ respecting $h$ (note we can apply $\alpha$-conversion to
ensure that $\theta$ also respects $h\cdot x^{o}$), such that
$\sigma\leq\theta$, and for any $S$ such that, $Q\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\theta}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}S$
then either: for some $i$, we have $S\models^{h\theta\cdot
x^{o}}\phi^{R}_{i}\theta$, or there exists some $j$ such that
$x_{j}\theta=y_{j}\theta$.

To see why such pairs of variables $x_{j}$ and $y_{j}$ can be constructed,
suppose, for contradiction, that they cannot be constructed in general. Hence,
there would exist substitution $\rho$ respecting $h\cdot x^{o}$, where
$\sigma\leq\rho$, and process $S$ such that: $Q\rho\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\rho}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}S$,
there is no $i$ such that $S\models^{h\rho\cdot x^{o}}\phi^{R}_{i}\rho$, and
also there is no pair of variables $u$ and $v$ in
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\cup\left\\{a\right\\}$
such that $u\sigma$ and $v\sigma$ are distinct and $u\rho=v\rho$. Hence
$\rho\leq\sigma$; therefore, there exists $\rho^{\prime}$ respecting
$h\rho\cdot x^{o}$ such that $\rho\cdot\rho^{\prime}=\sigma$ and hence, by
Lemma 4.8, $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}S\rho^{\prime}$,
where $S\rho^{\prime}=Q_{i}$ for some $i$. Since, $\rho\leq\sigma$ and
$\sigma\leq\rho$, we know $\rho^{\prime}$ has an inverse, say
$\sigma^{\prime}$. Now since, by Lemma 4.8,
$Q\sigma\sigma^{\prime}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma\sigma^{\prime}}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}\sigma^{\prime}$,
we have $Q\rho\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\rho}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q_{i}\sigma^{\prime}$;
and, since $Q_{i}\models^{h\sigma\cdot x^{o}}\phi^{R}_{i}\sigma$, by Lemma
4.7, we have $Q_{i}\sigma^{\prime}\models^{h\rho\cdot x^{o}}\phi^{R}_{i}\rho$,
i.e., $S\models^{h\rho\cdot x^{o}}\phi^{R}_{i}\rho$, contradicting the
assumption no such $i$ exists.

From the above, distinguishing formulae
$\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$
and
$\mathopen{\big{[}\sigma\big{]}}\mathopen{\mathopen{\big{[}\overline{a}(x)\big{]}}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left(x_{j}=y_{j}\right)\right)$
can be constructed. There are four cases to consider to verify these are
distinguishing formulae.

Case
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$
:

Consider all $\theta$ such that $\sigma\leq\theta$, $\theta$ respects $h$, and
without loss of generality $x$ is fresh for $\theta$, i.e., for
$y\in\mathopen{\mathrm{dom}}\left(\theta\right)$ and $x\not\in y\theta$. By
definition, there exists $\theta^{\prime}$ such that
$\sigma\cdot\theta^{\prime}=\theta$. Now since $\sigma\cdot\theta^{\prime}$
respects $h$, by Lemma 4.6, $\theta^{\prime}$ respects $h\sigma$ hence since
$x\not\in\mathopen{\mathrm{dom}}\left(\theta^{\prime}\right)$ and
$x\not\in\mathopen{\mathrm{fn}}\left(h\sigma\theta^{\prime}\right)$,
$\theta^{\prime}$ respects $h\sigma\cdot x^{o}$. Thereby since
$\theta^{\prime}$ respects $h\sigma\cdot x^{o}$ and also
$P^{\prime}\models^{h\sigma\cdot x^{o}}\phi^{L}_{i}\sigma$ holds, by Lemma
4.7, it holds that $P^{\prime}\theta^{\prime}\models^{h\theta\cdot
x^{o}}\phi^{L}_{i}\theta$. The above holds for all $i$, hence it holds that
$P^{\prime}\theta^{\prime}\models^{h\theta\cdot
x^{o}}\bigwedge_{i}\phi^{L}_{i}\theta$. Now, since $P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
by Lemma 4.8, since $x$ is fresh, $P\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\theta}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}\theta^{\prime}$
holds; and hence
$P\theta\models^{h\theta}\left(\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}\right)\mathclose{\theta}$
holds. Thereby, by Lemma 4.5,
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$
holds.

Case
$Q\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$
:

Assume for contradiction that
$Q\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$
holds. Since $\sigma$ respects $h$ and $\sigma\leq\sigma$, by Lemma 4.5, the
above assumption holds only if
$Q\sigma\models^{h\sigma}\left(\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}\right)\mathclose{\sigma}$
holds. Now
$Q\sigma\models^{h\sigma}\mathopen{\big{\langle}\overline{a\sigma}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}\mathclose{\sigma}$
holds only if there exists $Q^{\prime}$ such that $Q\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $Q^{\prime}\models^{h\sigma\cdot x^{o}}\bigwedge_{i}\phi^{L}_{i}\sigma$,
which holds only if $Q^{\prime}\models^{h\sigma\cdot x^{o}}\phi^{L}_{i}\sigma$
for all $i$. Notice that $Q^{\prime}=Q_{k}$ for some $k$, and therefore
$Q_{k}\models^{h\sigma\cdot x^{o}}\phi^{L}_{k}\sigma$; but it was assumed that
$Q_{k}\not\models^{h\sigma\cdot x^{o}}\phi^{L}_{k}\sigma$ leading to a
contradiction. Therefore
$Q\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{\langle}\overline{a}(x)\big{\rangle}}\bigwedge_{i}\phi^{L}_{i}$.

Case
$Q\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{[}\overline{a}(x)\big{]}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left(x_{j}=y_{j}\right)\right)$
:

Fix $Q^{\prime}$ and $\theta$ respecting $h$, such that $\sigma\leq\theta$,
and $Q\theta\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\theta}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$.
Above, in $\dagger$, we established that, in this scenario, either: for some
$\ell$, we have $Q^{\prime}\models^{h\theta\cdot x^{o}}\phi^{R}_{\ell}\theta$,
or there exists some $k$ such that $x_{k}\theta=y_{k}\theta$. In the case
where, for some $k$, $x_{k}\theta=y_{k}\theta$, we have
$Q^{\prime}\models^{h\theta\cdot x^{o}}{x_{k}\theta=y_{k}\theta}$ holds. Hence
in either case we have $Q^{\prime}\models^{h\theta\cdot
x^{o}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)\mathclose{\theta}$,
by definition of disjunction. Thereby, by definition,
$Q\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{[}\overline{a}(x)\big{]}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)$
holds.

Case
$P\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{[}\overline{a}(x)\big{]}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)$
:

Assume
$P\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{[}\overline{a}(x)\big{]}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)$
for contradiction. Since $\sigma$ respects $h$, $\sigma\leq\sigma$, and
$P\sigma\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a\sigma}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$,
the previous assumption can hold only if $P^{\prime}\models^{h\sigma\cdot
x^{o}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)\mathclose{\sigma}$.
This holds only if, for some $i$, $P^{\prime}\models^{h\sigma\cdot
x^{o}}\phi^{R}_{i}\sigma$, or, for some $j$, $P^{\prime}\models^{h\sigma\cdot
x^{o}}\left({x_{j}\sigma=y_{j}\sigma}\right)$. However, for all $i$,
$P^{\prime}\not\models^{h\sigma\cdot x^{o}}\phi^{R}_{i}\sigma$; and also, for
all $j$, we have $x_{j}\sigma$ and $y_{j}\sigma$ are distinct and
$P^{\prime}\not\models^{h\sigma\cdot
x^{o}}\left({x_{j}\sigma=y_{j}\sigma}\right)$, leading to a contradiction in
either case. Thereby
$P\not\models^{h}\mathopen{\big{[}\sigma\big{]}}\mathopen{\big{[}\overline{a}(x)\big{]}}\left(\bigvee_{i}\phi^{R}_{i}\vee\bigvee_{j}\left({x_{j}=y_{j}}\right)\right)$.

By induction we have established that, for any history $h$, processes $P$ and
$Q$, and any $n$, if $P\not\sim^{h}_{n}Q$ then we can construct $\phi_{L}$
such that $P\models^{h}\phi_{L}$ and $Q\not\models^{h}\phi_{L}$; and also we
can construct $\phi_{R}$ such that $Q\models^{h}\phi_{R}$ and
$P\not\models^{h}\phi_{R}$. The result then follows by observing that, since
$\not\sim$ is the least relation containing all $\not\sim_{n}$ whenever
$P\not\sim Q$; there exists $n$ such that
$P\not\sim^{x_{1}^{i}\cdot\ldots\cdot x^{i}_{n}}_{n}Q$ and, where
$\mathopen{\mathrm{fn}}\left(P\right)\cup\mathopen{\mathrm{fn}}\left(Q\right)\subseteq\left\\{x^{i}_{1},\ldots,x^{i}_{n}\right\\}$;
for which, there is $\phi^{L}$ such that $P\models^{x_{1}^{i}\cdot\ldots\cdot
x^{i}_{n}}\phi_{L}$ and $Q\not\models^{x_{1}^{i}\cdot\ldots\cdot
x^{i}_{n}}\phi_{L}$; and also $\phi^{R}$ such that
$Q\models^{x_{1}^{i}\cdot\ldots\cdot x^{i}_{n}}\phi_{R}$ and
$P\not\models^{x_{1}^{i}\cdot\ldots\cdot x^{i}_{n}}\phi_{R}$. Hence, by
Definition 2.2, indeed $P\models\phi_{L}$, $Q\not\models\phi_{L}$,
$Q\models\phi_{R}$ and $P\not\models\phi_{R}$ as required. ∎

###  4.3. The proof of completeness

Since open bisimilarity is decidable for finite $\pi$-calculus processes,
Definition 4.1 coincides with the negation of open bisimilarity.

######  Lemma 4.10.

For finite processes, $P\not\sim Q$ holds, according to non-bisimilarity in
Definition 4.1, if and only if $P\sim Q$ does not hold.

Combining Proposition 4.9 with Lemma 4.10 yields immediately the completeness
of $\mathcal{O\\!M}$ with respect to open bisimilarity. Completeness (Theorem
3.3) establishes that the set of all pairs of processes that have the same set
of distinguishing formulae is an open bisimulation. The proof can now be
stated as follows.

Proof of Theorem 3.3: Assume that for finite processes $P$ and $Q$, for all
formulae $\phi$, $P\models\phi$ iff $Q\models\phi$. Now for contradiction
suppose that $P\sim Q$ does not hold. By Lemma 4.10, $P\not\sim Q$ must hold.
Hence by Proposition 4.9 there exists $\phi_{L}$ such that $P\models\phi_{L}$
but $Q\not\models\phi_{L}$, but by the assumption above $Q\models\phi_{L}$,
leading to a contradiction. Thereby $P\sim Q$. ∎

Notice that soundness (Theorem 3.2) and the non-bisimilarity algorithm
(Proposition 4.9) also hold for infinite $\pi$-calculus processes (using
replication for instance). However, for infinite $\pi$-calculus processes,
open bisimilarity is undecidable; hence additional insight may be needed to
justify whether Lemma 4.10 holds for infinite processes. Thereby in the
infinite case, while it is impossible both $P\sim Q$ and $P\not\sim Q$ hold,
it may be possible neither holds. This is an open problem.

###  4.4. Example runs of distinguishing formulae algorithm

We provide further examples of non-bisimilar processes that illustrate subtle
aspects of the algorithm. In particular, these examples illustrate various
scenarios where postconditions are required.

####  4.4.1. Multiple postconditions and postconditions in an inductive step

The following example leads to multiple postconditions. Consider the following
non-bisimilar processes.

$\mathopen{\left[x=y\right]}\tau+[w=z]\tau\qquad\not\sim\qquad\tau$

Observe that clearly $\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
but
$\left(\mathopen{\left[x=y\right]}\tau+[w=z]\tau\right)\mathclose{\theta}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}$
only if $x\theta=y\theta$ or $w\theta=z\theta$. Thus,
$\mathopen{\left[x=y\right]}\tau+[w=z]\tau\models\mathopen{\mathopen{\big{[}\tau\big{]}}}\left((x=y)\vee(w=z)\right)$
is a distinguishing formula biased to the left process, while
$\tau\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ is biased to
the right.

We consider an example where postconditions are required in the inductive
case. However, firstly observe that
$\overline{a}a+\overline{b}b\not\sim\overline{a}a$ are distinguished since
$\overline{a}a+\overline{b}b\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\overline{b}b}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$,
but process $\overline{a}a$ can only make a $\overline{b}b$ transition under a
substitution such that $a=b$. Hence we have the distinguishing formulae
$\overline{a}a+\overline{b}b\models\mathopen{\big{\langle}\overline{b}b\big{\rangle}}\mathtt{tt}$
and $\overline{a}a\models\mathopen{\big{[}\overline{b}b\big{]}}(a=b)$. Now
consider the following.

$P\triangleq\mathopen{\tau.}\left(\overline{a}a+\overline{b}b\right)+\mathopen{\left[x=y\right]}\tau.\overline{a}a\qquad\not\sim\qquad\mathopen{\tau.}\left(\overline{a}a+\overline{b}b\right)+\tau.\overline{a}a\triangleq
Q$

To distinguishing these processes $Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\overline{a}a$
leads, which can only be matched by $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\overline{a}a+\overline{b}b$.
By the previous example, we have distinguishing formulae for
$\overline{a}a+\overline{b}b\not\sim\overline{a}a$. However, also observe, for
substitutions $\theta$ such that $x\theta=y\theta$, there is an additional
$\tau$-transitions enabled: $P{\theta}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\overline{a}a$.

This leads to the following distinguishing formula for the left side,
consisting of a box $\tau$ followed by a disjunction comprised of the left
distinguishing formula for $\overline{a}a+\overline{b}b\not\sim\overline{a}a$,
and the postcondition $x=y$ guaranteed after the additional $\tau$ transition.

$\mathopen{\tau.}\left(\overline{a}a+\overline{b}b\right)+\mathopen{\left[x=y\right]}\tau.\overline{a}a\models\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{\langle}\overline{b}b\big{\rangle}}\mathtt{tt}\vee
x=y\right)$

The distinguishing formula for the right process is diamond $\tau$ followed by
the right distinguishing formula for
$\overline{a}a+\overline{b}b\not\sim\overline{a}a$, as follows:
$\mathopen{\tau.}\left(\overline{a}a+\overline{b}b\right)+\tau.\overline{a}a\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathopen{\big{[}\overline{b}b\big{]}}(a=b)$.

####  4.4.2. Formulae generated by substitutions applied to labels

In some cases substitutions applied to labels play a role when generating
distinguishing formulae. For a minimal example consider the following non-
bisimilar processes: $\overline{a}a\not\sim\overline{a}b$. A distinguishing
strategy is where process $\overline{a}b$ makes a $\overline{a}b$ transition,
which cannot be matched by $\overline{a}a$. However,
$\left(\overline{a}a\right)\mathclose{\sigma}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{20.78197pt}{0.62pt}}\limits^{{\left(\overline{a}b\right)\mathclose{\sigma}}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
for any substitution such that $a\sigma=b\sigma$, leading to distinguishing
formula $\mathopen{\big{[}\overline{a}b\big{]}}(a=b)$ biased to
$\overline{a}a$. Notice substitution $\sigma$ is applied to both the process
and the label.

For a trickier example consider the following processes.

$\nu b.\overline{a}b.a(x).\mathopen{\left[x=b\right]}\overline{x}x\not\sim\nu
b.\overline{a}b.a(x).\overline{x}x$

After two actions, the above problem reduces to base case
$\mathopen{\left[x=b\right]}\overline{x}x\not\sim^{a^{i}\cdot b^{o}\cdot
x^{i}}\overline{x}x$, where $\overline{x}x$ can perform a $\overline{x}x$
action, but $\mathopen{\left[x=b\right]}\overline{x}x$ cannot. However,
$\left(\mathopen{\left[x=b\right]}\overline{x}x\right)\mathclose{\\{^{b\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{29.12032pt}{0.62pt}}\limits^{{\overline{x}x\mathclose{\\{^{b\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
does hold, and furthermore
$\mathclose{\\{^{b\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$
respects $a^{i}\cdot b^{o}\cdot x^{i}$. From these observations we can
construct a distinguishing formula biased to the left as follows.

$\nu
b.\overline{a}b.a(x).\mathopen{\left[x=b\right]}\overline{x}x\models\mathopen{\big{[}a(b)\big{]}}\mathopen{\big{[}a(x)\big{]}}\mathopen{\big{[}\overline{x}x\big{]}}(x=b)$

####  4.4.3.  Alternative forms for distinguishing formulae

Note our algorithm copes with sub-optimal distinguishing strategies. To
understand this, consider the distinguishing strategy for the following
processes that are clearly not open bisimilar.

$\mathopen{\left[x=y\right]}\tau\qquad\not\sim\qquad\tau.\mathopen{\left[x=y\right]}\tau$

There is an obvious optimal distinguishing strategy:
$\tau.\mathopen{\left[x=y\right]}\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\mathopen{\left[x=y\right]}\tau$,
which cannot be matched by $\mathopen{\left[x=y\right]}\tau$. By appealing to
the base case of the distinguishing formulae algorithm, we obtain two
distinguishing formulae $\mathopen{\big{[}\tau\big{]}}\left(x=y\right)$ and
$\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$ biased each respective
process.

There are however, sub-optimal, distinguishing strategies. Under substitution
$\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$, the
process on the left has transition
$\left(\mathopen{\left[x=y\right]}\tau\right)\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$,
which can be matched, under the same substitution, by
$\left(\tau.\mathopen{\left[x=y\right]}\tau\right)\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}\mathopen{\left[y=y\right]}\tau$.
Now $0$ and $\mathopen{\left[y=y\right]}\tau$ are distinguished, since
$\mathopen{\left[y=y\right]}\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\tau}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}0$
whereas $0$ is deadlocked. By applying the algorithm in Proposition 4.9, we
obtain the formula
$x=y\supset\mathopen{\big{[}\tau\big{]}}\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}$
biased to the process on the right, which is indeed distinguishing.

As a further example of alternative distinguishing formulae, consider the
following processes.

$\mathopen{\big{[}x=y\big{]}}\tau.\tau+\tau\qquad\not\sim\qquad\tau.\tau+\tau$

The following is a distinguishing formula biased to the left process:
$\mathopen{\big{[}\tau\big{]}}\mathopen{\big{[}\tau\big{]}}(x=y)$. However,
this is different from the left-biased formula
$\mathopen{\mathopen{\big{[}\tau\big{]}}}\left(\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\vee(x=y)\right)$
generated by the algorithm. Thus, there exist alternative distinguishing
formulae …and alternative algorithms.

####  4.4.4. A more elaborate example

Consider the following processes.

$P\triangleq\tau+\mathopen{\tau.}\left(\tau.\tau+\tau\right)+\mathopen{\tau.\mathopen{\left[x=y\right]}}\left(\tau.\mathopen{\left[u=v\right]}\tau+\tau.\tau+\tau\right)\qquad
Q\triangleq
P+\mathopen{\tau.\mathopen{\left[x=y\right]}}\left(\tau.\tau+\tau\right)$

The processes above are distinguished by the following strategy. Firstly, the
process $Q$ moves, as follows; for which there are three moves $P$ can
perform.

$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau}$$\scriptstyle{\tau}$$\scriptstyle{\tau}$$\textstyle{\mathopen{\left[x=y\right]}\left(\tau.\tau+\tau\right)}$$\textstyle{0}$$\textstyle{\tau.\tau+\tau}$$\textstyle{\mathopen{\left[x=y\right]}\left(\tau.\mathopen{\left[u=v\right]}\tau+\tau.\tau+\tau\right)}$

This leads to three sub-problems, for which we know already the distinguishing
strategies and formulae. Note, to distinguish
$\mathopen{\left[x=y\right]}\left(\tau.\tau+\tau\right)$ from
$\mathopen{\left[x=y\right]}\left(\tau.\mathopen{\left[u=v\right]}\tau+\tau.\tau+\tau\right)$,
there is a switch in the process that leads.

From the above strategy, we can construct the following distinguishing
formulae.

$Q\models\mathopen{\big{\langle}\tau\big{\rangle}}\left(\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\wedge\mathopen{\big{[}\tau\big{]}}\left(x=y\right)\wedge\mathopen{\big{[}\tau\big{]}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\right)$
$P\models\mathopen{\big{[}\tau\big{]}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\vee\left(x=y\supset\mathopen{\big{\langle}\tau\big{\rangle}}\left(\left(u=v\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\right)\wedge\mathopen{\big{[}\tau\big{]}}\left(u=v\right)\right)\right)\right)$

Notice this example nests a classic example, explained previously, inside
itself. The absence of the law of excluded middle is essential for the
existence of distinguishing formulae in this example.

##  5\. Mechanised Proofs in Abella

Abella [BCG+14] is a proof assistant based on intuitionistic logic that
supports both inductive and coinductive reasoning over logical specifications
of operational semantics for languages that contain binding structures, such
as the $\pi$-calculus. In particular, Abella is well-suited for reasoning
involving operational semantics specified in the higher-order logic
programming $\lambda$Prolog [MN12]. The formalisation of the modal logic
$\mathcal{O\\!M}$ in this section is built on top existing work on the
formalisation of the pi-calculus and bisimulation based on the higher-order
abstract syntax (HOAS) approach [BGM+07, TM10, BCG+14]. We give an overview of
the $\lambda$Prolog specification of the $\pi$-calculus labelled transition
semantics (Section 5.1) and the coinductive definition of open bisimilarity in
Abella (Section 5.2); for more details, the reader is referred to the
literature, in particular [TM10, BCG+14]. We present the formalisation of the
semantics of the modal logic $\mathcal{O\\!M}$ and explain our mechanised
proof of the soundness theorem (Theorem 3.2) in Section 5.3.

⬇

sig finite-pic. % file: finite-pic.sig

kind n type. % names

kind p type. % processes

type null p. % deadlock

type taup p $\boldsymbol{\to}$ p. % progress action

type plus, par p $\boldsymbol{\to}$ p $\boldsymbol{\to}$ p. % choice, par

type match, out n $\boldsymbol{\to}$ n $\boldsymbol{\to}$ p $\boldsymbol{\to}$
p. % match, output action

type in n $\boldsymbol{\to}$ (n $\boldsymbol{\to}$ p) $\boldsymbol{\to}$ p. %
input action

type nu (n $\boldsymbol{\to}$ p) $\boldsymbol{\to}$ p. % nu

kind a type. % actions (transition labels)

type tau a.

type up, dn n $\boldsymbol{\to}$ n $\boldsymbol{\to}$ a.

type one p $\boldsymbol{\to}$ a $\boldsymbol{\to}$ p $\boldsymbol{\to}$ o. %
one step free transition

type oneb p $\boldsymbol{\to}$ (n $\boldsymbol{\to}$ a) $\boldsymbol{\to}$ (n
$\boldsymbol{\to}$ p) $\boldsymbol{\to}$ o. % one step bound transition

module finite-pic. % file: finite-pic.mod

oneb (in X M) (dn X) M. % bound input

one (out X Y P) (up X Y) P. % free output

one (taup P) tau P. % tau

% match prefix

one (match X X P) A Q $\coloneq$ one P A Q. oneb (match X X P) A M $\coloneq$
oneb P A M.

% sum

one (plus P Q) A R $\coloneq$ one P A R. oneb (plus P Q) A M $\coloneq$ oneb P
A M.

one (plus P Q) A R $\coloneq$ one Q A R. oneb (plus P Q) A M $\coloneq$ oneb Q
A M.

% par

one (par P Q) A (par $\text{P}_{\\!1\\!}$ Q) $\coloneq$ one P A
$\text{P}_{\\!1\\!}$. oneb (par P Q) A (z\par (M z) Q) $\coloneq$ oneb P A M.

one (par P Q) A (par P $\text{Q}_{\\!1\\!}$) $\coloneq$ one Q A
$\text{Q}_{\\!1\\!}$. oneb (par P Q) A (z\par P (N z)) $\coloneq$ oneb Q A N.

% restriction

one (nu z\P z) A (nu z\Q z) $\coloneq$ pi z\ one (P z) A (Q z).

oneb (nu z\P z) A (y\nu z\Q z y) $\coloneq$ pi z\ oneb (P z) A (y\Q x z).

% open (bound output)

oneb (nu x\P x) (up X) Q $\coloneq$ pi z\ one (P y) (up X y) (Q y).

% close

one (par P Q) tau (nu z\par (M z) (N z)) $\coloneq$ oneb P (dn X) M, oneb Q
(up X) N.

one (par P Q) tau (nu z\par (M z) (N z)) $\coloneq$ oneb P (up X) M, oneb Q
(dn X) N.

% comm (interaction)

one (par P Q) tau (par (M Y) T) $\coloneq$ oneb P (dn X) M, one Q (up X Y) T.

one (par P Q) tau (par R (M Y)) $\coloneq$ oneb Q (dn X) M, one P (up X Y) R.

Figure 3. $\lambda$Prolog specification of the syntax and semantics of the
$\pi$-calculus. (Adopted from one of the examples distributed with Abella.)

###  5.1. Specification of the syntax and labelled transition semantics of the
$\pi$-calculus in $\lambda$Prolog

Recall the syntax and labelled transition semantics in Fig. 1 from Section 2.
Fig. 3 is a transcription of the syntactic constructs and transition rules in
$\lambda$Prolog. Each syntactic category is declared as a type (e.g., n, p,
and a) using the kind keyword. Syntactic constructs are defined as constants
in $\lambda$Prolog where some of which may require multiple arguments to
construct the desired syntactic category. For instance, plus needs two process
arguments to construct a process as its type (p$\boldsymbol{\to}$
p$\boldsymbol{\to}$ p) suggests. The table below summarises the process syntax
in $\lambda$Prolog and the notations used in the previous sections.

$\lambda$Prolog syntax | mathematical notation |
---|---|---
null |  $0$ |
nu x\P x (or nu P) |  $\nu z.P$ |  (P z) corresponds to $P$
taup P |  $\tau.P$ |
out x z P |  $\overline{x}{z}.P$ |
in x z\P z (or in x P) |  $x(z).P$ |  (P z) corresponds to $P$
match x y P |  $[x=y]P$ |
par P Q |  $P\mathrel{\|}Q$ |
plus P Q |  $P+Q$ |

Fig. 3 has few stylistic differences from Fig. 1. Firstly, distinct constants
are used for actions and its related processes (e.g., tau action for taup
prefixed process) because the constants cannot be overloaded as in
mathematical notations. Secondly, the action prefix $\pi.P$ in Fig. 1, where
$\pi$ ranges over several different types of action (progress, free out, and
input), is transcribed as three distinct process syntactic constructs (taup,
out, and in). Thirdly, free and bound actions are distinguished by their types
instead of using different notations ($\overline{x}{z}$ and
$\mathopen{\overline{x}}\left(z\right)$) as in Fig. 1. That is, bound actions
(e.g., up x : n$\boldsymbol{\to}$a) are partially applied free actions (e.g.,
up x z : a) using the same constants. Fourthly, two different set of
transition relations are defined: one relating a process (p) with another
process (p) via a free action (a) and oneb relating a process (p) with a bound
process (n$\boldsymbol{\to}$p) via a bound action (n$\boldsymbol{\to}$a).

One advantage of using $\lambda$Prolog [MN12] is that we can rely on its
native support for a variant of HOAS, known as _$\lambda$ -tree syntax_
[MP99], for handling bound names and $\alpha\beta\eta$-equivalence
automatically. For instance, consider the bound output transition rule for
name restricted process from both Fig. 3 and Fig. 1:

${\begin{array}[]{ll}{\small\texttt{ oneb (nu z\textbackslash P z) (up X) Q}}~{}\text{~{}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color<EMAIL_ADDRESS>\qquad{\small\texttt{pi z\textbackslash one (P z) (up X z) (Q z)}}\\\ {}\end{array}$ |  $\nu z.P\mathrel{\raise 1.6pt\hbox{$\mathop{\rule{17.34111pt}{0.62pt}}\limits^{{\mathopen{\overline{x}}\left(z\right)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}QP\mathrel{\raise 1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\overline{x}z}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q$
---|---

There is no need to explicitly state and keep track of the side conditions
such as $x\neq z$ and $x\notin\mathop{\mathrm{n}}(\pi)$ in $\lambda$Prolog
definitions. For example, consider pi z\one (P z) (up X z) (Q z) from above.
Here, it is guaranteed that z does not to occur free in the logic variables P,
X, and Q. This guarantee comes from the scoping of variables: the scopes of P,
X, and Q go beyond the scope of z, which is limited only to one (P z) (up X z)
(Q z). Had z freely occurred in any of P, X, or Q, the scope of z would have
been violated. Hence, X cannot be unified with z.

⬇

1Specification "finite-pic". % load the finite pi-calc. spec. in Fig. 3

2

3CoDefine bisim : p $\boldsymbol{\to}$ p $\boldsymbol{\to}$ prop % open
bisimulation

4by bisim P Q

5 $\coloneqq$ ($\forall$ A $\text{P}_{\\!1\\!}$, {one P A
$\text{P}_{\\!1\\!}$} $\boldsymbol{\to}$ $\exists$ $\text{Q}_{\\!1\\!}$, {one
Q A $\text{Q}_{\\!1\\!}$} /\ bisim $\text{P}_{\\!1\\!}$ $\text{Q}_{\\!1\\!}$)

6 /\ ($\forall$ X M, {oneb P (dn X) M} $\boldsymbol{\to}$ $\exists$ N, {oneb Q
(dn X) N} /\ $\forall$ z, bisim (M z) (N z))

7 /\ ($\forall$ X M, {oneb P (up X) M} $\boldsymbol{\to}$ $\exists$ N, {oneb Q
(up X) N} /\ $\nabla$ z, bisim (M z) (N z))

8 /\ ($\forall$ A $\text{Q}_{\\!1\\!}$, {one Q A $\text{Q}_{\\!1\\!}$}
$\boldsymbol{\to}$ $\exists$ $\text{P}_{\\!1\\!}$, {one P A
$\text{P}_{\\!1\\!}$} /\ bisim $\text{Q}_{\\!1\\!}$ $\text{P}_{\\!1\\!}$)

9 /\ ($\forall$ X N, {oneb Q (dn X) N} $\boldsymbol{\to}$ $\exists$ M, {oneb P
(dn X) M} /\ $\forall$ z, bisim (N z) (M z))

10 /\ ($\forall$ X N, {oneb Q (up X) N} $\boldsymbol{\to}$ $\exists$ M, {oneb
P (up X) M} /\ $\nabla$ z, bisim (N z) (M z)).

11

12Kind o′ type. % syntax of the modal logic

13Type tt, ff o′.

14Type $\boldsymbol{\curlyvee}$, $\boldsymbol{\curlywedge}$,
$\boldsymbol{\supset}$ o′ $\boldsymbol{\to}$ o′ $\boldsymbol{\to}$ o′.

15Type $\eqcirc$ n $\boldsymbol{\to}$ n $\boldsymbol{\to}$ o′.

16Type $\Box$, $\Diamond$ a $\boldsymbol{\to}$ o′ $\boldsymbol{\to}$ o′.

17Type $\Box^{\uparrow\\!}$, $\Diamond^{\uparrow}\\!\\!$,
$\Box^{\downarrow\\!}$, $\Diamond^{\downarrow}$ n $\boldsymbol{\to}$ (n
$\boldsymbol{\to}$ o′) $\boldsymbol{\to}$ o′.

18

19Define sat : p $\boldsymbol{\to}$ o′ $\boldsymbol{\to}$ prop % semantics of
the modal logic

20by sat P tt

21 ; sat P ($\boldsymbol{\curlyvee}$ A B) $\coloneqq$ sat P A /\ sat P B

22 ; sat P ($\boldsymbol{\curlywedge}$ A B) $\coloneqq$ sat P A \/ sat P B

23 ; sat P ($\boldsymbol{\supset}$ A B) $\coloneqq$ sat P A $\boldsymbol{\to}$
sat P B

24 ; sat P ($\eqcirc$ X Y) $\coloneqq$ X = Y

25 ; sat P ($\Box$ X A) $\coloneqq$ $\forall$ $\text{P}_{\\!1\\!}$, {one P X
$\text{P}_{\\!1\\!}$} $\boldsymbol{\to}$ sat $\text{P}_{\\!1\\!}$ A

26 ; sat P ($\Diamond$ X A) $\coloneqq$ $\exists$ $\text{P}_{\\!1\\!}$, {one P
X $\text{P}_{\\!1\\!}$} /\ sat $\text{P}_{\\!1\\!}$ A

27 ; sat P ($\Box^{\uparrow\\!}$ X A) $\coloneqq$ $\forall$ Q, {oneb P (up
X) Q} $\boldsymbol{\to}$ $\nabla$ z, sat (Q z) (A z)

28 ; sat P ($\Diamond^{\uparrow}\\!\\!$ X A) $\coloneqq$ $\exists$ Q, {oneb P
(up X) Q} /\ $\nabla$ z, sat (Q z) (A z)

29 % basic input modality (see Section 6.1 for related discussion)

30 ; sat P ($\Box^{\downarrow\\!}$ X A) $\coloneqq$ $\forall$ Q, {oneb P (dn
X) Q} $\boldsymbol{\to}$ $\forall$ z, sat (Q z) (A z)

31 % late input modality (see Section 6.1 for related discussion)

32 ; sat P ($\Diamond^{\downarrow}$ X A) $\coloneqq$ $\exists$ Q, {oneb P
(dn X) Q} /\ $\forall$ z, sat (Q z) (A z).

Figure 4. A coinductive definition of open bisimulation and an inductive
definition of the modal logic $\mathcal{O\\!M}$ in Abella.

###  5.2. Coinductive definition of open bisimulation in Abella’s reasoning
logic

Open bisimulation relation bisim is coinductively defined in Fig. 4. The
relation bisim is an Abella encoding of the open bisimulation relation
$\mathcal{R}$ in Definition 3.1 from Section 3. Lines 5, 6, and 7 correspond
to the latter three of the four bullet items in Definition 3.1, which state
the closure property under every pairwise bisimulation step where P leads and
Q follows. Lines 8, 9, and 10 are symmetric cases where Q leads and P follows.
Curly braces (e.g., {one P A $\text{P}_{\\!1\\!}$}) are used for referring to
the object logic proposition (i.e., $\lambda$Prolog proposition) from the
reasoning logic of Abella. Recall the type of the $\lambda$Prolog relation one
: p$\boldsymbol{\to}$a$\boldsymbol{\to}$p$\boldsymbol{\to}$o in Fig. 3. When
applied to three arguments, it becomes an object logic proposition one P A
$\text{P}_{\\!1\\!}$ : o. When we need to to refer to the $\lambda$Prolog
proposition from Abella’s reasoning logic, we must convert form the
$\lambda$Prolog proposition type (o) to the reasoning logic proposition type
(prop) using curly braces. For example, {one P A $\text{P}_{\\!1\\!}$} : prop.
Abella’s reasoning logic is richer than the object logic. It supports
coinductive definitions, which we used to define bisim. It also supports a
nominal quantifier ($\nabla$), which will be discussed shortly, in addition to
universal ($\forall$) and existential ($\exists$) quantifications.

The first bullet item in Definition 3.1 states that open bisimulation must be
closed under all substitutions that respect the history. In the definition
bisim, Abella guarantees this closure property under respectful substitutions
for free. Let us first demonstrate how histories are being handled in the
relation bisim, in order to lead the explanation on how the closure property
under respectful substitutions is ensured in Abella. Consider a trivial
bisimulation over identical processes, illustrated using both Abella and
mathematical notations as below:

${{{{{{{{{\text{\scriptsize\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\forall$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{x}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}}}}~{}
{bisim (nu z\textbackslash out x z (in x y\textbackslash null)) (nu
z\textbackslash out x z (in x y\textbackslash
null))}}^{\phantom{G^{G}}}\lx@proof@logical@and\quad\text{\scriptsize\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\forall$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{x}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\nabla$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{z}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}}}}~{}{bisim
(in x y\textbackslash null) (in x y\textbackslash
null)}}_{\phantom{G}}^{\phantom{G^{G}}}\lx@proof@logical@and\text{\scriptsize\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\forall$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{x}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\nabla$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{z}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}\@listingLiterate{{{\color[rgb]{0.3,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0,0}\pgfsys@color@cmyk@stroke{0}{0.83}{1}{0.70}\pgfsys@color@cmyk@fill{0}{0.83}{1}{0.70}$\forall$}}}}}}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{y}}\@listingLiterate{{{\color[rgb]{0,0.6,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.6,0}\pgfsys@color@cmyk@stroke{0.64}{0}{0.95}{0.40}\pgfsys@color@cmyk@fill{0.64}{0}{0.95}{0.40},}}}}}}~{}{bisim
null
null}}\qquad~{}\vdots\quad\qquad\qquad\vdots\qquad\quad_{\phantom{G_{G}}}\quad\nu
z.\overline{x}{z}.x(y).0~{}\sim^{\,x^{i}}~{}\nu
z.\overline{x}{z}.x(y).0\lx@proof@logical@and x(y).0~{}\sim^{\,x^{i}\cdot
z^{o}}~{}x(y).0\lx@proof@logical@and 0~{}\sim^{\,x^{i}\cdot z^{o}\cdot
y^{i}}~{}0~{}~{}\vdots~{}\quad\vdots~{}~{}$

Even for identical processes without nondeterministic constructs, the
bisimulation tree has at least two branches for each node because either one
of the two sides may take a leading step to be followed by the other side.
Here, let us focus on the leftmost branches where the left process leads. The
environment of quantified variables for the Abella relation bisim grows after
each bisimulation step. Growing the environment exactly corresponds to growing
the history. The bound output step extends the environment with $\nabla$z in
Abella, which corresponds to extending the history with $z^{o}$. The input
step extends the environment with $\forall$y in Abella, which corresponds to
extending the history with $y^{i}$. These quantified variables come from the
definition of bisim in Fig. 4, more specifically, from lines 6 and 7.

Recall the definition of respectful substitution (Definition 2.1) from Section
2. An input variable in the history adds no restriction to the respectfulness
of a substitution. An output variable in the history adds a restriction such
that respectful substitutions should not unify the output variable with any
variable that precedes the output variable. The nabla quantifier ($\nabla$) in
Abella coincides with such a notion of restriction. Nabla quantified variables
are guaranteed to be fresh with respect to all the previously introduced
variables. For instance, consider the environment
$\forall$x,$\nabla$z,$\forall$y,$\cdots$. Abella ensures that z cannot occur
free in x, hence, x cannot be unified with z; however, y can be unified with z
because y is introduced after z.

Intuitively, universal quantification represents all possible substitutions
over universally quantified variables. For example, consider $\forall$ x, pred
x. Proving this in Abella means that the predicate pred holds for all possible
substitutions over x. Together with nabla quantification, the notion of all
possible respectful substitutions can be represented by the environment of
quantified variables in Abella. In summary, the list of universal and nabla
quantified names before the bisim relation in Abella not only transcribes the
history but also represents all possible respectful substitutions.

###  5.3. Embedding of $\mathcal{O\\!M}$ in Abella and the soundness proof

The latter part of Fig. 4 is an embedding of $\mathcal{O\\!M}$ syntax and
semantics introduced earlier in Section 2.1. Recall the stylistic difference
between Abella and mathematical notations for the process syntax – prefixes of
free actions, bound output actions, and input actions are defined as three
different syntactic constructs in the Abella definitions (see Fig. 4). There
are similar stylistic difference regarding $\mathcal{O\\!M}$ formulae in the
Abella embedding (Fig. 4) and notation from Section 2.1. There are three
formulae constructs for each kind of modality. For instance, $\Box$,
$\Box^{\uparrow\\!}$, and $\Box^{\downarrow\\!}$ are the three different
syntactic constructs of the box modality for free actions, bound output
actions, and input actions, respectively. Similarly, there are three
constructs for the diamond modality.222In the Abella proof scripts, $\Box$,
$\Box^{\uparrow\\!}$, and $\Box^{\downarrow\\!}$ are represented using
keywords boxAct, boxOut and boxIn, respectively.

Recall that histories on the bisimulation relation are transcribed as
universal and nabla quantified variables in Abella and that closure under
respectful substitutions holds for free in Abella. Similarly, histories on
$\mathcal{O\\!M}$ semantics are handled exactly the same manner in Abella and
enjoy the closure properties regarding respectful substitutions. For example,
$\forall$x,$\nabla$z,$\forall$y, sat (P x y z) $\phi$ corresponds to
$\forall\sigma\mathrel{\textrm{respecting}}x^{i}\cdot z^{o}\cdot
y^{i},~{}P(x,y,z)\models^{x^{i}\cdot z^{o}\cdot y^{i}}\phi$. The relation sat
in Fig. 4 is an embedding of $\mathcal{O\\!M}$ semantics ($\models$) in
Abella. There is no explicit handing of substitutions in the sat relation
definition because they are handled by Abella automatically.

We mechanised the proof of soundness of open bisimilarity with respect to
$\mathcal{O\\!M}$ by proving the following theorem,

⬇

Theorem bisim_sat : $\forall$ P Q F, form F $\boldsymbol{\to}$

bisim P Q $\boldsymbol{\to}$ ((sat P F $\boldsymbol{\to}$ sat Q F) /\ (sat Q F
$\boldsymbol{\to}$ sat P F)).

where form: o′$\boldsymbol{\to}$prop is an inductive predicate for well-formed
$\mathcal{O\\!M}$ formulae, defined as follows:

⬇

Define form : o′ $\boldsymbol{\to}$ prop

by form tt

; form ff

; form ($\boldsymbol{\curlyvee}$ A B) $\coloneqq$ form A /\ form B

; form ($\boldsymbol{\curlywedge}$ A B) $\coloneqq$ form A /\ form B

; form ($\boldsymbol{\supset}$ A B) $\coloneqq$ form A /\ form B

; form ($\eqcirc$ X Y) $\coloneqq$ form A

; form ($\Box$ X A) $\coloneqq$ form A

; form ($\Diamond$ X A) $\coloneqq$ form A

; form ($\Box^{\uparrow\\!}$ X A) $\coloneqq$ $\forall$ w, form (A w)

; form ($\Diamond^{\uparrow}\\!\\!$ X A) $\coloneqq$ $\forall$ w, form (A w)

; form ($\Box^{\downarrow\\!}$ X A) $\coloneqq$ $\forall$ w, form (A w)

; form ($\Diamond^{\downarrow}$ X A) $\coloneqq$ $\forall$ w, form (A w).

The proof proceeds by induction on the structure of the modal formulae and
case analyses on the definition of the satisfiability relation sat. The
soundness theorem is a simple corollary of bisim_sat:

⬇

Theorem soundness: $\forall$ P Q,

bisim P Q $\boldsymbol{\to}$ $\forall$ F, form F $\boldsymbol{\to}$ (sat P F
$\boldsymbol{\to}$ sat Q F) /\ (sat Q F $\boldsymbol{\to}$ sat P F).

##  6\. Situating $\mathcal{OM}$ with Respect to Other Modal Logics
Characterising Bisimilarities

Open bisimilarity is not the only bisimilarity congruence. We consider here
the relationship between the intuitionistic modal logic for open bisimilarity
presented in this work and other modal logics. In doing so, we clarify why we
introduce $\mathcal{O\\!M}$ rather than taking an intuitionistic variant of an
established modal logic. We check that $\mathcal{O\\!M}$ has a classical
counterpart characterising late bisimilarity. Also, we note open bisimilarity
is not the only notion of bisimilarity that is a congruence relation. We
provide a sharp picture explaining where open bisimilarity sits in relation to
other notions of bisimilarity.

###  6.1. Why a new modal logic $\mathcal{O\\!M}$, rather than an
intuitionistic variant of $\mathcal{L\\!M}$?

A classical logic characterising late bisimilarity, called $\mathcal{L\\!M}$
for “($\mathcal{L}$) late modality with ($\mathcal{M}$) match,” was provided
by Milner, Parrow, and Walker [MPW93]. $\mathcal{L\\!M}$ differs from
$\mathcal{O\\!M}$ in two significant ways. Firstly, $\mathcal{L\\!M}$ is
classical, that is, the law of excluded middle for name equalities is induced
by eagerly applying substitutions and assuming all names are distinct.
Secondly, the late input box modality is defined differently, involving an
existential quantification over substitutions. Moving to the intuitionistic
setting, this gives rise to the following variant of the box input modality.

> $P\models\mathopen{\big{[}a(x)\big{]}}^{L}\phi$ iff
> $\forall\sigma\mathrel{\textrm{respecting}}h,\forall
> Q,P\sigma\mathrel{\raise
> 1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q==>\exists
> x,\mbox{such that }Q\models^{h\sigma}\phi$.

In the semantics of $\mathcal{O\\!M}$, we deliberately use a universally
quantified box input modality, recalled bellow; rather than existentially
quantified box input modality used in $\mathcal{L\\!M}$ above.

> $P\models\mathopen{\big{[}a(x)\big{]}}\phi$ iff
> $\forall\sigma\mathrel{\textrm{respecting}}h,\forall
> Q,P\sigma\mathrel{\raise
> 1.6pt\hbox{$\mathop{\rule{20.47859pt}{0.62pt}}\limits^{{a\sigma(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q==>Q\models^{h\sigma\cdot
> x^{i}}\phi$.

Recall from Sec. 5, in the box input modality of $\mathcal{O\\!M}$ immediately
above, the $x^{i}$ appended to the history has the effect of $\forall x$
appearing immediately after the implication (made explicit in Fig. 4).

Hence, due to the differences in quantification for the box input modality,
$\mathcal{O\\!M}$ is not quite an intuitionistic variant of $\mathcal{L\\!M}$.
The carefully selected box input modality in $\mathcal{O\\!M}$ is necessary
for our construction of distinguishing formulae in the completeness proof for
the characterisation of open bisimilarity using $\mathcal{O\\!M}$. To
understand why, consider the following non-bisimilar processes.

$a(x).\tau+a(x)+a(x).[x=a]\tau\quad\not\sim\quad a(x).\tau+a(x)$

For the above processes, our algorithm for distinguishing formulae,
Proposition 4.9, correctly generates the following $\mathcal{O\\!M}$ formula
biased to the right:

$a(x).\tau+a(x)+a(x).[x=a]\tau\not\models\mathopen{\big{[}a(x)\big{]}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\quad\mbox{and}\quad
a(x).\tau+a(x)\models\mathopen{\big{[}a(x)\big{]}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)$

If we were to use an intuitionistic variant of the input box modality of
$\mathcal{L\\!M}$, as suggested in related work [TM10], both processes satisfy
the above formulae modified with a late box input modality
$\mathopen{\mathopen{\big{[}a(x)\big{]}}^{L}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)$.
To see why
$a(x).\tau+a(x)+a(x).[x=a]\tau\models\mathopen{\mathopen{\big{[}a(x)\big{]}}^{L}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)$
holds, observe for the transition
$a(x).\tau+a(x)+a(x).[x=a]\tau\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.4787pt}{0.62pt}}\limits^{{a(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}[x=a]\tau$
there exists
$\mathclose{\\{^{a\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$ such
that
$\left([x=a]\tau\right)\mathclose{\\{^{a\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}\models\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}$.

Also, note the formula
$\mathopen{\mathopen{\big{[}a(x)\big{]}}^{L}}\left(\left(x=a\wedge\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\vee\mathopen{\big{\langle}\tau\big{\rangle}}\mathopen{\neg}\left(x=a\right)\right)$
fails in intuitionistic $\mathcal{L\\!M}$ for both processes, despite being
distinguishing for these processes in classical $\mathcal{L\\!M}$. Although,
if we use triple negation the formula becomes distinguishing in intuitionistic
$\mathcal{L\\!M}$, as follows:

$a(x).\tau+a(x)\models\mathopen{\mathopen{\big{[}a(x)\big{]}}^{L}}\left(\left(x=a\wedge\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\vee\mathopen{\big{\langle}\tau\big{\rangle}}\mathopen{\neg\neg\neg}\left(x=a\right)\right)$
(1)

####  6.1.1. Example where box input is necessary.

Notice, for the above example processes, formula
$\mathopen{\big{\langle}a(x)\big{\rangle}}\left(x=a\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\wedge\mathopen{\big{[}\tau\big{]}}\left(x=a\right)\right)$
is a distinguishing formula biased to the left, in both intuitionistic
$\mathcal{L\\!M}$ and $\mathcal{O\\!M}$, since the diamond input modalities
are the same in both intuitionistic modal logics. For a more sophisticated
example where box input modalities are necessary, regardless of the bias,
consider the follow processes that are not open bisimilar.

$P\triangleq
a(x)+\mathopen{a(x).}\left(a(y)+a(y).\tau\right)+a(x).\mathopen{\left[x=v\right]}\left(a(y)+a(y).\tau+a(y).\mathopen{\left[y=w\right]}\tau\right)$
$Q\triangleq P+a(x).\mathopen{\left[x=v\right]}\left(a(y)+a(y).\tau\right)$

Consider the distinguishing strategy. The first move must be made by $Q$,
which can be matched by $P$ in three ways.

$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a(x)}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a(x)}$$\scriptstyle{a(x)}$$\scriptstyle{a(x)}$$\textstyle{\mathopen{\left[x=v\right]}\left(a(y)+a(y).\tau\right)}$$\textstyle{0}$$\textstyle{a(y)+a(y).\tau}$$\textstyle{\mathopen{\left[x=v\right]}\left(a(y)+a(y).\tau+a(y).\mathopen{\left[y=w\right]}\tau\right)}$

Each of the processes reachable by a $a(x)$-transition from $P$ are not open
bisimilar to the process reachable from $Q$ indicated above. The interesting
case is the third process reached from $P$ above. After applying substitution
$\mathclose{\\{^{v\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!x}\\}}$, the
process on the right leads the distinguishing strategy.

$\textstyle{\mathopen{\left[v=v\right]}\left(a(y)+a(y).\tau\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a(y)}$$\scriptstyle{a(y)}$$\textstyle{\mathopen{\left[v=v\right]}\left(a(y)+a(y).\tau+a(y).\mathopen{\left[y=w\right]}\tau\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a(y)}$$\textstyle{0}$$\textstyle{\tau}$$\textstyle{\mathopen{\left[y=w\right]}\tau}$

The necessity of box input modalities is due to the switch from $Q$ leading
initially to the other process leading for the second input in the
distinguishing strategy. From the above distinguishing strategy the following
formula biased to $P$ can be constructed.

$P\models\mathopen{\big{[}a(x)\big{]}}\left(\mathopen{\big{[}a(y)\big{]}}\mathtt{ff}\vee\mathopen{\big{\langle}a(y)\big{\rangle}}\mathtt{tt}\vee\left(x=v\supset\mathopen{\big{\langle}a(y)\big{\rangle}}\left(y=w\supset\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\wedge\mathopen{\big{[}\tau\big{]}}\left(y=w\right)\right)\right)\right)$

For a formula biased to $Q$ we obtain the following.

$Q\models\mathopen{\big{\langle}a(x)\big{\rangle}}\left(x=v\supset\mathopen{\big{\langle}a(y)\big{\rangle}}\mathtt{tt}\wedge\mathopen{\big{[}a(y)\big{]}}\left(x=v\right)\wedge\mathopen{\big{[}a(y)\big{]}}\left(\mathopen{\big{\langle}\tau\big{\rangle}}\mathtt{tt}\vee\mathopen{\big{[}\tau\big{]}}\mathtt{ff}\right)\right)$

Neither of the above formulae would be distinguishing if, instead of the open
box modalities of $\mathcal{O\\!M}$, the late box modalities of
$\mathcal{L\\!M}$ were employed.

####  6.1.2. Discussion on intuitionistic $\mathcal{L\\!M}$.

We have formalised the intuitionistic variant of $\mathcal{L\\!M}$ in Abella.
The language of formulae for $\mathcal{L\\!M}$ replaces the “basic” box input
modality of $\mathcal{O\\!M}$ with the following “late” box input modality:

⬇

Type $\Box_{L}^{\downarrow\\!}$ n $\boldsymbol{\to}$ (n $\boldsymbol{\to}$
o′) $\boldsymbol{\to}$ o′.

The clauses for the satisfaction relation (encoded as the predicate satLM) are
those for $\mathcal{O\\!M}$ (Figure 4) without the “basic” box operator, but
with the following clause for satLM :

⬇

satLM P ($\Box_{L}^{\downarrow\\!}$ X A) $\coloneqq$ $\forall$ Q, {oneb P
(dn X) Q} $\boldsymbol{\to}$ $\exists$ z, sat (Q z) (A z).

The example involving triple negation above (1) has been verified using this
formalisation of intuitionistic $\mathcal{L\\!M}.$

Related work [TM10] suggested that intuitionistic $\mathcal{L\\!M}$
characterises open bisimilarity. Unfortunately, the completeness proof in that
work is flawed since they appeal to classical principals that are not valid in
the intuitionistic setting. This oversight is rectified in the current paper,
by a more direct construction in the completeness proof and by the careful
choice of input modalities in $\mathcal{OM}$, explained in this section. Note
however the example above involving triple negation, suggests the problem of
whether intuitionistic $\mathcal{L\\!M}$ characterises open bisimilarity
remains an open problem. To offer an intuition for triple negation: it can be
regarded as an explicit test that variables are “not equal yet,” in contrast
to single negation indicating that variables are never going to be equal.

###  6.2. What about the classical counterpart to $\mathcal{O\\!M}$?

A criteria an intuitionistic modal logic is expected to satisfy is that, when
the law of excluded middle is induced, we obtain a meaningful classical logic.
Fortunately, this criteria holds for $\mathcal{O\\!M}$ — the classical
counterpart to $\mathcal{O\\!M}$ characterises late bisimilarity. For
convenience we, recall the definition of late bisimilarity.

######  Definition 6.1.

A late bisimulation $\mathcal{R}$ is a symmetric relation, such that, whenever
$P\mathrel{\mathcal{R}}Q$:

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
then there exists $Q^{\prime}$ such that $Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$.

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
then there exists $Q^{\prime}$ such that $Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{17.7786pt}{0.62pt}}\limits^{{\overline{a}(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$.

  * •

If $P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.4787pt}{0.62pt}}\limits^{{a(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}P^{\prime}$
then there exists $Q^{\prime}$ such that $Q\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.4787pt}{0.62pt}}\limits^{{a(x)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q^{\prime}$
and, for all $x$, $P^{\prime}\mathrel{\mathcal{R}}Q^{\prime}$.

Late bisimilarity $\mathrel{\dot{\sim}_{L}}$ is the greatest late
bisimulation.

$\begin{array}[]{c}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\\
\begin{array}[]{lcl}P\mathrel{\dot{\models}_{L}}\mathtt{tt}&\mbox{and}&\qquad
P\mathrel{\dot{\models}_{L}}x=x\qquad\mbox{always hold.}\\\
P\mathrel{\dot{\models}_{L}}\phi_{1}\supset\phi_{1}&\mbox{iff}&P\mathrel{\dot{\models}_{L}}\phi_{1}~{}==>~{}P\mathrel{\dot{\models}_{L}}\phi_{2}.\\\
P\mathrel{\dot{\models}_{L}}\mathopen{\big{\langle}\alpha\big{\rangle}}\phi&\mbox{iff}&\exists\,Q,~{}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{10.0pt}{0.62pt}}\limits^{{\alpha}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q~{}\mbox{and}~{}Q\mathrel{\dot{\models}_{L}}\phi.\\\
P\mathrel{\dot{\models}_{L}}\mathopen{\big{\langle}{a}(z)\big{\rangle}}\phi&\mbox{iff}&\exists\,Q,~{}P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.04121pt}{0.62pt}}\limits^{{{a}(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q~{}\mbox{and,}~{}\forall
y,\,Q\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!z}\\}}\mathrel{\dot{\models}_{L}}\phi\mathclose{\\{^{y\\!\\!\\!}\reflectbox{$\\!\smallsetminus$}_{\\!z}\\}}.\\\
P\mathrel{\dot{\models}_{L}}\mathopen{\big{[}{a}(z)\big{]}}\phi&\mbox{iff}&\forall
Q,P\mathrel{\raise
1.6pt\hbox{$\mathop{\rule{16.04121pt}{0.62pt}}\limits^{{a(z)}\;}$}\mkern-6.0mu{\scriptstyle\blacktriangleright}}Q==>\forall
z,Q\mathrel{\dot{\models}_{L}}\phi.\end{array}\end{array}$ Figure 5. Semantics
of “classical $\mathcal{O\\!M}$”, where $\alpha$ is $\tau$, $\overline{a}b$ or
$\overline{a}(z)$.

A direct semantics of classical $\mathcal{O\\!M}$, in the style of Milner,
Parrow and Walker [MPW93], is presented in Fig. 5. Observe histories are not
employed in the classical semantics since inputs are instantiated eagerly,
immediately after performing an input transition. Also, missing operators
(conjunction, disjunction, and $\mathopen{\big{[}\alpha\big{]}}\phi$) are
derivable using classical negation; whereas in an intuitionistic modal logic
they have independent interpretations. Classical $\mathcal{O\\!M}$
characterises late bisimilarity.

######  Corollary 6.2 (characterisation).

$P\mathrel{\dot{\sim}_{L}}Q$ if and only if, for all $\mathcal{O\\!M}$
formulae $\phi$, we have $P\mathrel{\dot{\models}_{L}}\phi$ iff
$Q\mathrel{\dot{\models}_{L}}\phi$, according to the classical semantics for
$\mathcal{O\\!M}$ in Fig. 5.

###### Proof.

Observe that the definition of $\mathopen{\big{\langle}a(x)\big{\rangle}}\phi$
in Figure 5 coincides with the late modality
$\mathopen{\big{\langle}a(x)\big{\rangle}}^{L}\phi$ in $\mathcal{L\\!M}$. Also
observe that, classically, $\neg\mathopen{\big{[}a(x)\big{]}}\neg\phi$ is the
“basic” diamond modality of Milner, Parrow and Walker [MPW93]; hence classical
$\mathcal{OM}$ is classical $\mathcal{L\\!M}$ extended with “basic”
modalities. The original paper on modal logics for mobile processes
establishes that, classical $\mathcal{L\\!M}$ characterises late bisimilarity,
and also $\mathcal{L\\!M}$ extend with basic modalities has the same
expressive power at $\mathcal{L\\!M}$. ∎

Historically, Milner, Parrow and Walker emphasised late equivalence (the
greatest congruence contained in late bisimilarity) rather than late
bisimilarity in the original paper on the $\pi$-calculus[MPW92]. This is
because late equivalence is closed under input prefixes. Late equivalence has
a simpler characterisation in terms of closure under substitutions defined as
follows.

######  Definition 6.3.

$P$ is late equivalent to $Q$, written $P\mathrel{{\sim}_{L}}Q$, whenever
there exists a late bisimulation $\mathcal{R}$ such that for all $\sigma$,
$P\sigma\mathrel{\mathcal{R}}Q\sigma$. Define $P\mathrel{{\models}_{L}}\phi$
whenever for all $\sigma$, $P\sigma\mathrel{\dot{\models}_{L}}\phi\sigma$.

Quantifying over all substitutions, combined with the distinct name
assumption, means that we check late bisimilarity with respect to all
combinations of equalities and inequalities between free variables. As such,
late equivalence is not a bisimilarity; but is a late bisimulation. Using the
above, we obtain a characteristic logic for late equivalence, using
$\mathcal{O\\!M}$ formulae.

######  Corollary 6.4.

$P\mathrel{{\sim}_{L}}Q$ if and only if, for all $\phi$,
$P\mathrel{{\models}_{L}}\phi$ iff $Q\mathrel{{\models}_{L}}\phi$.

###### Proof.

This follows immediately from Corollary 6.2 and the following facts. For $a$