**Title:** Mean field approximation for stochastic model checking

**Time:** 14:00

**Location:** Meeting room

**Type:** Research Result

**Speaker:** Luca Bortolussi

**Abstract:**

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.

# Tag Archives: Model checking

# 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

**Abstract:**

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.