Difference results in MDP bisimulation by using dd engine and sparse engine

[sadeghrk2]

Hi,

When I use bisimulation for MDPs with dd and sparse engines the numbers of states of the reduced models are different for some case studies.

Several sample files are attached as follows:

coin_4_4_dd.log
coin_4_4_sparse.log
coin_4_12_dd.log
coin_4_12_sparse.log
wlan_3_200_dd.log
wlan_3_200_sparse.log
wlan_4_300_dd.log
wlan_4_300_sparse.log
zeroconf_3_dd.log
zeroconf_3_sparse.log
zeroconf_4_dd.log
zeroconf_4_sparse.log

Best,
Mohammadsadegh

[volkm]

We can reproduce this issue in the current master branch.

A minimal example is the following:

Sparse

storm --prism ~/prism-benchmarks/models/mdps/wlan/wlan1.nm --prop "Pmax=? [F col=COL]" -const "COL=1" -bisim
yields:

Model type: 	MDP (sparse)
States: 	2
Transitions: 	2
Choices: 	2

DD

storm --prism ~/prism-benchmarks/models/mdps/wlan/wlan1.nm --prop "Pmax=? [F col=COL]" -const "COL=1" -bisim -e dd-to-sparse
yields:

Model type: 	MDP (sparse)
States: 	15
Transitions: 	29
Choices: 	29

The sparse engine seems to merge everything into one state which has both labels init and col=COL. The original model however has no state with both labels.
It seems to me that the sparse bisimulation is too eager in this case.