{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,14]],"date-time":"2025-04-14T04:26:29Z","timestamp":1744604789682},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616047"},{"type":"electronic","value":"9783540706250"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61604-7_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:03:05Z","timestamp":1330275785000},"page":"514-529","source":"Crossref","is-referenced-by-count":23,"title":["A space-efficient on-the-fly algorithm for real-time model checking"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"1","key":"30_CR1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, May 1993.","journal-title":"Information and Computation"},{"issue":"2","key":"30_CR2","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. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013236, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"30_CR3","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"R. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116\u2013146, 1996.","journal-title":"Journal of the ACM"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74\u2013106. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0031988"},{"issue":"1","key":"30_CR5","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur and T. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35\u201377, May 1993.","journal-title":"Information and Computation"},{"issue":"1","key":"30_CR6","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181\u2013204, 1994.","journal-title":"Journal of the ACM"},{"key":"30_CR7","unstructured":"R. Alur. Techniques for Automatic Verification of Real-time Systems. PhD thesis, Stanford University, 1991."},{"key":"30_CR8","first-page":"142","volume-title":"volume 818 of Lecture Notes in Computer Science","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branchingtime model checking. In D. L. Dill, editor, Computer Aided Verification, Proc. 6th Int. Conference, volume 818 of Lecture Notes in Computer Science, pages 142\u2013155, Stanford, June 1994. Springer-Verlag."},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer-Verlag, 1981.","DOI":"10.1007\/BFb0025774"},{"issue":"2","key":"30_CR10","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"30_CR11","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Real time and the \u039c-calculus. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 176\u2013194. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0031992"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 136\u2013145. Springer-Verlag, 1990.","DOI":"10.1007\/BFb0023727"},{"key":"30_CR14","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00121127","volume":"1","author":"J.-C. Fernandez","year":"1992","unstructured":"J.-C. Fernandez, L. Mounier, C. Jard, and T. Jeron. On-the-fly verification of finite transition systems. Formal Methods in System Design, 1:251\u2013273, 1992.","journal-title":"Formal Methods in System Design"},{"key":"30_CR15","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, pages 408\u2013422, Philadelphia, August 1995.","DOI":"10.1007\/3-540-60218-6_31"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d \u2014 on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174\u2013185, January 1980.","DOI":"10.1145\/567446.567463"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"F. Laroussinie and K. G. Larsen. Compositional model checking of real time systems. In Proc. 6th Conferance on Concurrency Theory, pages 27\u201341, Philadelphia, August 1995.","DOI":"10.1007\/3-540-60218-6_3"},{"key":"30_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992."},{"key":"30_CR20","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16761-7_77"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137, pages 337\u2013351. Springer-Verlag, Lecture Notes in Computer Science, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"30_CR24","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of prepositional linear temporal logic. J. ACM, 32:733\u2013749, 1985.","journal-title":"J. ACM"},{"key":"30_CR25","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-60045-0_52","volume":"939","author":"O.V. Sokolsky","year":"1995","unstructured":"O.V. Sokolsky and S.A. Smolka. Local model checking for real-time systems. In Computer Aided Verification, Proc. 7th Int. Workshop, Lecture Notes in Computer Science 939, pages 211\u2013224, Liege, July 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proc. 15th Col. on Trees in Algebra and Programming. Lecture Notes in Computer Science, 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"key":"30_CR27","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 165\u2013191, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"issue":"1","key":"30_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"30_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-56922-7_18","volume-title":"volume 697 of Lecture Notes in Computer Science 697","author":"M. Yannakakis","year":"1993","unstructured":"M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In C. Courcoubetis, editor, Computer Aided Verification, Proc. 5th Int. Workshop, volume 697 of Lecture Notes in Computer Science 697, pages 210\u2013224, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","CONCUR '96: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61604-7_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:51:22Z","timestamp":1640929882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61604-7_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616047","9783540706250"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-61604-7_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}