### Jane Hillston (Informatics, University of Edinburgh)

#### A fluid approach to model checking

*Joint work with Luca Bortolussi (University of Trieste, CNR and University of Saarbrueken).*

*Wednesday 28 January 2015 at 15.00, JCMB 6206*

##### Abstract

In computer science, "model checking" refers to a technique for automatically
querying the behaviour of an automata-based model with respect to a property
expressed in a suitable logic. This technique has been extended to continuous
time Markov chain (CTMC) models with properties expressed in the Continuous
Stochastic Logic (CSL). However, this technique relies on an explicit
representation of the state space, with suitable modification to reflect the
property of interest. For many models, particularly population CTMC (PCTMC)
the approach becomes intractable.

For some analysis of PCTMCs, based on Kurtz's Theorem, a fluid or mean field
approximation of the CTMC is used, capturing the dynamics of the system
instead as a set of ordinary differential equations (ODEs). This avoids the
state space explosion problem and gives a good approximation of the expected
behaviour of the process; an approximation that improves as the size of the
system gets larger.

In this talk I will introduce the ideas of model checking CTMCs and the logic
CSL. I will then go on to present recent work on adapting the model checking
approach to work with a fluid representation of a PCTMC, when checking
properties of a single agent within the system.

### Seminars by year

*Current*
*2016*
*2015*
*2014*
*2013*
*2012*
*2011*
*2010*
*2009*
*2008*
*2007*
*2006*
*2005*
*2004*
*2003*
*2002*
*2001*
*2000*
*1999*
*1998*
*1997*
*1996*