Model checking single agent behaviours by fluid approximation

TitleModel checking single agent behaviours by fluid approximation
Publication TypeJournal Article
Year of Publication2015
AuthorsBortolussi L, Hillston J
JournalInformation and Computation
Volume242
Pages183-226
ISSN0890-5401
Keywordsfluid approximation, mean field approximation, reachability probability, Stochastic model checking, time-inhomogeneous Continuous Time Markov Chains
Abstract

In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will 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, and model check this process. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

URLhttp://www.sciencedirect.com/science/article/pii/S0890540115000176
DOI10.1016/j.ic.2015.03.002
File: