Model Checking Single Agent Behaviors by Fluid Approximation

In the last decade fluid approximation or mean field approximation techniques, used to approximate very large scale stochastic population systems modelled as CTMCs, have been embedded in various quantitative formal methods.  Initially the focus was on tracking the behaviour of subpopulations over time and checking the satisfaction of simple LTL properties against the deterministic traces generated by the ordinary differential equations used to approximate the behaviour.  However this loses all the stochasticity in the system.
In this work we develop an approach to stochastic model checking of CSL formulae, which takes advantage of the fluid limit results, but nevertheless retains some stochasticity. We focus on properties describing the behaviour of a single agent in a large population of agents, exploiting a limit result known as “fast simulation” which allows us to assume a form of decoupling between agents.  In particular, we approximate the behaviour of a single agent with a time-inhomogeneous CTMC, which depends on the environment and on the other agents only through the solution of the fluid differential equation. I will aim to give an intuitive introduction to the ideas underlying fluid limits and how we can harness them to efficiently, approximately model check single agent behaviours within extremely large populations which would be very inefficient to check using rival techniques such as statistical model checking.
This is joint work with Luca Bortolussi (University of Trieste, CNR and University of Saarbrueken).