Title: The PRISM tool and its applications
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.