Bisimulation in state transition system

278 views Asked by At

I have a labelled transition system (the one to the left in the picture below)

enter image description here

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.

0

There are 0 answers