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.
Current 2016 2015 2014 2013 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996