Tag Archives: Model checking

29.05.2013 – Talk by Luca Bortolussi

Title: Mean field approximation for stochastic model checking
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Luca Bortolussi
Mean field approximation techniques are well established approaches to analyse large-scale stochastic processes, especially population Markov models. Some years ago, they have entered the arena of quantitative formal methods, and they provided a consistent way to define fluid semantics for stochastic process algebras.
Here, we will discuss how mean field approximation can play a role in another successful area of quantitative formal methods, namely stochastic model checking. In particular, we will focus on a subclass of Continuous Stochastic Logic (CSL), considering formulae that expresses properties of single agents in a population model, and we will present an approximate model checking algorithm based on mean field approximation. We will also discuss model checking CSL formulae against time-inhomogeneous CTMC models, as this turns out to be the core procedure needed for fluid approximation.
Finally, we will consider a class of global properties that can be analysed by linear noise approximation, a higher order fluid approximation.

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.