Please use this identifier to cite or link to this item:
Title: A Monte Carlo model checker for probabilistic LTL with numerical constraints
Authors: Gilbert, D
Donaldson, R
Issue Date: 2008
Publisher: University of Glasgow
Citation: Technical Report TR-2008-282 at the Department of Computer Science at University of Glasgow
Abstract: 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. The efficiency of the model checker is through approximation using Monte Carlo sampling of finite paths through the model’s state space (simulation outputs) and parallel model checking of the paths. Our model checking method can be applied to any model producing quantitative output – continuous or stochastic, 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 find in this paper that 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. 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 rigourous approach for the structured formal engineering of biological systems.
Appears in Collections:Publications
Computer Science
Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
technicalreportMC2pltlc[1].pdf209.57 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.