{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T00:49:58Z","timestamp":1791420598413,"version":"4.3.3"},"publisher-location":"Boston","reference-count":9,"publisher":"Kluwer Academic Publishers","isbn-type":[{"value":"1402081480","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8149-9_5","type":"book-chapter","created":{"date-parts":[[2006,2,22]],"date-time":"2006-02-22T14:53:33Z","timestamp":1140620013000},"page":"43-52","source":"Crossref","is-referenced-by-count":6,"title":["Modeling and Verification of Hybrid Systems Based on Equations"],"prefix":"10.1007","author":[{"given":"Kazuhiro","family":"Ogata","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daigo","family":"Yamagishi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Takahiro","family":"Seino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"AMAST Series in Computing","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R. and Futatsugi, K. (1998). CafeOBJ Report, volume 6 of AMAST Series in Computing. World Scientific, Singapore."},{"key":"5_CR2","volume-title":"Texts and Monographs in Computer Science","author":"D. Gries","year":"1993","unstructured":"Gries, D. and Schneider, F. B. (1993). A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, NY."},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1007\/s002360050177","volume":"36","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Manna, Z., and Pnueli, A. (2000). Verification of clocked and hybrid systems. Acta Informatica, 36:837\u2013912.","journal-title":"Acta Informatica"},{"key":"5_CR4","first-page":"77","volume":"736","author":"L. Lamport","year":"1993","unstructured":"Lamport, L. (1993). Hybrid systems in TLA+. In Hybrid Systems, volume 736 of LNCS, pages 77\u2013102. Springer.","journal-title":"LNCS"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N. Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., and Vaandraager, F. (2003). Hybrid I\/O automata. Information and Computation, 185:105\u2013157.","journal-title":"Information and Computation"},{"key":"5_CR6","first-page":"441","volume":"2609","author":"K. Ogata","year":"2003","unstructured":"Ogata, K. and Futatsugi, K. (2003a). Formal analysis of the iKP electronic payment protocols. In ISSS 2002, volume 2609 of LNCS, pages 441\u2013460. Springer.","journal-title":"LNCS"},{"key":"5_CR7","first-page":"238","volume":"2575","author":"K. Ogata","year":"2003","unstructured":"Ogata, K. and Futatsugi, K. (2003b). Formal verification of the Horn-Preneel micropayment protocol. In VMCAI 2003, volume 2575 of LNCS, pages 238\u2013252. Springer.","journal-title":"LNCS"},{"key":"5_CR8","first-page":"170","volume":"2884","author":"K. Ogata","year":"2003","unstructured":"Ogata, K. and Futatsugi, K. (2003c). Proof scores in the OTS\/CafeOBJ method. In FMOODS 2003, volume 2884 of LNCS, pages 170\u2013184. Springer.","journal-title":"LNCS"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P. C. and Meseguer, J. (2000). Real-Time Maude: A tool for simulating and analyzing real-time and hybrid systems. In WRLA 2000, volume 36 of ENTCS. Elsevier.","DOI":"10.1016\/S1571-0661(05)80134-3"}],"container-title":["IFIP International Federation for Information Processing","Design Methods and Applications for Distributed Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8149-9_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T15:29:37Z","timestamp":1683386977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8149-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081480"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8149-9_5","relation":{},"subject":[]}}