<p>Suppose <span class="math-container">$(S, \Lambda, \rightarrow)$</span> is a labeled transition system. A <em>bisimulation</em> is a relation <span class="math-container">$R \subseteq S \times S$</span> s.t. <span class="math-container">$\forall \alpha \in \Lambda$</span> and <span class="math-container">$\forall p, q \in S$</span> with <span class="math-container">$R(p,q)$</span>,</p>
<ul>
<li><span class="math-container">$\forall p'. p \xrightarrow{\alpha} p' \implies \exists q' . q \xrightarrow{\alpha} q' \land R(p',q');$</span></li>
<li><span class="math-container">$\forall q'. q \xrightarrow{\alpha} q' \implies \exists p' . p \xrightarrow{\alpha} p' \land R(p',q').$</span></li>
</ul>
<p>I noticed that for this definition of bisimulation, if <span class="math-container">$p$</span> can take an <span class="math-container">$\alpha$</span>-step, then so can <span class="math-container">$q$</span> and vice-versa. I.e., the transition-labels <span class="math-container">$\alpha \in \Lambda$</span> are are <em>syntactically</em> the same. But what if the transition system labels allow for value-passing? E.g., <span class="math-container">$\alpha(x) \triangleq \text{send}(x)$</span>, the action of sending a value <span class="math-container">$x$</span> to some location. Then clearly <span class="math-container">$\text{send}(x) \neq \text{send}(y)$</span> when <span class="math-container">$x \neq y$</span>, but we might want to consider two systems as doing the &quot;same action&quot; if <span class="math-container">$x$</span> and <span class="math-container">$y$</span> belong to some equivalence class (or even just some relation), even if they are not <em>syntactically</em> the same value.</p>
<p>So, modify the definition as so: Let <span class="math-container">$\approx \subseteq \Lambda \times \Lambda$</span> be some relation. Let <span class="math-container">$R\subseteq S \times S$</span> be a relation s.t. <span class="math-container">$\forall \alpha \in \Lambda$</span>, <span class="math-container">$\forall p,q\in S$</span> with <span class="math-container">$R(p,q)$</span>,</p>
<ul>
<li><span class="math-container">$\forall p'. p \xrightarrow{\alpha} p' \implies \exists \beta, q'. \alpha \approx \beta \land q \xrightarrow{\beta} q' \land R(p',q');$</span></li>
<li><span class="math-container">$\forall q'. q \xrightarrow{\alpha} q' \implies \exists \beta, p' . \alpha \approx \beta \land p \xrightarrow{\beta} p' \land R(p',q').$</span></li>
</ul>
<p>If we take <span class="math-container">$\approx$</span> to be syntactic equality <span class="math-container">$\equiv$</span>, we recover the original definition of bisimulation.</p>
<p>My question: Has this form of bisimulation been studied? What is it called? In particular, I'm interested in workable definitions of (bi)simulation in a system which allows value-passing, where we might want to allow some set of OK values, rather than restrict to syntactic equality of actions.</p>
<p>More generally, I am interested in alternative definitions of bisimulation which lead to notions of &quot;observational equivalence&quot;.</p>

CC BY-SA 4.0
2022-11-02T23:36:08.160Z
There has been a lot of work on different notions of process equivalence in the 1990s. Rob van Glabbeek's *The Linear Time - Branching Time Spectrum* Parts 1 and 2 are places to start looking. In the context of $\pi$-calculus you have *early* and *late* bisimulations, and b/c you can extrude scope, you will certainly want to equate $\alpha$-equivalent output-transitions. In higher-order process calculi, where you can pass processes (so they show up in labels) the question comes up as well.
Martin Berger
CC BY-SA 4.0
2022-11-03T07:09:49.000Z
Your notion of bisimulation is just the standard one where you consider the set of labels to be $\Lambda/\!\approx$ (the equivalence classes) rather than $\Lambda$.  So there's nothing you can do with your definition that you can't do with the usual one.  Or maybe you want to say something different?
Damiano Mazza
CC BY-SA 4.0
2022-11-03T23:23:05.020Z
@DamianoMazza One can repackage the standard definition of bisimulation into a coalgebraic definition (see [here](https://en.wikipedia.org/wiki/Bisimulation#Coalgebraic_definition)). This gives a nice characterization of bisimulation as a particular kind of commuting diagram. It is not obvious to me how things here change when considering equivalence classes instead of syntactic equality. This is one of the main examples I had in mind with this question.
NathanLiitt
CC BY-SA 4.0
2022-11-04T06:49:31.713Z
Suppose you have an lts $S$ with labels $\{a,b,c\}$.  You decide that $a$ and $b$ should be equivalent, so you take $S$, rename all transitions labelled by $a$ or $b$ to a new label $d$, and get an lts $S'$ on $\{c,d\}$.  The usual definition of bisimulation for $S'$ corresponds exactly to your modified bisimulation on $S$, in the sense that $p$ and $p'$ will be bisimilar in $S'$ iff they are bisimilar in $S$ in your sense.  Also, the coalgebraic reformulation you are interested in applies without changes to $S'$.  You just needed to relabel things.  What else are you looking for?
Damiano Mazza
CC BY-SA 4.0
2022-11-04T13:11:32.537Z
Since you mention "observational equivalence", there are also *weak* notions of process equivalences, where, simplifying a bit, strings $\sigma_1$ and $\sigma_2$ are considered equal if $\hat{\sigma}_1 = \hat{\sigma}_2$ where the function $\hat{\cdot}$ removes invisible actions.  If your model of computing is un-timed, you will need something like this for observational equivalency, since in such a setting, internal compute steps  cannot be observed.
Martin Berger
CC BY-SA 4.0
2022-11-04T13:16:24.897Z
A useful model for thinking about observational equivalence is that computational steps are given unlabelled: $P \rightarrow Q$. Observational equivalence is defined as closure under all possible context using $\rightarrow$. Now reasoning about process (in)equality wrt all possible context is annoying, so you use labelled transitions as convenience: a proof techniques for reasoning about process (in)equality where labels represent *minimal distinguishing contexts*: if you can say something about a process wrt minimal context, this then can (often) be used to say something about all contexts.
Martin Berger
<reference-request><automata-theory><pl.programming-languages><process-algebra><lts-simulations>
Alternative notions of bisimulation
NathanLiitt
# Alternative notions of bisimulation

(Asked by: username_0 on 2022-11-02)

Suppose $(S, \Lambda, \rightarrow)$ is a labeled transition system. A *bisimulation* is a relation $R \subseteq S \times S$ s.t. $\forall \alpha \in \Lambda$ and $\forall p, q \in S$ with $R(p,q)$,

* $\forall p'. p \xrightarrow{\alpha} p' \implies \exists q' . q \xrightarrow{\alpha} q' \land R(p',q');$
* $\forall q'. q \xrightarrow{\alpha} q' \implies \exists p' . p \xrightarrow{\alpha} p' \land R(p',q').$

I noticed that for this definition of bisimulation, if $p$ can take an $\alpha$-step, then so can $q$ and vice-versa. I.e., the transition-labels $\alpha \in \Lambda$ are are *syntactically* the same. But what if the transition system labels allow for value-passing? E.g., $\alpha(x) \triangleq \text{send}(x)$, the action of sending a value $x$ to some location. Then clearly $\text{send}(x) \neq \text{send}(y)$ when $x \neq y$, but we might want to consider two systems as doing the "same action" if $x$ and $y$ belong to some equivalence class (or even just some relation), even if they are not *syntactically* the same value.

So, modify the definition as so: Let $\approx \subseteq \Lambda \times \Lambda$ be some relation. Let $R\subseteq S \times S$ be a relation s.t. $\forall \alpha \in \Lambda$, $\forall p,q\in S$ with $R(p,q)$,

* $\forall p'. p \xrightarrow{\alpha} p' \implies \exists \beta, q'. \alpha \approx \beta \land q \xrightarrow{\beta} q' \land R(p',q');$
* $\forall q'. q \xrightarrow{\alpha} q' \implies \exists \beta, p' . \alpha \approx \beta \land p \xrightarrow{\beta} p' \land R(p',q').$

If we take $\approx$ to be syntactic equality $\equiv$, we recover the original definition of bisimulation.

My question: Has this form of bisimulation been studied? What is it called? In particular, I'm interested in workable definitions of (bi)simulation in a system which allows value-passing, where we might want to allow some set of OK values, rather than restrict to syntactic equality of actions.

More generally, I am interested in alternative definitions of bisimulation which lead to notions of "observational equivalence".

**Tags:** reference-request, automata-theory, pl.programming-languages, process-algebra, lts-simulations
> **Comments:**
> **username_1**: There has been a lot of work on different notions of process equivalence in the 1990s. Rob van Glabbeek's *The Linear Time - Branching Time Spectrum* Parts 1 and 2 are places to start looking. In the context of $\pi$-calculus you have *early* and *late* bisimulations, and b/c you can extrude scope, you will certainly want to equate $\alpha$-equivalent output-transitions. In higher-order process calculi, where you can pass processes (so they show up in labels) the question comes up as well.  
> **username_2**: Your notion of bisimulation is just the standard one where you consider the set of labels to be $\Lambda/\!\approx$ (the equivalence classes) rather than $\Lambda$.  So there's nothing you can do with your definition that you can't do with the usual one.  Or maybe you want to say something different?  
> **username_0**: @DamianoMazza One can repackage the standard definition of bisimulation into a coalgebraic definition (see [here](https://en.wikipedia.org/wiki/Bisimulation#Coalgebraic_definition)). This gives a nice characterization of bisimulation as a particular kind of commuting diagram. It is not obvious to me how things here change when considering equivalence classes instead of syntactic equality. This is one of the main examples I had in mind with this question.  
> **username_2**: Suppose you have an lts $S$ with labels $\{a,b,c\}$.  You decide that $a$ and $b$ should be equivalent, so you take $S$, rename all transitions labelled by $a$ or $b$ to a new label $d$, and get an lts $S'$ on $\{c,d\}$.  The usual definition of bisimulation for $S'$ corresponds exactly to your modified bisimulation on $S$, in the sense that $p$ and $p'$ will be bisimilar in $S'$ iff they are bisimilar in $S$ in your sense.  Also, the coalgebraic reformulation you are interested in applies without changes to $S'$.  You just needed to relabel things.  What else are you looking for?  
> **username_1**: Since you mention "observational equivalence", there are also *weak* notions of process equivalences, where, simplifying a bit, strings $\sigma_1$ and $\sigma_2$ are considered equal if $\hat{\sigma}_1 = \hat{\sigma}_2$ where the function $\hat{\cdot}$ removes invisible actions.  If your model of computing is un-timed, you will need something like this for observational equivalency, since in such a setting, internal compute steps  cannot be observed.  
> **username_1**: A useful model for thinking about observational equivalence is that computational steps are given unlabelled: $P \rightarrow Q$. Observational equivalence is defined as closure under all possible context using $\rightarrow$. Now reasoning about process (in)equality wrt all possible context is annoying, so you use labelled transitions as convenience: a proof techniques for reasoning about process (in)equality where labels represent *minimal distinguishing contexts*: if you can say something about a process wrt minimal context, this then can (often) be used to say something about all contexts.  

---

## 0 answers

