www.prismmodelchecker.org

The PRISM Language /

Model Type

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.

PRISM Manual

The PRISM Language

[ View all ]