{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:49Z","timestamp":1725664009492},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584681"},{"type":"electronic","value":"9783540489849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58468-4_157","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:14:43Z","timestamp":1330254883000},"page":"1-18","source":"Crossref","is-referenced-by-count":3,"title":["Hybrid verification by exploiting the environment"],"prefix":"10.1007","author":[{"given":"Limor","family":"Fix","sequence":"first","affiliation":[]},{"given":"Fred B.","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. An old-fashioned recipe for real-time. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Real-time: Theory in Practice, pages 1\u201317. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0031985"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, T.A. Henzinger, and P-H. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 209\u2013229. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_30"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In 16th Annual ACM Aymposium on Theory of Computing, pages 51\u201363, 1984.","DOI":"10.1145\/800057.808665"},{"issue":"5","key":"1_CR4","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, 1991.","journal-title":"Information Processing Letters"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Z. Chaochen, A.P. Ravn, and M.R. Hansen. An extended duration calculus for hybrid real-time systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 36\u201359. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_23"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings 4th IEEE Symposium on Logic in Computer Science, pages 353\u2013362, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg (eds.). Real-Time: Theory in Practice. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0031984"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"E.A. Emerson. Alternative semantics for temporal logics. Theoretical computer science, 26:121\u2013130, 1983.","journal-title":"Theoretical computer science"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"L. Fix, N. Francez, and O. Grumberg. Program composition via unification. In 19th International Colloquium On Automata, Languages and Programming, pages 672\u2013684. Lecture Notes in Computer Science Vol. 623, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55719-9_113"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"L. Fix and F.B. Schneider. Reasoning about programs by exploiting the environment. To appear, 21st International Colloquium On Automata, Languages and Programming.","DOI":"10.21236\/ADA275852"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. In CONCUR'91, 2nd International Conference on Concurrency Theory, pages 250\u2013263. Lecture Notes in Computer Science Vol. 527, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, Z. Manna, and A. Pnueli. Towards refining temporal specifications into hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 60\u201376. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_24"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"J. Hooman. A compositional approach to the design of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 121\u2013148. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_27"},{"key":"1_CR14","unstructured":"C.B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, editor, Information Processing'83, pages 321\u2013332. Elsevier Science Publishers, 1983."},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engineering, 3:125\u2013143, 1977.","journal-title":"IEEE Trans. Software Engineering"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"L. Lamport. The hoare logic of concurrent programs. Acta Informatica, 14, 1980.","DOI":"10.1007\/BF00289062"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"L. Lamport. Hybrid systems in tla +. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 77\u2013102. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_25"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop, Real-time: Theory in practice, pages 447\u2013484. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032003"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Verifying hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, pages 4\u201335. Lecture Notes in Computer Science Vol. 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_22"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"K. Marzullo, F.B. Schneider, and N. Budhiraja. Derivation of sequential real-time, process-control programs. In A. Van Tilborg and G. Koob, editors, Foundations of Real-Time Computing, pages 39\u201354. Kluwer Academic Publishers, 1991.","DOI":"10.21236\/ADA238877"},{"issue":"4","key":"1_CR21","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"SE-7","author":"J. Misra","year":"1981","unstructured":"J. Misra and M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417\u2013426, 1981.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"X. Nicollin, J. Sifakis, and S. Yovine. From atp to timed graphs and hybrid systems. In J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, REX Workshop, Real-time: Theory in practice, pages 549\u2013572. Lecture Notes in Computer Science Vol. 600, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032007"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about program. In K.R. Apt, editor, Logics and models of concurrent systems, pages 123\u2013144. NATO ASI Series, Vol. F13, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"1_CR24","unstructured":"F.B. Schneider. Designing real-time systems (that really work!). Invited lecture at Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Warwick, England, Sept. 1988."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58468-4_157.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:21:41Z","timestamp":1605630101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58468-4_157"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584681","9783540489849"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-58468-4_157","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}