probabilistic-model-checking Analysing and modelling probabilistic systems with PRISM concurrent-philosophers Markov decision processes dynamic-power-management Continuous-time Markov chains EGL-contract-signing Discrete-time Markov chains self-stabilisation-and-die-algorithms Probabilistic automata