{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:40:12Z","timestamp":1737060012521,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430759"},{"type":"electronic","value":"9783540455752"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45575-2_6","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T01:30:22Z","timestamp":1180575022000},"page":"39-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Expressive and Model Checking Power of Propositional Program Logics"],"prefix":"10.1007","author":[{"given":"Nikolai V.","family":"Shilov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kwang","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,18]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Baldamus M, Schneider K., Wenz M., Ziller R. Can American Checkers be Solved by Means of Symbolic Model Checking? Electronic Notes in Theoretical Computer Science, v.43, http:\/\/www.elsevier.nl\/gej-ng\/31\/29\/23\/show\/Products\/notes\/","DOI":"10.1016\/S1571-0661(04)80892-2"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E., Gr\u00e4del E., Gurevich Y. The Classical Decision Problem. Springer, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"6_CR3","first-page":"1","volume":"II","author":"R.A. Bull","year":"1984","unstructured":"Bull R.A., Segerberg K. Basic Modal Logic. Handbook of Philosophical Logic, v.II, Reidel Publishing Company, 1984 (1-st ed.), Kluwer Academic Publishers, 1994 (2-nd ed.), p.1\u201388.","journal-title":"Handbook of Philosophical Logic"},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. Symbolic Model Checking: 10 20 states and beyond. Information and Computation, v.98, n.2, 1992, p.142\u2013170.","journal-title":"Information and Computation"},{"key":"6_CR5","unstructured":"Clarke E.M., Grumberg O., Peled D. Model Checking. MIT Press, 1999."},{"key":"6_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/3-540-56496-9_32","volume-title":"Faster Model-Checking for Mu-Calculus","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland R., Klain M., Steffen B. Faster Model-Checking for Mu-Calculus. Lecture Notes in Computer Science, v.663, 1993, p.410\u2013422."},{"key":"6_CR7","first-page":"995","volume":"B","author":"E.A. Emerson","year":"1990","unstructured":"Emerson E.A. Temporal and Modal Logic. Handbook of Theoretical Computer Science, v.B, Elsevier and The MIT Press, 1990, 995\u20131072.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. MIT Press, 1995.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"6_CR9","unstructured":"Immerman N Descriptive Complexity: a Logician\u2019s Approach to Computation. Notices of the American Mathematical Society, v.42, n.10, p.1127\u20131133."},{"issue":"3","key":"6_CR10","first-page":"333","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen D. Results on the Propositional Mu-Calculus. Theoretical Computer Science, v.27, n.3, 1983, p.333\u2013354.","journal-title":"Results on the Propositional Mu-Calculus"},{"key":"6_CR11","first-page":"789","volume":"B","author":"D. Kozen","year":"1990","unstructured":"Kozen D., Tiuryn J. Logics of Programs. Handbook of Theoretical Computer Science, v.B, Elsevier and The MIT Press, 1990, 789\u2013840.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin M.O. Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc., v.141, 1969, p.1\u201335.","journal-title":"Trans. Amer. Math. Soc."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Rabin M.O. Decidable Theories. in Handbook of Mathematical Logic, ed. Barwise J. and Keisler H.J., North-Holland Pub. Co., 1977, 595\u2013630.","DOI":"10.1016\/S0049-237X(08)71116-9"},{"key":"6_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/BFb0023896","volume-title":"On expressive power of Modal Logic on Trees","author":"H. Schlinglo","year":"1992","unstructured":"Schlinglo. H. On expressive power of Modal Logic on Trees. LNCS, v.620, 1992, p.441\u2013450."},{"key":"6_CR15","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1093\/oso\/9780198537618.003.0005","volume":"2","author":"C. Stirling","year":"1992","unstructured":"Stirling C. Modal and Temporal Logics. Handbook of Logic in Computer Science, v.2, Claredon Press, 1992, p.477\u2013563.","journal-title":"Handbook of Logic in Computer Science"},{"key":"6_CR16","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Local Model Checking Games","author":"C. Stirling","year":"1995","unstructured":"Stirling C. Local Model Checking Games. Lecture Notes in Computer Science, v.962, 1995, p.1\u201311."},{"key":"6_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-61042-1_51","volume-title":"Games and Modal Mu-Calculus","author":"C. Stirling","year":"1996","unstructured":"Stirling C. Games and Modal Mu-Calculus. Lecture Notes in Computer Science, v.1055, 1996, p.298\u2013312."},{"key":"6_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Practical Model Checking Using Games","author":"P. Steven","year":"1998","unstructured":"Steven P., Stirling C. Practical Model Checking Using Games. Lecture Notes in Computer Science, v.1384, 1998, p.85\u2013101."}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45575-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:12:52Z","timestamp":1737058372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45575-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430759","9783540455752"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45575-2_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"18 December 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}