×

zbMATH — the first resource for mathematics

A logic of behaviour in context. (English) Zbl 1311.68083
Summary: We present a novel temporal logic for expressing properties of behaviour in context. The logic is applied to models of continuous processes, specifically using the continuous \(\pi\)-calculus as a modelling language for biochemical systems.
The logic allows the expression of the temporal behaviour of a system when placed in the context of another system. Here we study this in terms of biochemical reactions and the expression of temporal behaviour in the context of other biochemical processes. We present the syntax and semantics of the logic and study the model-checking problem over continuous time and continuous state-space process models, using the continuous \(\pi\)-calculus.
We present a succinct, but naive, model-checking algorithm and then show how this can be improved. We investigate the complexity of model-checking, where repeated ODE solving emerges as a particular cost; assess some limitations of the technique; and identify potential routes to overcome these.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
92C40 Biochemistry, molecular biology
Software:
Casaal; MoMo; COPASI
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Cardelli, L.; Gordon, A., Anytime, anywhere: modal logics for mobile ambients, (Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (2000), ACM), 365-377 · Zbl 1323.68405
[2] Antoniotti, M.; Policriti, A.; Ugel, N.; Mishra, B., Model building and model checking for biochemical processes, Cell Biochem. Biophys., 38, 3, 271-286, (2003)
[3] Calzone, L.; Chabrier-Rivier, N.; Fages, F.; Soliman, S., Machine learning biochemical networks from temporal logic properties, (Transactions on Computational Systems Biology VI, (2006)), 68-94
[4] Kwiatkowski, M., A formal computational framework for the study of molecular evolution, (2010), University of Edinburgh, PhD thesis
[5] Kwiatkowski, M.; Stark, I., The continuous π-calculus: A process algebra for biochemical modelling, (Computational Methods in Systems Biology, (2008), Springer), 103-122
[6] Milner, R., Communicating and mobile systems: the pi-calculus, (1999), Cambridge University Press · Zbl 0942.68002
[7] Regev, A.; Silverman, W.; Shapiro, E., Representation and simulation of biochemical processes using the pi-calculus process algebra, (Pacific Symposium on Biocomputing, vol. 6, (2001), World Scientific Pub. Co. Inc.), 459-470
[8] Regev, A.; Shapiro, E., Cells as computation, Nature, 419, 343, (2002)
[9] Chabrier-Rivier, N.; Fages, F.; Soliman, S., The biochemical abstract machine BIOCHAM, (Computational Methods in Systems Biology, (2005), Springer), 172-191 · Zbl 1088.68817
[10] Calder, M.; Gilmore, S.; Hillston, J., Automatically deriving ODEs from process algebra models of signalling pathways, (Proceedings of Computational Methods in Systems Biology, (2005)), 204-215
[11] Calder, M.; Duguid, A.; Gilmore, S.; Hillston, J., Stronger computational modelling of signalling pathways using both continuous and discrete-state methods, (Computational Methods in Systems Biology, (2006), Springer), 63-77
[12] Huang, C. Y.; Ferrell, J. E., Ultrasensitivity in the mitogen-activated protein kinase cascade, Proc. Natl. Acad. Sci. USA, 93, 19, 10078-10083, (1996)
[13] Clark, A.; Gilmore, S.; Georgoulas, A.; Hillston, J.; Stark, I.; Banks, C.; Milios, D., Stochastic modelling of the kai-based Circadian clock, Electron. Notes Theor. Comput. Sci., 296, 43-60, (2013)
[14] Jolley, C. C.; Ode, K. L.; Ueda, H. R., A design principle for a posttranslational biochemical oscillator, Cell Rep., 2, 4, 938-950, (2012)
[15] Buchler, N. E.; Louis, M., Molecular titration and ultrasensitivity in regulatory networks, J. Mol. Biol., 384, 5, 1106-1119, (2008)
[16] Alur, R.; Feder, T.; Henzinger, T., The benefits of relaxing punctuality, J. ACM, 43, 1, 116-146, (1996) · Zbl 0882.68021
[17] Caires, L.; Lozes, E., Elimination of quantifiers and undecidability in spatial logics for concurrency, Theor. Comput. Sci., 358, 2-3, 293-314, (2006) · Zbl 1097.68085
[18] de Nicola, R. D.; Loreti, M., Momo: A modal logic for reasoning about mobility, (Formal Methods for Components and Objects, (2005), Springer), 95-119 · Zbl 1143.68364
[19] Hoops, S.; Sahle, S.; Gauges, R.; Lee, C.; Pahle, J.; Simus, N.; Singhal, M.; Xu, L.; Mendes, P.; Kummer, U., COPASI-a complex pathway simulator, Bioinformatics, 22, 24, 3067-3074, (2006)
[20] Rizk, A.; Batt, G.; Fages, F.; Soliman, S., Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures, Theor. Comput. Sci., 412, 26, 2827-2839, (2011) · Zbl 1216.68164
[21] Fages, F.; Rizk, a., On temporal logic constraint solving for analyzing numerical data time series, Theor. Comput. Sci., 408, 1, 55-65, (2008) · Zbl 1160.68545
[22] Rosu, G.; Havelund, K., Rewriting-based techniques for runtime verification, Autom. Softw. Eng., 12, 2, 151-197, (2005)
[23] Bulychev, P.; David, A.; Larsen, K.; Legay, A.; Li, G.; Poulsen, D. B.g., Monitor-based statistical model checking for weighted metric temporal logic, (Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, (2012), Springer-Verlag), 168-182 · Zbl 1352.68147
[24] Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, (Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, (2004), Springer), 152-166 · Zbl 1109.68518
[25] Donzé, A.; Maler, O., Robust satisfaction of temporal logic over real-valued signals, (Formal Modeling and Analysis of Timed Systems, (2010), Springer), 92-106 · Zbl 1290.68071
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.