symbolic bisimulation changes results

[temunds]

Hello everyone,

i am currently working on branch 1.8.0 (due to compatibility with stormpy) and trying to solve timed reachability properties for markov automata.

I have encountered a difference in the results depending on whether bisimulation is used.

Log 1 (without bisim):

storm --prism 2_trains_default_no_precedence.pm -pc --prop 'Tmin=? [F "done"]' -e hybrid
Storm 1.8.0

Date: Mon Feb  5 08:27:47 2024
Command line arguments: --prism 2_trains_default_no_precedence.pm -pc --prop 'Tmin=? [F "done"]' -e hybrid

Time for model input parsing: 0.001s.

 WARN (model-handling.h:305): Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.
Time for model construction: 0.525s.

--------------------------------------------------------------
Model type:     Markov Automaton (symbolic)
States:         42 (68 nodes)
Transitions:    51 (709 nodes)
Choices:        42
Reward Models:  none
Variables:      rows: 8 meta variables (16 DD variables), columns: 8 meta variables (16 DD variables), nondeterminism: 11 meta variables (11 DD variables)
Labels:         3
   * deadlock -> 0 state(s) (1 nodes)
   * init -> 1 state(s) (17 nodes)
   * done
--------------------------------------------------------------

Model checking property "1": T[exp]min=? [F "done"] ...
Result (for initial states): 11.00823786
Time for model checking: 0.043s.

Log 2 (with bisim):

storm --prism 2_trains_default_no_precedence.pm -pc --prop 'Tmin=? [F "done"]' -e hybrid -bisim
Storm 1.8.0

Date: Mon Feb  5 08:21:46 2024
Command line arguments: --prism 2_trains_default_no_precedence.pm -pc --prop 'Tmin=? [F "done"]' -e hybrid -bisim

Time for model input parsing: 0.001s.

 WARN (model-handling.h:305): Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the input model.
Time for model construction: 0.413s.

--------------------------------------------------------------
Model type:     Markov Automaton (symbolic)
States:         42 (68 nodes)
Transitions:    51 (709 nodes)
Choices:        42
Reward Models:  none
Variables:      rows: 8 meta variables (16 DD variables), columns: 8 meta variables (16 DD variables), nondeterminism: 11 meta variables (11 DD variables)
Labels:         3
   * deadlock -> 0 state(s) (1 nodes)
   * init -> 1 state(s) (17 nodes)
   * done
--------------------------------------------------------------

Time for model preprocessing: 0.092s.

--------------------------------------------------------------
Model type:     Markov Automaton (symbolic)
States:         31 (17 nodes)
Transitions:    40 (506 nodes)
Choices:        31
Reward Models:  none
Variables:      rows: 1 meta variables (16 DD variables), columns: 1 meta variables (16 DD variables), nondeterminism: 11 meta variables (11 DD variables)
Labels:         4
   * ((((state_dispatching = 0) & (state_arrs_line_1 = 4)) & (state_t2 = 8)) & (state_t2 = 8)) -> 1 state(s) (17 nodes)
   * deadlock -> 0 state(s) (1 nodes)
   * done -> 1 state(s) (17 nodes)
   * init -> 1 state(s) (17 nodes)
--------------------------------------------------------------

Model checking property "1": T[exp]min=? [F "done"] ...
Result (for initial states): 4.742193126
Time for model checking: 0.014s.

In both cases the enginge 'hybrid' has been used, as the sparse engine does not seem to support bisimulation for markov automata.

Unfortunately, i can only share the full model file in private.

Best regards :)

[volkm]

Thanks for the bug report. Can you privately share the model file with us via the following email address: support@stormchecker.org Then we can take a deeper look into the issue.

[temunds]

Sure, thanks for looking into this.

[tquatmann]

This seems to work if instead of --engine hybrid you select --engine dd-to-sparse. Maybe that is a workaround for your use case? The two engines are rather similar. More precisely: dd-to-sparse in combination with --bisimulation will extract the bisimulation quotient in an explicit (sparse) format and will act as the (default) sparse engine from that point on. hybrid on the other hand uses symbolic (BDD-based) representations for computations on the underlying graph structure, (e.g., finding the states that almost surely reach the target) and only switches to explicit data structures for numerical computations (e.g. Value Iteration).

Side note: the expression for the label done ends with (state_t2 = 8) & (state_t2 = 8). Is there a typo?

[temunds]

Awesome, that workaround does work. Thank you!

Also thanks for the sidenote, this has been a typo, indeed.

Cheers!