{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:51:53Z","timestamp":1742381513776},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540009139"},{"type":"electronic","value":"9783540365808"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36580-x_19","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T07:13:36Z","timestamp":1197184416000},"page":"233-248","source":"Crossref","is-referenced-by-count":41,"title":["Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata"],"prefix":"10.1007","author":[{"given":"Ronojoy","family":"Ghosh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claire","family":"Tomlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,3,14]]},"reference":[{"key":"19_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45873-5_6","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2002","unstructured":"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\u201348. Springer Verlag, 2002."},{"key":"19_CR2","unstructured":"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."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"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\u20132898, Orlando, 2001.","DOI":"10.1109\/CDC.2001.980715"},{"key":"19_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/3-540-46430-1_8","volume-title":"Hybrid Systems: Computation and Control","author":"A. Bemporad","year":"2000","unstructured":"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\u201359. Springer Verlag, 2000."},{"key":"19_CR5","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Rue\u03b2, J. Rushby, V. Rusu, H. Sa\u03cadi, 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\u2013196, Hampton, VA, June 2000. NASA Langley Research Center."},{"key":"19_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-46430-1_10","volume-title":"Hybrid Systems: Computation and Control","author":"O. Botchkarev","year":"2000","unstructured":"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\u201388. Springer Verlag, 2000."},{"issue":"9","key":"19_CR7","doi-asserted-by":"publisher","first-page":"1401","DOI":"10.1109\/9.948467","volume":"46","author":"A. Chutinan","year":"2001","unstructured":"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\u20131410, 2001.","journal-title":"IEEE Trans. on Automatic Control"},{"key":"19_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Proc. Second GI Conf. Automata Theory and Formal Languages","author":"G. E. Collins","year":"1975","unstructured":"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\u2013183. Springer Verlag, 1975."},{"key":"19_CR9","unstructured":"Computer Science Laboratory, SRI International, Menlo Park, California. SAL: Symbolic Analysis Laboratory. http:\/\/www.csl.sri.com\/projects\/sal\/ ."},{"key":"19_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-45351-2_21","volume-title":"Hybrid Systems: Computation and Control","author":"R. Ghosh","year":"2001","unstructured":"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\u2013246. Springer Verlag, 2001."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Sa\u03cadi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verification (CAV\u201997), volume 1254, pages 72\u201383. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P. H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110\u2013122, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. In Proc. ISAAC 90, pages 261\u2013264, 1990.","DOI":"10.1145\/96877.96943"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1089\/10665270252833208","volume":"9","author":"H. Jong de","year":"2002","unstructured":"H. de Jong. Modeling and simulation of genetic regulatory systems: A literature review. J. Computational Biology, 9(1):69\u2013105, 2002.","journal-title":"J. Computational Biology"},{"key":"19_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/3-540-45873-5_24","volume-title":"Hybrid Systems: Computation and Control","author":"B. Kuipers","year":"2002","unstructured":"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\u2013307. Springer Verlag, 2002."},{"key":"19_CR16","unstructured":"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\u2013337, 2000."},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0747-7171(88)80010-5","volume":"5","author":"S. McCallum","year":"1988","unstructured":"S. McCallum. An improved projection operator for cylindrical algebraic decomposition of three dimensional space. J. Symbolic Computation, 5:141\u2013161, 1988.","journal-title":"J. Symbolic Computation"},{"key":"19_CR18","unstructured":"I. Mitchell. Application of level set methods to control and reachability problems in continuous and hybrid systems. PhD thesis, Stanford University, August 2002."},{"key":"19_CR19","unstructured":"I. Mitchell and C. J. Tomlin. Overapproximating reachable sets by Hamilton-Jacobi projections. J. Symbolic Computation, 2003."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"J. Preug and H. Wong-Toi. A procedure for reachability analysis of rectangular automata. In Proc. of the American Control Conference, pages 1674\u20131678, Chicago, 2000.","DOI":"10.1109\/ACC.2000.879486"},{"key":"19_CR21","first-page":"91","volume":"92","author":"B. Shults","year":"1997","unstructured":"B. Shults and B. J. Kuipers. Proving properties of continuous systems: qualitative simulation and temporal logic. AI Journal, 92:91\u2013129, 1997.","journal-title":"AI Journal"},{"key":"19_CR22","unstructured":"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 ."},{"key":"19_CR23","unstructured":"A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, second edition, 1948."},{"key":"19_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2002","unstructured":"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\u2013478. Springer Verlag, 2002."}],"container-title":["Lecture Notes in Computer Science","Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36580-X_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T16:16:17Z","timestamp":1557072977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36580-X_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540009139","9783540365808"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-36580-x_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}