Bisimulation

See Colin Stirling, Bisimulation and Logic.pdf

A labelled transition system a triple \((\text{Pr},\text{Act},\to)\) where \(\text{Pr}\) is a nonempty set of states or processes, \(\text{Act}\) a set of labels and \(\to\) is a subset of \(\text{Pr}\times\text{Act}\times\text{Pr}\), which is called the transition relation. We write \(P\xrightarrow{a}Q\) when \((P,a,Q)\in \to\) and call it a transition.

A Kripke model is an LTS with a valuation \(V:\text{Prop}\to \mathcal{P}(\text{Pr})\) that maps each proposition \(p\in\text{Prop}\) to a set \(V(p)\subseteq \text{Pr}\). (Traditionally a Kripke model has unlabelled transition \(P\to Q\) representing that state \(Q\) is accessible to \(P\).

Bisimulation. A bisimulation is a binary relation \(r\) on states of an LTS s.t. whenever \(P r Q\) and \(a\in A\):

For all \(P'\) with \(P\xrightarrow{a} P'\) there is \(Q'\) such that \(Q\xrightarrow{a} Q'\) and \(P' r Q'\).
For all \(Q'\) with \(Q\xrightarrow{a} Q'\) there is \(P'\) such that \(P\xrightarrow{a} P'\) and \(P' r Q'\).

Occasionally bisimulations are also allowed between states of different LTSs by taking the disjoint union of two LTSs as an LTS. We denote with \(P\sim Q\) if \(P\) and \(Q\) are bisimilar. Oddly enough, this seems to be the statement that product and coproduct exist.

In the case of Kripke models (with valuation \(V\)) there is an extra clause in the definition:

for all \(p\in\text{Prop}\), \(P\in V(p)\) iff \(Q\in V(p)\).

Bisimulation invariant. An \(n\)ary property of a LTS is a set \(\Gamma\subseteq \text{Pr}^n\). It is bisimulation invariant if whenever \((P_1,\ldots,P_n)\in \Gamma\) and \(P_i \sim Q_i\) then also \(Q_i\in\Gamma\).

van Bentham's expressive result#

Propositional modal logic corresponds to the fragment of first-order logic that is bisimulation invariant.