{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T23:46:19Z","timestamp":1794354379935,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540789123","type":"print"},{"value":"9783540789130","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78913-0_15","type":"book-chapter","created":{"date-parts":[[2008,4,11]],"date-time":"2008-04-11T08:13:06Z","timestamp":1207901586000},"page":"191-205","source":"Crossref","is-referenced-by-count":2,"title":["Automated Reasoning for Hybrid Systems \u2014 Two Case Studies \u2014"],"prefix":"10.1007","author":[{"given":"Peter","family":"H\u00f6fner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1\u20132","key":"15_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3166\/jancl.16.9-33","volume":"16","author":"K. Aboul-Hosn","year":"2006","unstructured":"Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics\u00a016(1\u20132), 9\u201333 (2006)","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"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 Comp. Sc.\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Comp. Sc."},{"key":"15_CR3","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"issue":"2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comp. Sc.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Comp. Sc."},{"issue":"2-3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/j.tcs.2004.04.019","volume":"335","author":"J.A. Bergstra","year":"2005","unstructured":"Bergstra, J.A., Middleburg, C.A.: Process algebra for hybrid systems. Theoretical Comp. Sc.\u00a0335(2-3), 215\u2013280 (2005)","journal-title":"Theoretical Comp. Sc."},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.biosystems.2004.12.002","volume":"80","author":"K.-H. Cho","year":"2005","unstructured":"Cho, K.-H., Johansson, K.H., Wolkenhauer, O.: A hybrid systems framework for cellular processes. Biosystems\u00a080(3), 273\u2013282 (2005)","journal-title":"Biosystems"},{"key":"15_CR7","volume-title":"Regular Algebra and Finite Machines","author":"J.H. Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Sydney, Australia (1971)"},{"key":"15_CR8","first-page":"167","volume-title":"Conference on Ergonomics of Hybrid Automated Systems I","author":"J.M. Corbett","year":"1988","unstructured":"Corbett, J.M.: Designing hybrid automated manufacturing systems: A european perspective. In: Conference on Ergonomics of Hybrid Automated Systems I, pp. 167\u2013172. Elsevier, Amsterdam (1988)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-3-540-30101-1_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2004","unstructured":"Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO 2003. LNCS, vol.\u00a03188, pp. 77\u2013110. Springer, Heidelberg (2004)"},{"key":"15_CR10","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)","edition":"2"},{"issue":"7","key":"15_CR11","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1109\/5.871305","volume":"88","author":"J.M. Davoren","year":"2000","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proc. of the IEEE\u00a088(7), 985\u20131010 (2000)","journal-title":"Proc. of the IEEE"},{"issue":"4","key":"15_CR12","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comp. Logic\u00a07(4), 798\u2013833 (2006)","journal-title":"ACM Trans. Comp. Logic"},{"key":"15_CR13","first-page":"76","volume-title":"FMCAD 2006","author":"J. Faber","year":"2006","unstructured":"Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the european train control system. In: FMCAD 2006, pp. 76\u201377. IEEE Press, Los Alamitos (2006)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Kemal, M. (ed.) IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278\u2013292. IEEE Press, Los Alamitos (1996): Extended Version: Kemal, M.: Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol.\u00a0170, pp. 265\u2013292. Springer, Heidelberg (2000)","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-48320-9_23","volume-title":"CONCUR\u201999. Concurrency Theory","author":"T.A. Henzinger","year":"1999","unstructured":"Henzinger, T.A., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 320\u2013335. Springer, Heidelberg (1999)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-46419-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Majumdar, R.: Symbolic model checking for rectangular hybrid systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 142\u2013156. Springer, Heidelberg (2000)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/11734673_10","volume-title":"Relational Methods in Computer Science","author":"P. H\u00f6fner","year":"2006","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: Towards an algebra of hybrid systems. In: MacCaull, W., Winter, M., D\u00fcntsch, I. (eds.) RelMiCS 2005. LNCS, vol.\u00a03929, pp. 121\u2013133. Springer, Heidelberg (2006)"},{"key":"15_CR18","unstructured":"H\u00f6fner, P., M\u00f6ller, B.: An algebra of hybrid systems. Technical Report 2007-08, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg (2007)"},{"key":"15_CR19","unstructured":"H\u00f6fner, P., Struth, G.: January 14 (2008), \n                  \n                    http:\/\/www.dcs.shef.ac.uk\/~georg\/ka"},{"key":"15_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"15_CR21","series-title":"ENTCS","volume-title":"Refine 2007","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Can refinement be automated? In: Boiten, E., Derrick, J., Smith, G. (eds.) Refine 2007. ENTCS, Elsevier, Amsterdam (to appear, 2007)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","first-page":"179","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 179\u2013190. Springer, Heidelberg (2004)"},{"issue":"3","key":"15_CR23","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. Trans. Prog. Languages and Systems\u00a019(3), 427\u2013443 (1997)","journal-title":"Trans. Prog. Languages and Systems"},{"key":"15_CR24","unstructured":"McCune, W.: Prover9 and Mace4, \n                  \n                    http:\/\/www.cs.unm.edu\/~mccune\/prover9"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.scico.2006.01.010","volume":"65","author":"B. M\u00f6ller","year":"2007","unstructured":"M\u00f6ller, B.: Kleene getting lazy. Sc. Comp. Prog.\u00a065, 195\u2013214 (2007)","journal-title":"Sc. Comp. Prog."},{"issue":"1","key":"15_CR26","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1076\/1387-3954(200003)6:1;1-Q;FT071","volume":"6","author":"O. M\u00fcller","year":"2000","unstructured":"M\u00fcller, O., Stauner, T.: Modelling and verification using linear hybrid automata \u2013 A case study. Math. and Comp. Modelling of Dynamical Systems\u00a06(1), 71\u201389 (2000)","journal-title":"Math. and Comp. Modelling of Dynamical Systems"},{"key":"15_CR27","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR: FLoC 2006, CEUR Workshop Proceedings, vol.\u00a0192, pp. 18\u201333 (2006)"},{"key":"15_CR28","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-36280-0_19","volume-title":"Relational Methods in Computer Science","author":"G. Struth","year":"2002","unstructured":"Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol.\u00a02561, pp. 276\u2013290. Springer, Heidelberg (2002)"},{"key":"15_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Yury, P.: SRASS-A semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Relations and Kleene Algebra in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78913-0_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:36Z","timestamp":1619507016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78913-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540789123","9783540789130"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78913-0_15","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-78913-0","asserted-by":"object"}]},"subject":[]}}