As mentioned above, the PRISM language can be used to describe several types of probabilistic models:
DTMCs, CTMCs, MDPs and PTAs.
To indicate which type is being described, a PRISM model should include one of the keywords
dtmc
, ctmc
, mdp
or pta
.
This is typically at the very start of the file,
but can actually occur anywhere in the file (except inside modules and other declarations).
If no such model type declaration is included, the model is by default assumed to be an MDP.
Note: As mentioned earlier, PRISM also supports probabilistic automata (PAs) [Seg95], but (mis)uses the terminology Markov decision process (MDP) for this model.
Note: For compatibility with old versions of PRISM,
the keywords probabilistic
, stochastic
and nondeterministic
can be used as alternatives for dtmc
, ctmc
and mdp
, respectively.