I have a labelled transition system (the one to the left in the picture below)
As can be seen from the picture, the two transition systems are 'equivalent'.
So I want to transform the one on the left to the one on the right. I know this is called bisimulation contraction (partition refinement), and I have found some lecture slides explaining what the algorithm is like (which also includes some Haskell code), but I don't really understand how to do it.
I am trying to use the algorithm in JavaScript.
I have an array of nodes S and an array of edges R
N = [
{ id: 'n1', propositions: 'p' },
{ id: 'n2', propositions: 'p' },
{ id: 'n3', propositions: 'q' },
{ id: 'n4', propositions: 'q' },
]
R = [
{ source: 'n1', target: 'n2', label: 'pi_1' },
{ source: 'n2', target: 'n3', label: 'pi_2' },
{ source: 'n1', target: 'n4', label: 'pi_2' },
}
In the algorithm, it says that I should initially create a partition with all the same valuations, so the initial partition has two subblocks:
initial_partition = {
'p': ['n1', 'n2'],
'q': ['n3', 'n4']
}
Now I need to partition each block into subblocks based on their relations.
But how do I do this and how do I end up with the one to the left (i.e. when do I delete some of the nodes)?
I have found this StackExchange question and this Wikipedia page, but it does not help me to fully understand it.