moves-rwth / storm

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

Enhance support of continuous time models in dd-based engines #61

Closed tquatmann closed 4 years ago

tquatmann commented 4 years ago

Right now, CTMCs and MAs can not be model checked using the dd engine. MAs can not be checked with the hybrid engine.

Since for many queries we could just invoke the corresponding DTMC/MDP implementations, I think adding support for these is a reasonable thing to do.

tquatmann commented 4 years ago

Model checking MAs with the hybrid engine is supported since version 1.5.0. There does not seem to be a need for fully symbolic (dd) implementations right now, so I'm closing this issue.