The probabilistic model corresponding to a PRISM language description is constructed as the parallel composition of its modules. In every state of the model, there is a set of commands (belonging to any of the modules) which are enabled, i.e. whose guards are satisfied in that state. The choice between which command is performed (i.e. the scheduling) depends on the model type.
For an MDP, as in Example 1, the choice is nondeterministic. By way of example, consider state (0,0) (i.e. x=0 and y=0). There are two commands enabled, one from each module:
In state (0,0) of the MDP, there would be a nondeterministic choice between these two probability distributions:
0.8:(0,0) + 0.2:(1,0) (module M1 moves)
0.8:(0,0) + 0.2:(0,1) (module M2 moves)
For a DTMC, the choice is probabilistic: each enabled command is selected with equal probability.
If Example 1 was a DTMC, then in state (0,0) of the model
the following probability distribution would result:
0.8:(0,0) + 0.1:(1,0) + 0.1:(0,1)
For a CTMC, as will be discussed shortly, the choice is modelled as a "race" between transitions.
See the later sections on "Synchronisation" and "Process Algebra Operators" for other topics related to parallel composition.
Site hosted at the Department of Computer Science, University of Oxford