Tag Archives: PRISM

25.01.2013 – Talk by Hoang Vu Tuan

Title: The PRISM tool and its applications
Time: 14:00
Location: Meeting room
Type: Tool presentation
Speaker: Hoang Vu Tuan

In this presentation, I will consider some models and show how it is possible to derive some meaningful properties by using the PRISM model checker. PRISM tool supports  four types of models whose underlying processes can be Discrete-time Markov chain (DTMC), Continuous-time
Markov chains (CTMC), Markov decision processes (MDP) and Probabilistic timed automata (PTA). For each of these classes, a set of properties can be analysed. The talk will rely on a case study to illustrate the PRISM functionalities. Specifically,  the Stable Matching problem will be addressed by applying the DTMC analysis.