{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T15:47:23Z","timestamp":1743349643165},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651932"},{"type":"electronic","value":"9783540494980"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-65193-4_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:42:32Z","timestamp":1330299752000},"page":"4-73","source":"Crossref","is-referenced-by-count":4,"title":["Verification of clocked and hybrid systems"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kestent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D.L. Dill. A theory of timed automata. Theor. Comp. Sci., 126:183\u2013235, 1994.","journal-title":"Theor. Comp. Sci."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. A really temporal logic. In Proc. 30th IEEE Symp. Found. of Comp. Sci., pages 164\u2013169, 1989.","DOI":"10.1109\/SFCS.1989.63473"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. Logics and models of real time: A survey. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d, volume 600 of Lect. Notes in Comp. Sci., pages 74\u2013106. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0031988"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Real-time system = discrete system + clock variables. In T. Rus and C. Rattray, editors, Theories and Experiences for Real-time System Development, AMAST Series in Computing 2, pages 1\u201329. World Scientific, 1994.","DOI":"10.1142\/9789812831583_0001"},{"issue":"5","key":"2_CR5","doi-asserted-by":"crossref","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"M. Abadi and L. Lamport. An old-fashioned recipe for real time. ACM Trans. Prog. Lang. Sys., 16(5):1543\u20131571, 1994.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"2_CR6","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207\u2013226, 1983.","journal-title":"Acta Informatica"},{"key":"2_CR7","unstructured":"[BBC+95] N. Bj\u00f8rner, I.A. Browne, E. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User's Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"N.S. Biorner, Z. Manna, H.B. Sipma, and T.E. Uribe. Deductive verification of real-time systems using STeP. In 4th Intl. AMAST Workshop on Real-Time Systems, volume 1231 of Lect. Notes in Comp. Sci., pages 22\u201343. Springer-Verlag, May 1997.","DOI":"10.1007\/3-540-63010-4_3"},{"key":"2_CR9","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comp. Prog., 2:241\u2013266, 1982.","journal-title":"Sci. Comp. Prog."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"L. Fix and O. Grumberg. Verification of temporal properties. to appear in Logic and Computation, 1995.","DOI":"10.21236\/ADA278869"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comp. Prog., 8:231\u2013274, 1987.","journal-title":"Sci. Comp. Prog."},{"issue":"3","key":"2_CR12","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0020-0190(92)90005-G","volume":"43","author":"T.A. Henzinger","year":"1992","unstructured":"T.A. Henzinger. Sooner is safer than later. Info. Proc. Lett., 43(3):135\u2013142, 1992.","journal-title":"Info. Proc. Lett."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HYTECH. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Aarhus, Denmark, 1995. To appear.","DOI":"10.1007\/3-540-60630-0_3"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger and P.W. Kopke. Verification methods for the divergent runs of clock systems. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 351\u2013372. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58468-4_173"},{"issue":"2","key":"2_CR15","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1006\/inco.1994.1060","volume":"112","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for timed transition systems. Inf. and Comp., 112(2):273\u2013337, 1994.","journal-title":"Inf. and Comp."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"R. Koymans and W.-P. de Roever. Examples of a real-time temporal logic specifications. In B.D. Denvir, W.T. Harwood, M.I. Jackson, and M.J. Wray, editors, The Analysis of Concurrent Systems, volume 207 of Lect. Notes in Comp. Sci., pages 231\u2013252. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-16047-7_50"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Verifying clocked transition systems. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, volume 1066 of Lect. Notes in Comp. Sci., pages 13\u201340. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0020933"},{"issue":"4","key":"2_CR18","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"R. Koymans. Specifying real-time properties with metric temporal logic. Real-time Systems, 2(4):255\u2013299, 1990.","journal-title":"Real-time Systems"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"R. Koymans, J. Vytopyl, and W.-P. de Roever. Real-time programming and asynchronous message passing. In Proc. 2nd ACM Symp. Princ. of Dist. Comp., pages 187\u2013197, 1983.","DOI":"10.1145\/800221.806721"},{"key":"2_CR20","unstructured":"L. Lamport. Proving possibiity properties. Technical Report 137, Digital Equipment Corporation, Systems Research Center, Palo Alto, July 1995."},{"key":"2_CR21","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, Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d, volume 600 of Lect. Notes in Comp. Sci., pages 447\u2013484. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032003"},{"issue":"1","key":"2_CR22","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97\u2013130, 1991.","journal-title":"Theor. Comp. Sci."},{"key":"2_CR23","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"2_CR24","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609\u2013678, 1993.","journal-title":"Acta Informatica"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Verifying hybrid systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lect. Notes in Comp. Sci., pages 4\u201335. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_22"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal verification diagrams. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Comp. Sci., pages 726\u2013765. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-57887-0_123"},{"key":"2_CR27","unstructured":"Z. Manna and A. Pnueli. Clocked transition systems. In Logic and Software Workshop, August 1995. Beijing, China."},{"key":"2_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Pnueli. Temporal Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli.Temporal Verification of Reactive Pnueli. Temporal Safety. Springer-Verlag, New York, 1995."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"F. Moller and C. Tofts. A temporal calculus of communicating systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of Concur'90, volume 458 of Lect. Notes in Comp. Sci., pages 401\u2013415. Springer-Verlag, 1990.","DOI":"10.1007\/BFb0039073"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lect. Notes in Comp. Sci., pages 149\u2013178. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_28"},{"key":"2_CR31","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, Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d, volume 600 of Lect. Notes in Comp. Sci., pages 549\u2013572. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032007"},{"key":"2_CR32","volume-title":"Advanced Software Development Series","author":"J.S. Ostroff","year":"1990","unstructured":"J.S. Ostroff. Temporal Logic of Real-Time Systems. Advanced Software Development Series. Research Studies Press (John Wiley & Sons), Taunton, England, 1990."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"F. B. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop \u201cReal-Time: Theory in Practice\u201d, volume 600 of Lect. Notes in Comp. Sci., pages 618\u201339. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032010"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"J. Sifakis. An overview and synthesis on timed process algebra. In K.G. Larsen and A. Skou, editors, 3rd Computer Aided Verification Workshop, volume 575 of Lect. Notes in Comp. Sci., pages 376\u2013398. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55179-4_36"}],"container-title":["Lecture Notes in Computer Science","Lectures on Embedded Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-65193-4_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:20:47Z","timestamp":1605648047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-65193-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651932","9783540494980"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-65193-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}