{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:31:34Z","timestamp":1754487094109},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_52","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:36:12Z","timestamp":1330259772000},"page":"211-224","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Local model checking for real-time systems"],"prefix":"10.1007","author":[{"given":"Oleg V.","family":"Sokolsky","sequence":"first","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"18_CR1","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. \u201cAn Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness\u201d. In Proceedings of IEEE Real-Time Symposium. IEEE Computer Society Press, 1992."},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. \u201cModel-Checking for Real-Time Systems\u201d. Information and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"18_CR3","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. \u201cMinimization of Timed Transition Systems\u201d. In Proceedings of CONCUR'92. LNCS 630, 1992."},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and D. L. Dill. \u201cThe Theory of Timed Automata\u201d. Theoretical Comput. Sci., 126(2), 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"18_CR5","unstructured":"R. Alur. Techniques for Authomatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. \u201cModel Checking and Boolean Graphs\u201d. Theoretical Comput. Sci., 126(1), 1994.","DOI":"10.1016\/0304-3975(94)90266-6"},{"issue":"3","key":"18_CR7","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. \u201cMinimal State Graph Generation\u201d. Sci. Comput. Programming, 18(3):247\u2013269, 1992.","journal-title":"Sci. Comput. Programming"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"O. Bernholz, M. Y. Vardi, and P. Wolper. \u201cAn Automata-Thoeretic Approach to Branching-Time Model Checking\u201d. In Proceedings of CAV'94. LNCS 818, 1994.","DOI":"10.1007\/3-540-58179-0_50"},{"issue":"1","key":"18_CR9","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P. Cousot","year":"1979","unstructured":"P. Cousot and R. Cousot. \u201cConstructive Versions of Tarski's Fixed Point Theorems\u201d. Pacific J. Math., 82(1):43\u201357, 1979.","journal-title":"Pacific J. Math."},{"key":"18_CR10","unstructured":"E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. LNCS 131, 1981."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. \u201cAutomatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications\u201d. ACM Trans. Prog. Lang. Syst., 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. N. Gada, P. M. Lewis, S. A. Smolka, O. V. Sokolsky, and S. Zhang. \u201cThe Concurrency Factory \u2014 Practical Tools for Specification, Simulation, Verification and Implementation of Concurrent Systems\u201d. In Proceedings of the DIMACS Workshop on Specification Techniques for Concurrent Systems, Princeton, NJ, 1994.","DOI":"10.1090\/dimacs\/018\/06"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"R. Cleaveland. \u201cTableau-Based Model Checking in the Propositional Mu-Calculus\u201d. Acta Inf., 27, 1990.","DOI":"10.1007\/BF00264284"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. \u201cThe Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems\u201d. ACM TOPLAS, 15(1), 1993.","DOI":"10.1145\/151646.151648"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and B. Steffen. \u201cA Linear-Time Model Checking Algorithm for the Alternation-Free Modal Mu-Calculus\u201d. Formal Methods in System Design, 2, 1993.","DOI":"10.1007\/BF01383878"},{"key":"18_CR16","unstructured":"D. Dill. \u201cTiming Assumptions and Verification of Finite-State Concurrent Systems\u201d. In Proceedings of CAV'89. LNCS 407, 1989."},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, C. S. Jutla, and A. P. Sistla. \u201cOn Model Checking for Fragments of \u03bc-calculus\u201d. In Proceedings of CAV'93. LNCS 697, 1993.","DOI":"10.1007\/3-540-56922-7_32"},{"key":"18_CR18","unstructured":"E. A. Emerson and C.-L. Lei. \u201cEfficient Model Checking in Fragments of the Propositional Mu-Calculus\u201d. In Proceedings LICS '86. IEEE Computer Society Press, 1986."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. \u201cReal-Time and the Mu-Calculus\u201d. In Real-Time: Theory in Practice. LNCS 600, 1991.","DOI":"10.1007\/BFb0031992"},{"key":"18_CR20","unstructured":"U. Holmer, K. G. Larsen, and Y. Wang. \u201cDeciding Properties of Regular Real Timed Processes\u201d. In Proceedings of CAV'91. LNCS 575, 1991."},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. \u201cSymbolic Model Checking for Real-time Systems\u201d. Information and Computation, 111(2), 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"18_CR22","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. \u201cResults on the Propositional Mu-Calculus\u201d. Theoretical Comput. Sci., 27:333\u2013354, 1983.","journal-title":"Theoretical Comput. Sci."},{"key":"18_CR23","unstructured":"K. G. Larsen. \u201cEfficient Local Correctness Checking\u201d. In Proceedings of CAV'92. LNCS 663, 1992."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. A. Smolka. \u201cIncremental Model Checking in the Modal Mu-Calculus\u201d. In Proceedings of CAV'94. LNCS 818, 1994.","DOI":"10.1007\/3-540-58179-0_67"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. \u201cLocal Model Checking in the Modal Mu-Calculus\u201d. Theoretical Comput. Sci., 89(1), 1991.","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"18_CR26","unstructured":"B. Vergauwen, J. Lewi, I. Avau, and A. Pote. \u201cEfficient Computation of Nested Fix-Points, with applications to Model Checking\u201d. In Proceedings of ICTL'94, 1st Intl. Conference on Temporal Logic. LNCS 827, 1994."},{"key":"18_CR27","unstructured":"M. Y. Vardi and P. Wolper. \u201cAn Automata-Theoretic Approach to Automatic Program Verification\u201d. In Proceedings of LICS'86, pages 322\u2013331. IEEE Computer Society Press, 1986."},{"key":"18_CR28","unstructured":"Y. Wang. A Calculus of Real Time Systems. PhD thesis, Chalmers University of Technology, 1991."},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"M. Yannakakis and D. Lee. \u201cAn Efficient Algorithm for Minimizing Real-Time Transition Systems\u201d. In Proceedings of CAV'93. LNCS 697, 1993.","DOI":"10.1007\/3-540-56922-7_18"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:32:33Z","timestamp":1578508353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_52"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}