search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
138 stars 75 forks source link

Missing handling of terminal states for POMDPs #603

Open AlexBork opened 2 months ago

AlexBork commented 2 months ago

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 states, only one self-loop without action label is added. This, however, may lead to violation of the requirement that states with the same observation must have the same actions enabled.

This can be worked around with by using option --buildfull, but terminal states should be handled properly to reduce model building times.

This issue is based on the discussion on issue #48.

sjunges commented 2 months ago

It would probably be easy to allow this in makeCanonic and add the additional self-loops there?

AlexBork commented 2 months ago

I'm not sure if it's not a bit convoluted to get the information to makeCanonic. We need to be careful to distinguish between problems that are actual modelling errors (with respect to the POMDP requirements) and ones that arise due to our handling.

I think the most robust solution would be to handle the absorbing/terminal states correctly in the state generation, i.e. adding the self-loop transitions instead of nothing or transitions to successor states. I have implemented this yesterday and it seems to run fine. It should also introduce only minimal overhead.