Partition refinement in transition state systems (bisimulation contraction)

Question

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.

Answer 1

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.