{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215110,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426738"},{"type":"electronic","value":"9783540454496"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45449-7_2","type":"book-chapter","created":{"date-parts":[[2007,9,21]],"date-time":"2007-09-21T15:54:26Z","timestamp":1190390066000},"page":"14-31","source":"Crossref","is-referenced-by-count":43,"title":["Hierarchical Hybrid Modeling of Embedded Systems"],"prefix":"10.1007","author":[{"given":"R.","family":"Alur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Esposito","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Fierro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Hur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I.","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Mishra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Pappas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,27]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"key":"2_CR2","unstructured":"R. Alur, A. Das, J. Esposito, R. Fierro, Y. Hur, G. Grudic, V. Kumar, I. Lee, J. P. Ostrowski, G. Pappas, J. Southall, J. Spletzer, and C. J. Taylor. A framework and architecture for multirobot coordination. In Proc. ISER00, Seventh Intl. Symp. on Experimental Robotics, pages 289\u2013299, 2000."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, L. de Alfaro, R. Grosu, T.A. Henzinger, M. Kang, R. Majumdar, F. Mang, C.M. Kirsch, and B.Y. Wang. Mocha: A model checking tool that exploits design structure. In Proc. 23rd Intl. Conf. on Software Engineering, pages 835\u2013836, 2001.","DOI":"10.1109\/ICSE.2001.919196"},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","first-page":"33","volume-title":"Hybrid Systems: Computation and Control","author":"A. R","year":"2001","unstructured":"R. Alur, R. Grosu, I. Lee, and O. Sokolsky. Compositional refinement for hierarchical hybrid systems. In Hybrid Systems: Computation and Control, LNCS 2034, pages 33\u201348, 2001."},{"issue":"7","key":"2_CR5","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"A. R","year":"2000","unstructured":"R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. Discrete abstractions of hybrid systems. Proceedings ofthe IEEE, 88(7):971\u2013984, July 2000.","journal-title":"Proceedings ofthe IEEE"},{"key":"2_CR6","first-page":"888","volume":"887","author":"B. A","year":"2000","unstructured":"A. Balluchi, L. Benvenuti, M. Di Benedetto, C. Pinello, and A. Sangiovanni-Vicentelli. Automotive engine control and hybrid systems: Challenges and opportunities. Proceedings ofthe IEEE, 88(7):888\u2013912, July 2000.","journal-title":"Proceedings ofthe IEEE"},{"key":"2_CR7","unstructured":"G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997."},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Hybrid Systems: Computation and Control","author":"C. A","year":"1999","unstructured":"A. Chutinan and B. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Hybrid Systems: Computation and Control, LNCS 1569, 1999."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154\u2013169, 2000.","DOI":"10.1007\/10722167_15"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"336","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke and R.P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","first-page":"160","volume-title":"Computer Aided Verification, 11th Intl. Conf","author":"D. S","year":"1999","unstructured":"S. Das, D. Dill, and S. Park. Experience with predicate abstraction. In Computer Aided Verification, 11th Intl. Conf., LNCS 1633, pages 160\u2013171, 1999."},{"key":"2_CR12","unstructured":"J. Davis, M. Goel, C. Hylands, B. Kienhuis, E.A. Lee, J. Liu, X. Liu, L. Muliadi, S. Neuendorffer, J. Reekie, N. Smyth, J. Tsay, and Y. Xiong. Overview of the Ptolemy project. Technical Report UCB\/ERL M99\/37, 1999."},{"key":"2_CR13","first-page":"1050","volume":"887","author":"E. S","year":"2000","unstructured":"S. Engell, S. Kowalewski, C. Schulz, and O. Stursberg. Continuous-discrete interactions in chemical processing plants. Proc. ofthe IEEE, 88(7):1050\u20131068, 2000.","journal-title":"Proc. ofthe IEEE"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"J. Esposito and V. Kumar. Efficient dynamic simulation of robotic systems with hierarchy. In Intl. Conf. on Robotics and Automation, pages 2818\u20132823, 2001.","DOI":"10.1109\/ROBOT.2001.933049"},{"key":"2_CR15","series-title":"Lect Notes Comput Sci","first-page":"204","volume-title":"Hybrid Systems: Computation and Control","author":"E. J","year":"2001","unstructured":"J. Esposito, V. Kumar, and G. Pappas. Accurate event detection for simulating hybrid systems. In Hybrid Systems: Computation and Control, LNCS 2034, pages 204\u2013217, 2001."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"R. Fierro, A. Das, V. Kumar, and J. P. Ostrowski. Hybrid control of formations of robots. Proc. Int. Conf. Robot. Automat., pages 157\u2013162, 2001.","DOI":"10.1109\/ROBOT.2001.932546"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"Harel. D","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science ofComputer Programming, 8:231\u2013274, 1987.","journal-title":"Science ofComputer Programming"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"Proc. TACAS\u201995","author":"T.A. Henzinger","year":"1995","unstructured":"T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation. In Proc. TACAS\u201995, LNCS 1019, pages 41\u201371, 1995."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"5","key":"2_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering,23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"G. Lafferriere, G. Pappas, and S. Yovine. Symbolic reachability computation for families of linear vector fields. Journal ofSymb olic Computation, 2001.","DOI":"10.1006\/jsco.2001.0472"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Springer Intl. Journal of Software Tools for Technology Transfer, 1, 1997.","DOI":"10.1007\/s100090050010"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"E.A. Lee. What\u2019s ahead for embedded software. IEEE Computer, pages 18\u201326, September 2000.","DOI":"10.1109\/2.868693"},{"key":"2_CR24","series-title":"Lect Notes Comput Sci","first-page":"496","volume-title":"Hybrid Systems III: Verification and Control","author":"L. N","year":"1996","unstructured":"N. Lynch, R. Segala, F. Vaandrager, and H. Weinberg. Hybrid I\/O automata. In Hybrid Systems III: Verification and Control, LNCS 1066, pages 496\u2013510, 1996."},{"key":"2_CR25","series-title":"Lect Notes Comput Sci","first-page":"447","volume-title":"Real-Time: Theory in Practice, REX Workshop","author":"M. O","year":"1991","unstructured":"O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Real-Time: Theory in Practice, REX Workshop, LNCS 600, pages 447\u2013484, 1991."},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus ofCommunic ating Systems","author":"Milner. R","year":"1980","unstructured":"R. Milner. A Calculus ofCommunic ating Systems. LNCS92, 1980."},{"key":"2_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 9th Intl. Conf. on Computer Aided Verification","author":"G. S","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. 9th Intl. Conf. on Computer Aided Verification, LNCS 1254, 1997."},{"issue":"4","key":"2_CR29","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"T. C","year":"1998","unstructured":"C. Tomlin, G. Pappas, and S. Sastry. Conflict resolution for air traffic management: A study in multi-agent hybrid systems. IEEE Trans. Automatic Control, 43(4):509\u2013521, 1998.","journal-title":"IEEE Trans. Automatic Control"}],"container-title":["Lecture Notes in Computer Science","Embedded Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45449-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T04:16:41Z","timestamp":1737433001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45449-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426738","9783540454496"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-45449-7_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}