# Partition refinement in transition state systems (bisimulation contraction)

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.

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.