For uncertain models, currently interval MDPs (IMDPs) or interval DTMCs (IDTMCs), PRISM performs robust verification, which considers the best- or worst-case behaviour that can arise depending on the way that probabilities are selected from intervals.
For example, instead of a property for a DTMC such as
which asks for the probability to reach a state satisfying "goal", IDTMCs use MDP-style queries:
which compute the minimum or maximum possible probability that can arise.
Similarly, for an IMDP, there are now two separate quantifications, firstly over strategies (policies) and secondly over the distinct ways that transition probabilities can be selected from intervals, for which min or max appear in that order in the query. For example:
return the minimum and maximum values, respectively, over resolutions of transition probabilities for the maximum probability of reaching "goal". Similarly, minmin and minmax are used for the minimum probability of reaching "goal". Model checking is supported for:
P operator, for next and bounded/unbounded until/reachability properties
R operator, for the expected reward to reach a target or satisfy a co-safe LTL formula
Site hosted at the Department of Computer Science, University of Oxford