Computing at Glasgow University
Paper ID: 8891
DCS Tech Report Number: TR-2008-282

A Monte Carlo Model Checker for Probabilistic LTL with Numerical Constraints
Donaldson,R. Gilbert,D.

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2008

We define the syntax and semantics of a new temporal logic called probabilistic LTL with numerical constraints (PLTLc). We introduce an efficient model checker for PLTLc properties. PLTLc properties with constraints over free variables can replace full model checking experiments, resulting in a significant gain in efficiency. This overcomes one disadvantage of model checking experiments which is that the complexity depends on system granularity and number of variables, and quickly becomes infeasible. In addition, the efficiency of the model checker is improved by approximation using Monte Carlo sampling of behaviour traces and parallel model checking of the traces. Our model checking method can be applied to any model producing quantitative output -- including those with complex dynamics and those with an infinite state space. Furthermore, our offline approach allows the analysis of observed (real-life) behaviour traces. We focus on models of biochemical networks, and specifically in this paper on intracellular signalling pathways; however our method can be applied to a wide range of biological as well as technical systems and their models. Our work contributes to the emerging field of synthetic biology by proposing a rigorous approach for the structured formal engineering of biological systems.

Keywords: Systems Biology, Model Checking, Probabilistic LTL

PDF Bibtex entry Endnote XML