<p>From both states in $\{n_1,n_2\}$, action $\pi_1$ takes you to $n_2$, while action $\pi_2$ takes you to states in $\{n_3,n_4\}$.  Hence no refinement of that block takes place.  The second block doesn't refine either; therefore the partition refinement terminates.</p>

<p>At this point you have proved that $n_1$ and $n_2$ are bisimilar and $n_3$ and $n_4$ are bisimilar.  You have computed the maximal bisimulation relation on the states of the given structure.  You then proceed to build a <em>quotient</em> structure, with one state for each equivalence class of the bisimulation relation.</p>

<p>This seems to be the part that puzzles you, but it's really simple: it's just another step in the procedure.  The upper state of the result represents the equivalence class $\{n_1,n_2\}$.  Unsurprisingly, action $\pi_1$ takes you back to that state, and so on.  In general, all states in one block of the partition agree on the block containing the destination state of transitions labeled by a certain action.  Hence constructing the quotient structure is straightforward.  </p>

<p>A state of the quotient structure is an initial state if and only if at least one state of its equivalence class is initial.  Then, the structure you build is bisimilar to the one given.</p>

<p>Note that I've used "bisimilar" in two related, but slightly different ways here: bisimilar states, and bisimilar structures.  In this example, first we compute a bisimulation relation on the states of the original structure, then we build a structure that is guaranteed to have the following property: the maximal bisimulation on the states of the two structures matches each initial state of one structure to at least one initial state of the other structure.  A structure with this property is said to be bisimilar to the original one.</p>

CC BY-SA 3.0
2016-12-23T18:31:47.070Z
2016-12-23T18:31:47.070Z
Fabio Somenzi
<p>I am trying to understand bisimulation contraction of Kripke models.</p>

<p>I have read these <a href="http://homepages.cwi.nl/~jve/courses/lai0506/LAI11.pdf" rel="nofollow noreferrer">lecture slides</a> and this <a href="https://en.wikipedia.org/wiki/Bisimulation" rel="nofollow noreferrer">Wikipedia page</a>, but I still don't fully understand it.</p>

<p>I can understand that the two models below are bisimilar</p>

<p><a href="https://i.sstatic.net/KqLvR.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/KqLvR.png" alt="enter image description here"></a></p>

<p>In the lecture slides, the partition refinement algorithm is given as</p>

<p><a href="https://i.sstatic.net/2mV6x.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/2mV6x.png" alt="enter image description here"></a></p>

<p>I do understand that from the graph on the left in the first picture, the initial partition becomes</p>

<pre><code>initial_partition = {
  'p': ['n1', 'n2'],
  'q': ['n3', 'n4']
}
</code></pre>

<p>because two of the nodes have $p$ and the two remaining nodes have $q$.</p>

<p>But now I need to understand the second step in the algorithm. It seems to me that I should first loop through each of the two blocks in the initial partition, and for each node check its relations to nodes in the other blocks in the initial partition.</p>

<p>Can someone give me an example of a larger model (more nodes), and show me the steps in reducing the larger model to a smaller model, or give me a hint on where to find literature about it where it is described more easy?</p>

<h1>Edit</h1>

<p>What I mean is that the model in the middle of this picture</p>

<p><a href="https://i.sstatic.net/kXAZG.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/kXAZG.png" alt="enter image description here"></a></p>

<p>shows the first partition, but I don't know what the next partition look like, and why I can suddenly remove two of the nodes.</p>

<graph-theory><graph-algorithms><automata-theory><partition-problem>
Partition refinement in transition state systems (bisimulation contraction)
Jamgreen
# Partition refinement in transition state systems (bisimulation contraction)

(Asked by: username_0 on 2016-12-19)

I am trying to understand bisimulation contraction of Kripke models.
I have read these lecture slides and this Wikipedia page, but I still don't fully understand it.
I can understand that the two models below are bisimilar

In the lecture slides, the partition refinement algorithm is given as

I do understand that from the graph on the left in the first picture, the initial partition becomes
initial_partition = {
  'p': ['n1', 'n2'],
  'q': ['n3', 'n4']
}

because two of the nodes have $p$ and the two remaining nodes have $q$.
But now I need to understand the second step in the algorithm. It seems to me that I should first loop through each of the two blocks in the initial partition, and for each node check its relations to nodes in the other blocks in the initial partition.
Can someone give me an example of a larger model (more nodes), and show me the steps in reducing the larger model to a smaller model, or give me a hint on where to find literature about it where it is described more easy?
Edit
What I mean is that the model in the middle of this picture

shows the first partition, but I don't know what the next partition look like, and why I can suddenly remove two of the nodes.

**Tags:** graph-theory, graph-algorithms, automata-theory, partition-problem

---

## 1 answers

### Answer by username_1 on 2016-12-23. Score: 5

From both states in $\{n\_1,n\_2\}$, action $\pi\_1$ takes you to $n\_2$, while action $\pi\_2$ takes you to states in $\{n\_3,n\_4\}$. Hence no refinement of that block takes place. The second block doesn't refine either; therefore the partition refinement terminates.

At this point you have proved that $n\_1$ and $n\_2$ are bisimilar and $n\_3$ and $n\_4$ are bisimilar. You have computed the maximal bisimulation relation on the states of the given structure. You then proceed to build a *quotient* structure, with one state for each equivalence class of the bisimulation relation.

This seems to be the part that puzzles you, but it's really simple: it's just another step in the procedure. The upper state of the result represents the equivalence class $\{n\_1,n\_2\}$. Unsurprisingly, action $\pi\_1$ takes you back to that state, and so on. In general, all states in one block of the partition agree on the block containing the destination state of transitions labeled by a certain action. Hence constructing the quotient structure is straightforward.

A state of the quotient structure is an initial state if and only if at least one state of its equivalence class is initial. Then, the structure you build is bisimilar to the one given.

Note that I've used "bisimilar" in two related, but slightly different ways here: bisimilar states, and bisimilar structures. In this example, first we compute a bisimulation relation on the states of the original structure, then we build a structure that is guaranteed to have the following property: the maximal bisimulation on the states of the two structures matches each initial state of one structure to at least one initial state of the other structure. A structure with this property is said to be bisimilar to the original one.


---

