Alex Bork

Add interpreter lock release to POMDP check function

4

The POMDP check function binding is lacking the release of the global interpreter lock that allows other processes to take control of a stopped belief exploration model checker. Thanks to...

This PR extends Storm to handle reward bounded until formulae without an explicitly specified reward model, i.e. a formula of the form `P=? [ "safe" Urew

Support for discounted properties in MDPs and DTMCs

4

This PR adds support for checking cumulative and total reward properties with a given discount factor on MDPs and DTMCs. - Extends the parser to allow discounted properties, proposed syntax...

Extended handling of terminal states for POMDPs

1

This PR extends the handling of states marked as terminal in the PrismNextStateGenerator. In particular, terminal states in POMDPs are expanded with self-loops for all enabled actions, preventing erroneous behavior...

Missing handling of terminal states for POMDPs

2

States that are marked as terminal while building a POMDP model (for example due to violating the left-hand side of an Until) are not handled appropriately. By default, for terminal...

The detection of terminal states in the model building leads to unexpected, diverging behavior. Consider for example the following MDP ``` mdp module model s : [0..4] init 0; [a]...