{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T08:38:41Z","timestamp":1769071121812,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664598","type":"print"},{"value":"9783540482949","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48294-6_22","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:16:02Z","timestamp":1186172162000},"page":"330-354","source":"Crossref","is-referenced-by-count":69,"title":["Model-Checking"],"prefix":"10.1007","author":[{"given":"Markus","family":"M\u00fcller-Olm","sequence":"first","affiliation":[]},{"given":"David","family":"Schmidt","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,10,1]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","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. Theoretical Computer Science 126 (1994) 183\u2013235.","journal-title":"Theoretical Computer Science"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"H. Andersen, C. Stirling, and G. Winskel, A compositional proof system for the modal mu-calculus. In Proc. 9th LICS. IEEE Computer Society Press, 1994.","DOI":"10.7146\/brics.v1i34.21609"},{"key":"22_CR3","unstructured":"G. Birkhoff, Lattice Theory, 3d edition. Amer. Math. Soc., 1967."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"R. Bryant, Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computation, 8(35), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"22_CR5","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"R. Bull","year":"1994","unstructured":"R. Bull and K. Segerberg, Basic Modal Logic. In Handbook of Philosophical Logic, Vol. 2, D. Gabbay and F. Guenther, eds., Kluwer, Dortdrecht, 1994, pp. 1\u201388."},{"key":"22_CR6","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, Symbolic model checking: 1020 states and beyond. In Proc. 5th LICS. IEEE Computer Society Press, 1990."},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, F. Moller, and B. Steffen, Verification on infinite structures. In Handbook of Process algebra, Jan Bergstra, Alban Ponse, and Scott Smolka, eds., Elsevier, to appear.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"O. Burkart and J. Esparza, More infinite results. Electronic Notes in Theoretical Computer Science 6 (1997). URL: http:\/\/www.elsevier.nl\/locate\/entcs\/volume6.html .","DOI":"10.1016\/S1571-0661(05)80680-2"},{"key":"22_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-56922-7_21","volume-title":"Computer Aided Verification (CAV\u201993)","author":"K. \u010cer\u0101ns","year":"1993","unstructured":"K. \u010cer\u0101ns, J.C. Godesken, and K.G. Larsen, Timed modal specification\u2013theory and tools. In Computer Aided Verification (CAV\u201993), C. Courcoubetis, ed., Lecture Notes in Computer Science 697, Springer, 1993, pp. 253\u2013267."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"E. Clarke, D. Long, and K. McMillan, Compositional model checking. In Proc. 4th LICS. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1996","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 (1996) 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"A Decade of Concurrency: Reflections and Perspectives","author":"E. M. Clarke","year":"1993","unstructured":"E. M. Clarke, O. Grumberg, and D. Long, Verification tools for finite-state concurrent systems. In A Decade of Concurrency: Reflections and Perspectives, J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds., Lecture Notes in Computer Science 803, Springer, 1993, pp. 124\u2013175."},{"key":"22_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/BFb0084777","volume-title":"Computer Aided Verification (CAV\u201992)","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland, M. Klein, and B. Steffen, Faster model checking for the modal mu-calculus. In Computer Aided Verification (CAV\u201992), G. v. Bochmann and D. K. Probst, eds., Lecture Notes in Computer Science 663, 1992, pp. 410\u2013422."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, Pragmatics of Model Checking. Software Tools for Technology Transfer 2(3), 1999.","DOI":"10.1007\/s100090050030"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings 4th POPL, Los Angeles, California, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"22_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-02962-6","volume-title":"Logic and Structure","author":"D. Dalen van","year":"1994","unstructured":"D. van Dalen, Logic and Structure, 3d edition. Springer, Berlin, 1994.","edition":"3d edition"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, Temporal and modal logic. In Handbook of Theoretical Computer Science, Vol B. J. van Leeuwen, ed., Elsevier Science Publishers B.V., 1990, pp. 995\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"22_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/3-540-55179-4_20","volume-title":"Computer Aided Verification (CAV\u201991)","author":"R. Enders","year":"1992","unstructured":"R. Enders, T. Filkorn, and D. Taubner, Generating BDDs for symbolic model checking in CCS. In Computer Aided Verification (CAV\u201991), K. G. Larsen and A. Skou, eds., Lecture Notes in Computer Science 575, Springer, pp. 203\u2013213."},{"key":"22_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume-title":"Computer Aided Verification (CAV\u201991)","author":"P. Godefroid","year":"1992","unstructured":"P. Godefroid and P. Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties. n Computer Aided Verification (CAV\u201991), K. G. Larsen and A. Skou, eds., Lecture Notes in Computer Science 575, Springer, pp. 332\u2013342."},{"key":"22_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Computer Aided Verification (CAV\u201993)","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and D. Pirottin, Refining dependencies improves partial-order verification methods. In Computer Aided Verification (CAV\u201993), C. Courcoubetis, ed., Lecture Notes in Computer Science 697, Springer pp. 438\u2013449."},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"G. Gr\u00e4tzer, General Lattice Theory. Birkh\u00e4user Verlag, 1978.","DOI":"10.1007\/978-3-0348-7633-9"},{"key":"22_CR22","unstructured":"S. Graf and C. Loiseaux, Program Verification using Compositional Abstraction. In Proceedings FASE\/TAPSOFT, 1993."},{"key":"22_CR23","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"S. Graf, B. Steffen, and G. L\u00fcttgen, Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computing, 8:607\u2013616, 1996.","journal-title":"Formal Aspects of Computing"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. C. B. Hennessy","year":"1985","unstructured":"M. C. B. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32 (1985) 137\u2013161.","journal-title":"Journal of the ACM"},{"key":"22_CR25","unstructured":"G. Hughes and M. Cresswell. An Introduction to Modal Logic. Methuen, London, 1972."},{"key":"22_CR26","volume-title":"Introduction to Metamathematics","author":"S. Kleene","year":"1952","unstructured":"S. Kleene, Introduction to Metamathematics. D. van Nostrand, Princeton, 1952."},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen, Results on the propositional mu-calculus, Theoretical Computer Science, 27 (1983) 333\u2013354.","journal-title":"Theoretical Computer Science"},{"key":"22_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"Kripke, S. A completeness theorem in modal logic. J. Symbolic Logic 24 (1959) 1\u201314.","journal-title":"J. Symbolic Logic"},{"key":"22_CR29","first-page":"83","volume":"16","author":"S. Kripke","year":"1953","unstructured":"Kripke, S. Semantical considerations on modal logic. Acta Philosophica Fennica 16 (1953) 83\u201394.","journal-title":"Acta Philosophica Fennica"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"K. G. Larsen, B. Steffen, and C. Weise. A constraint oriented proof methodology based on modal transition systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201995), E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, eds, Lecture Notes of Computer Science 1019, Springer, pp. 17\u201340.","DOI":"10.1007\/3-540-60630-0_2"},{"key":"22_CR31","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/0020-0190(82)90065-5","volume":"14","author":"J.-L. Lassez","year":"1982","unstructured":"J.-L. Lassez, V. L. Nguyen, and E. A. Sonenberg, Fixed point theorems and semantics: A folk tale. Information Processing Letters 14 (1982) 112\u2013116.","journal-title":"Information Processing Letters"},{"key":"22_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-58179-0_66","volume-title":"Computer Aided Verification (CAV\u201994)","author":"D. E. Long","year":"1994","unstructured":"D. E. Long, A. Browne, E. M. Clarke, S. Jha, and W. R. Marrero, An improved algorithm for the evaluation of fixpoint expressions. In Computer Aided Verification (CAV\u201994), David L. Dill, ed., Lecture Notes in Computer Science 818, Springer pp. 338\u2013349."},{"key":"22_CR33","unstructured":"Robin Milner, Communication and Concurrency. Prentice Hall, 1989."},{"key":"22_CR34","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 5th Internat. Symp. on Programming","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR. In Proc. 5th Internat. Symp. on Programming, M. Dezani-Ciancaglini and U. Montanari, eds., Lecture Notes in Computer Science 137, Springer, 1982."},{"key":"22_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis (SAS\u201998)","author":"D. Schmidt","year":"1998","unstructured":"D. Schmidt and B. Steffen, Program analysis as model checking of abstract interpretations. In Static Analysis (SAS\u201998), Giorgio Levi, ed., Lecture Notes in Computer Science 1503, Springer, 1998, 351\u2013380."},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"C. Stirling, Modal and temporal logics. In Handbook of Logic in Computer Science S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, eds., Clarendon Press, 1992, pp 477\u2013563.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"22_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-50939-9_144","volume-title":"Proc. TAPSOFT\u2019 89","author":"C. Stirling","year":"1989","unstructured":"C. Stirling and D. Walker, Local model checking in the modal mu-calculus, Proc. TAPSOFT\u2019 89, J. Diaz and F. Orejas, eds., Lecture Notes in Computer Science 351, Springer, 1989, pp. 369\u2013383."},{"key":"22_CR38","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/s100090050006","volume":"1","author":"Special section on timed and hybrid systems","year":"1997","unstructured":"Special section on timed and hybrid systems, Software Tools for Technology Transfer 1 (1997) 64\u2013153.","journal-title":"Software Tools for Technology Transfer"},{"key":"22_CR39","first-page":"3","volume":"2","author":"Special section on model checking","year":"1999","unstructured":"Special section on model checking, Software Tools for Technology Transfer 2\/3 (1999).","journal-title":"Software Tools for Technology Transfer"},{"key":"22_CR40","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski, A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics 5 (1955) 285\u2013309.","journal-title":"Pacific Journal of Mathematics"},{"key":"22_CR41","doi-asserted-by":"crossref","unstructured":"W. Thomas, Automata on infinite objects. In Handbook of Theoretical Computer Science, Vol B. J. van Leeuwen, ed., Elsevier Science Publishers B.V., 1990, pp. 133\u2013191.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"22_CR42","doi-asserted-by":"publisher","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 (1994) 1\u201337.","journal-title":"Information and Computation"},{"key":"22_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Computer Aided Verification (CAV\u201993)","author":"A. Valmari","year":"1993","unstructured":"A. Valmari, On-the-fly verification with stubborn sets. In Computer Aided Verification (CAV\u201993), C. Courcoubetis, ed., Lecture Notes in Computer Science 697, Springer, pp. 397\u2013408."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48294-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T07:30:35Z","timestamp":1708155035000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48294-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664598","9783540482949"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/3-540-48294-6_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}