Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Hybrid Systems: Computation and Control

HSCC 2003: Hybrid Systems: Computation and Control pp 233–248Cite as

Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2623))

Abstract

This paper describes the implementation of predicate abstraction techniques to automatically compute symbolic backward reachable sets of high dimensional piecewise affine hybrid automata, used to model Delta-Notch biological cell signaling networks. These automata are analyzed by creating an abstraction of the hybrid model, which is a finite state discrete transition system, and then performing the computation on the abstracted system. All the steps, from model generation to the simplification of the reachable set, have been automated using a variety of decision procedure and theorem-proving tools. The concluding example computes the reach set for a four cell network with 8 continuous and 256 discrete states. This demonstrates the feasibility of using these tools to compute on high dimensional hybrid automata, to provide deeper insight into realistic biological systems.

This research is supported by the DARPA Bio:Info:Micro program, grant MDA972- 00-1-0032, and the DARPA BioSpice program under contract DE-AC03-765F00098.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, T. Dang, and F. Ivancic. Reachability analysis of hybrid systems via predicate abstraction. In C. J. Tomlin and M. Greenstreet, editors, Hybrid Systems: Computation and Control, LNCS 2289, pages 35–48. Springer Verlag, 2002.

    Chapter  Google Scholar 

  2. K. Amonlirdviman, R. Ghosh, J. Axelrod and C. Tomlin. A hybrid systems approach to modeling and analyzing planar cell polarity. In International Conference on Systems Biology, Stockholm, 2002.

    Google Scholar 

  3. E. Asarin, T. Dang, and O. Maler. d/dt: A verification tool for hybrid systems. In Proc. of the IEEE Conf. on Decision and Control, pages 2893–2898, Orlando, 2001.

    Google Scholar 

  4. A. Bemporad, F. D. Torrisi, and M. Morari. Optimization-based verification and stability characterization of piecewise affine and hybrid systems. In B. Krogh and N. Lynch, editors, Hybrid Systems: Computation and Control, LNCS 1790, pages 45–59. Springer Verlag, 2000.

    Chapter  Google Scholar 

  5. S. Bensalem, V. Ganesh, Y. Lakhnech, C. Muñoz, S. Owre, H. Rueβ, J. Rushby, V. Rusu, H. Saϊdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In C. M. Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187–196, Hampton, VA, June 2000. NASA Langley Research Center.

    Google Scholar 

  6. O. Botchkarev and S. Tripakis. Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In B. Krogh and N. Lynch, editors, Hybrid Systems: Computation and Control, LNCS 1790, pages 73–88. Springer Verlag, 2000.

    Chapter  Google Scholar 

  7. A. Chutinan and B. H. Krogh. Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans. on Automatic Control, 46(9):1401–1410, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  8. G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Proc. Second GI Conf. Automata Theory and Formal Languages, LNCS 33, pages 134–183. Springer Verlag, 1975.

    Google Scholar 

  9. Computer Science Laboratory, SRI International, Menlo Park, California. SAL: Symbolic Analysis Laboratory. http://www.csl.sri.com/projects/sal/.

  10. R. Ghosh and C. J. Tomlin. Lateral inhibition through delta-notch signaling: a piecewise affine hybrid model. In M. D. D. Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, LNCS 2034, pages 232–246. Springer Verlag, 2001.

    Chapter  Google Scholar 

  11. S. Graf and H. Saϊdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verification (CAV’97), volume 1254, pages 72–83. Springer Verlag, 1997.

    Google Scholar 

  12. T. A. Henzinger, P. H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997.

    Article  MATH  Google Scholar 

  13. H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. In Proc. ISAAC 90, pages 261–264, 1990.

    Google Scholar 

  14. H. de Jong. Modeling and simulation of genetic regulatory systems: A literature review. J. Computational Biology, 9(1):69–105, 2002.

    Article  Google Scholar 

  15. B. Kuipers and S. Ramamoorthy. Qualitative modeling and heterogeneous control of global systems behavior. In C. J. Tomlin and M. Greenstreet, editors, Hybrid Systems: Computation and Control, LNCS 2289, pages 294–307. Springer Verlag, 2002.

    Chapter  Google Scholar 

  16. G. Marnellos, G. A. Deblandre, E. Mjolsness, and C. Kintner. Delta-notch lateral inhibitory patterning in the emergence of ciliated cells in Xenopus: experimental observations and a gene network model. In Pacific Symposium on Biocomputing, pages 326–337, 2000.

    Google Scholar 

  17. S. McCallum. An improved projection operator for cylindrical algebraic decomposition of three dimensional space. J. Symbolic Computation, 5:141–161, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  18. I. Mitchell. Application of level set methods to control and reachability problems in continuous and hybrid systems. PhD thesis, Stanford University, August 2002.

    Google Scholar 

  19. I. Mitchell and C. J. Tomlin. Overapproximating reachable sets by Hamilton-Jacobi projections. J. Symbolic Computation, 2003.

    Google Scholar 

  20. J. Preug and H. Wong-Toi. A procedure for reachability analysis of rectangular automata. In Proc. of the American Control Conference, pages 1674–1678, Chicago, 2000.

    Google Scholar 

  21. B. Shults and B. J. Kuipers. Proving properties of continuous systems: qualitative simulation and temporal logic. AI Journal, 92:91–129, 1997.

    MATH  MathSciNet  Google Scholar 

  22. O. Sokolsky and H. S. Hong. Qualitative modeling of hybrid systems. In Proc. of the Montreal Workshop, 2001. Available from http://www.cis.upenn.edu/~rtg/rtg papers.htm.

  23. A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, second edition, 1948.

    Google Scholar 

  24. A. Tiwari and G. Khanna. Series of abstractions for hybrid automata. In C. J. Tomlin and M. Greenstreet, editors, Hybrid Systems: Computation and Control, LNCS 2289, pages 465–478. Springer Verlag, 2002.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stanford University, Stanford, CA, USA

    Ronojoy Ghosh & Claire Tomlin

  2. Computer Science Laboratory, SRI International, Menlo Park, CA, USA

    Ashish Tiwari

Authors
  1. Ronojoy Ghosh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Claire Tomlin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS-VERIMAG, 2 avenue de Vignate, 38610, Gières, France

    Oded Maler

  2. Weizmann Institute of Science, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ghosh, R., Tiwari, A., Tomlin, C. (2003). Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-36580-X_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00913-9

  • Online ISBN: 978-3-540-36580-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation