We present an algorithm, called BioLab, for verifying temporal properties of rule-based models of cellular signalling networks. BioLab models are encoded in the BioNetGen language, and properties are expressed as formulae in probabilistic bounded linear temporal logic. Temporal logic is a formalism for representing and reasoning about propositions qualified in terms of time. Properties are then verified using sequential hypothesis testing on executions generated using stochastic simulation. BioLab is optimal, in the sense that it generates the minimum number of executions necessary to verify the given property. BioLab also provides guarantees on the probability of it generating Type-I (i.e., false-positive) and Type-II (i.e., false-negative) errors. Moreover, these error bounds are pre-specified by the user. We demonstrate BioLab by verifying stochastic effects and bistability in the dynamics of the T-cell receptor signaling network. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Clarke, E. M., Faeder, J. R., Langmead, C. J., Harris, L. A., Jha, S. K., & Legay, A. (2008). Statistical model checking in BioLab: Applications to the automated analysis of T-cell receptor signaling pathway. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5307 LNBI, pp. 231–250). https://doi.org/10.1007/978-3-540-88562-7_18
Mendeley helps you to discover research relevant for your work.