Abstract
In this paper, we suggest a possible confluence of the theory of hybrid automata and the techniques of algorithmic algebra to create a computational basis for systems biology. We describe a method to compute bounded reachability by combining Taylor polynomials and cylindric algebraic decomposition algorithms. We discuss the power and limitations of the framework we propose and we suggest several possible extensions. We briefly show an application to the study of the Delta-Notch protein signaling system in biology.
The work reported in this paper was supported by grants from NSF’s Qubic program, NSF’s ITR program, Defense Advanced Research Projects Agency (DARPA),Howard Hughes Medical Institute (HHMI) biomedical support research grant, the US Department of Energy (DOE), the S Air Force (AFRL), National Institutes of Health (NIH) and New York State Office of Science, Technology & Academic Research (NYSTAR).F.W.was partially supported by the Austrian Science Foundation (FWF) under the research project DET (P16357-N04). C.P.was partially supported by MIUR FIRB grant RBAU018RCZ and the MIUR PRIN’04 grant 2004013015.
Chapter PDF
Similar content being viewed by others
Keywords
- Hybrid System
- Symbolic Computation
- Hybrid Automaton
- Taylor Polynomial
- Defense Advance Research Project Agency
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Courcoubetis, C., Dill, D.: Model-Checking for Real-Time Systems. In: International Symposium on Logic in Computer Science, vol. 5, pp. 414–425. IEEE Computer Press, Los Alamitos (1990)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 3–34 (1995)
Alur, R., Dang, T., Ivancic, F.: Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003)
Alur, R., Henzinger, T.A.: Pei-Hsin Ho. Automatic Symbolic Verification of Embedded Systems. In: IEEE Real-Time Systems Symposium, pp. 2–11. IEEE Press, Los Alamitos (1993)
Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Reasoning about Biochemical Processes. Cell Biochemistry and Biophysics 38, 271–286 (2003)
Asarin, E., Dang, T., Maler, O., Bournez, O.: Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Bensalem, S., Ganesh, V., Lakhnech, Y., Muñoz, C., Owre, S., Rueß, H., Rushby, J., Rusu, V., Saïdi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: Holloway, C.M. (ed.) NASA Langley Formal Methods Workshop, pp. 187–196 (2000)
Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and Real Computation. Springer, Heidelberg (1997)
Chutinan, A., Krogh, B.: Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 76–90. Springer, Heidelberg (1999)
Collier, J.R., Monk, N.A.M., Maini, P.K., Lewis, J.H.: Pattern Formation by Lateral Inhibition with Feedback: a Mathematical Model of Delta-Notch Intercellular Signalling. Journal of Theor. Biology 183, 429–446 (1996)
Cornish-Bowden, A.: Fundamentals of Enzyme Kinetics, 3rd edn. Portland Press, London (2004)
Ghosh, R., Tiwari, A., Tomlin, C.: Automated symbolic reachability analysis; with application to delta-notch signaling automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 233–248. Springer, Heidelberg (2003)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-time Systems. In: 7th Annual IEEE Symposium on Logic in Computer Science, June 1992, pp. 394–406. IEEE Computer Society Press, Los Alamitos (1992)
Hong, H.: Quantifier elimination in elementary algebra and geometryby partial cylindrical algebraic decomposition, version 13 (1995), WWW site, www.eecis.udel.edu/~saclib
Keener, J.P., Sneyd, J.: Mathematical Physiology. Springer, New York (1998)
Lanotte, R., Tini, S.: Taylor Approximation for Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 402–416. Springer, Heidelberg (2005)
Mishra, B.: Algorithmic Algebra. Springer, New York (1993)
Mishra, B.: Computational Differential Algebra, pp. 111–145. World Scientific, Singapore (2000)
Mishra, B.: A Symbolic Approach to Modeling Cellular Behavior. In: Sahni, S.K., Prasanna, V.K., Shukla, U. (eds.) HiPC 2002. LNCS, vol. 2552, pp. 725–732. Springer, Heidelberg (2002)
Mishra, B.: Computational Real Algebraic Geometry, pp. 740–764. CRC Press, Boca Raton (2004)
Nerode, A., Kohn, W.: Hybrid Systems and Constraint Logic Programming. In: Warren, D.S. (ed.) International Conference on Logic Programming (ICLP 1993), pp. 18–24. MIT Press, Cambridge (1993)
Tiwari, A., Khanna, G.: Series of Abstraction for Hybrid Automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002)
Voit, E.O.: Computational Analysis of Biochemical Systems. In: A Pratical Guide for Biochemists and Molecular Biologists. Cambridge University Press, Cambridge (2000)
Winkler, F.: Polynomial Algorithms in Computer Algebra. Springer, New York (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B. (2005). Algorithmic Algebraic Model Checking I: Challenges from Systems Biology. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_3
Download citation
DOI: https://doi.org/10.1007/11513988_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)