Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/2886
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Gilbert, D | - |
dc.contributor.author | Donaldson, R | - |
dc.coverage.spatial | 14 | en |
dc.date.accessioned | 2008-12-05T15:15:22Z | - |
dc.date.available | 2008-12-05T15:15:22Z | - |
dc.date.issued | 2008 | - |
dc.identifier.citation | Technical Report TR-2008-282 at the Department of Computer Science at University of Glasgow | en |
dc.identifier.uri | http://bura.brunel.ac.uk/handle/2438/2886 | - |
dc.description.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. | en |
dc.format.extent | 214603 bytes | - |
dc.format.mimetype | application/pdf | - |
dc.language.iso | en | - |
dc.publisher | University of Glasgow | en |
dc.title | A Monte Carlo model checker for probabilistic LTL with numerical constraints | en |
dc.type | Report | en |
Appears in Collections: | Publications Computer Science Dept of Computer Science Research Papers |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
technicalreportMC2pltlc[1].pdf | 209.57 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.