Separately from the choice of engines, PRISM often offers several different solution methods that can be used when performing model checking. The choice of method (and their settings) depends on the type of analysis that is being done.
When analysing MDPs, there are several options. You can select these under the "MDP solution method" setting from the GUI, or use the command-line switches listed below. Currently, all except value iteration are only supported by the explicit engine. For more details of the methods, see e.g. [FKNP11] (about probabilistic verification of MDPs) or classic MDP texts such as [Put94]).
-valiter) [this is the default]
-gs)
-politer)
-modpoliter)
Where the methods above use iterative numerical solution, you can also use the settings under "Convergence" described in the Iterative Numerical Methods section.
When computing transient probabilities of a CTMC
(either directly or when verifying time-bounded operators of CSL), there are two options:
uniformisation and fast adaptive uniformisation (FAU). These can be selected using the GUI option "Transient probability computation method", or using the command-line switch -transientmethod <name>, where <name> is either unif or fau.
Uniformisation is a standard iterative numerical method for computing transient probabilities on a CTMC, which works by reducing the problem to an analysis of a "uniformised" DTMC.
As an optimisation, when it is detected that the transient probabilities have converged, no further iterations are performed. If necessary (e.g. in case of round-off problems), this optimisation can be disabled with the "Use steady-state detection" option (command-line switch -nossdetect).
Fast adaptive uniformisation (FAU) [MWDH10] is a method to efficiently approximate transient properties of large CTMCs. The basic idea is that only the parts of the model that are relevant for the current time period are kept in memory. In more detail, starting with the initial states, in each step FAU explores further states in a DTMC which is a discrete-time version of the original CTMC. By combining the probabilities there with those of a certain continuous-time stochastic process (a birth process), transient properties in the original CTMC can be computed. If it turns out that the probability of being in some state in the DTMC is below a given threshold, this state is removed from the model explored so far. After a given number of steps, which corresponds to the number of steps which are likely to happen within the time bound, the exploration can be stopped. In the implementation in PRISM [DHK13], FAU can be used to compute transient probability distributions and to model check the following types of non-nested CSL formulas: time-bounded until, instantaneous reward, cumulative reward.
The following options can be used to configure FAU:
-fauepsilon <x>): FAU analyses the DTMC for a number of iterations such that the probability of more steps being relevant is below this value. The default is 1e-6.
-faudelta <x>): States that have a lower probability than this value are discarded. The default is 1e-12.
-fauarraythreshold <x>): After this number of steps without any new states being explored or discarded, FAU will switch to a faster, fixed-size data structure until further states have to be explored or discarded. The default is 100.
-fauintervals <x>): In some cases, it is advantageous to divide the time interval the analysis is done for into several smaller intervals. This option dictates the number of (equal length) intervals used for this split. The default is 1, meaning that only one time interval is used.
-fauinitival <x>): It is also possible to specify an additional initial time interval which is handled separately from the rest of the time. This is often advantageous, because in this interval certain parameters of the model can be explored, which can subsequently be used to speed up the computation of the remaining time interval. The default for this option is 1.0.