Fluid approximation and stochastic model checking

In this seminar, we will discuss how and to what extent fluid approximation techniques, which have recently received a lot of attention in the formal methods community to speed up the analysis of stochastic process algebra models, can be used to define approximate stochastic model checking algorithms. In particular, we will focus on a class of stochastic temporal logic (CSL) formulae, that expresses properties of single agents in a population model, and we will present an approximate model checking algorithm based on fluid 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.