For example, for prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm and property P=?[ F>=0 s>3 ], the explicit engine yields Infinity, while the symbolic engines yield a value ~1/3.
This is due to performing Until computations using the DTMC model checker directly on the CTMC instead of on the embedded DTMC here and here.
This only happens if there is a lower bound but no upper bound, i.e., for F>=t target or a U>=t b, CTMCs and the explicit engine.
kleinj
commented
8 years ago
For example, for
prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.smand propertyP=?[ F>=0 s>3 ], the explicit engine yieldsInfinity, while the symbolic engines yield a value ~1/3.This is due to performing Until computations using the DTMC model checker directly on the CTMC instead of on the embedded DTMC here and here.
This only happens if there is a lower bound but no upper bound, i.e., for
F>=t targetora U>=t b, CTMCs and the explicit engine.