{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T21:40:16Z","timestamp":1737322816742,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540725039"},{"type":"electronic","value":"9783540725046"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72504-6_35","type":"book-chapter","created":{"date-parts":[[2007,7,22]],"date-time":"2007-07-22T11:36:39Z","timestamp":1185104199000},"page":"386-397","source":"Crossref","is-referenced-by-count":1,"title":["QBF-Based Symbolic Model Checking for Knowledge and Time"],"prefix":"10.1007","author":[{"given":"Conghua","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenyu","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihong","family":"Tao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","volume-title":"Model checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (2000)"},{"key":"35_CR2","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice Hall International, Hemel Hempstead (1991)"},{"issue":"5","key":"35_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Spin model checker. IEEE Transaction on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transaction on Software Engineering"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.Y. Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 1\u201322. Springer, Heidelberg (2001)"},{"key":"35_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)"},{"key":"35_CR6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/B978-0-12-450010-5.50015-3","volume-title":"Artificial Intelligence and Mathematical Theory of Computation","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: a manifesto. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation, pp. 151\u2013176. Academic Press, San Diego (1991)"},{"key":"35_CR7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Resaoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., et al.: Resaoning about Knowledge. MIT Press, Cambridge (1995)"},{"key":"35_CR8","unstructured":"Vardi, M.Y.: Implementing knowledge-based programs. In: Proc. of the Conf. on Theoretical Aspects of Rationality and Knowledge, pp. 15\u201330 (1996)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., et al.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"2","key":"35_CR10","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundamenta Informaticae\u00a055(2), 167\u2013185 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Luo, X., et al.: Bounded Model Checking Knowledge and Branching Time in Synchronous Multi-agent Systems. In: AAMAS\u201905 (2005)","DOI":"10.1145\/1082473.1082657"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Wozna, B., Lomuscio, A., Penczek, W.: Bounded Model Checking for Knowledge and Real Time. In: AAMAS\u201905 (2005)","DOI":"10.1145\/1082473.1082498"},{"key":"35_CR13","series-title":"ENTCS","first-page":"93","volume-title":"Proc. of LCMAS\u201904","author":"B. Wozna","year":"2004","unstructured":"Wozna, B., Lomuscio, A., Penczek, W.: Bounded model checking for deontic interpreted systems. In: Proc. of LCMAS\u201904. ENTCS, vol.\u00a0126, pp. 93\u2013114. Elsevier, Amsterdam (2004)"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","first-page":"18","volume-title":"Logic versus Approximation","author":"X. Zhao","year":"2004","unstructured":"Zhao, X., Kleine B\u00fcning, H.: On Models for Quantified Boolean Formulas. In: Lenski, W. (ed.) Logic versus Approximation. LNCS, vol.\u00a03075, pp. 18\u201332. Springer, Heidelberg (2004)"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-24605-3_8","volume-title":"Theory and Applications of Satisfiability Testing","author":"H. Kleine B\u00fcning","year":"2004","unstructured":"Kleine B\u00fcning, H., Subramani, K., Zhao, X.: On Boolean Models for Quantified Boolean Horn Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 93\u2013104. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72504-6_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T21:27:08Z","timestamp":1737322028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72504-6_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540725039","9783540725046"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72504-6_35","relation":{},"subject":[]}}