{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T16:40:09Z","timestamp":1743525609564,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642309465"},{"type":"electronic","value":"9783642309472"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30947-2_56","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T09:16:30Z","timestamp":1340010990000},"page":"514-523","source":"Crossref","is-referenced-by-count":3,"title":["Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge"],"prefix":"10.1007","author":[{"given":"Artur","family":"M\u0119ski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Szreter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo\u017cena","family":"Wo\u017ana-Szcze\u015bniak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"56_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Highly Dependable Software. Advances in Computers, vol.\u00a058. Academic Press (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"56_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-540-45069-6_10","volume-title":"Computer Aided Verification","author":"R.H. Bordini","year":"2003","unstructured":"Bordini, R.H., Fisher, M., Pardavila, C., Visser, W., Wooldridge, M.: Model Checking Multi-Agent Programs with CASP. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 110\u2013113. Springer, Heidelberg (2003)"},{"key":"56_CR3","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Can BDD compete with SAT solvers on bounded model checking? In: DAC 2002, pp. 117\u2013122 (2002)","DOI":"10.1109\/DAC.2002.1012605"},{"key":"56_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"56_CR5","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"56_CR6","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)"},{"key":"56_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"Computer Aided Verification","author":"P. Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 479\u2013483. Springer, Heidelberg (2004)"},{"key":"56_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-46017-9_9","volume-title":"Model Checking Software","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Wooldridge, M.: Model Checking Knowledge and Time. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 95\u2013111. Springer, Heidelberg (2002)"},{"key":"56_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-20674-0_7","volume-title":"Model Checking and Artificial Intelligence","author":"X. Huang","year":"2011","unstructured":"Huang, X., Luo, C., van der Meyden, R.: Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS (LNAI), vol.\u00a06572, pp. 95\u2013111. Springer, Heidelberg (2011)"},{"key":"56_CR10","unstructured":"Jones, A., Lomuscio, A.: A BDD-based BMC approach for the verification of multi-agent systems. In: CS&P 2009, vol.\u00a01, pp. 253\u2013264. Warsaw University (2009)"},{"issue":"1-4","key":"56_CR11","doi-asserted-by":"crossref","first-page":"313","DOI":"10.3233\/FUN-2008-851-422","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak, M., Nabia\u0142ek, W., Niewiadomski, A., Penczek, W., P\u00f3\u0142rola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundamenta Informaticae\u00a085(1-4), 313\u2013328 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"56_CR12","unstructured":"Lomuscio, A., Penczek, W., Qu, H.: Partial order reduction for model checking interleaved multi-agent systems. In: AAMAS, pp. 659\u2013666. IFAAMAS Press (2010)"},{"key":"56_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/3-540-46691-6_35","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Meyden van der","year":"1999","unstructured":"van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 432\u2013445. Springer, Heidelberg (1999)"},{"issue":"2","key":"56_CR14","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"},{"issue":"2","key":"56_CR15","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.jal.2005.12.010","volume":"5","author":"F. Raimondi","year":"2007","unstructured":"Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic\u00a05(2), 235\u2013251 (2007)","journal-title":"Journal of Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Agent and Multi-Agent Systems. Technologies and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30947-2_56","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T15:59:20Z","timestamp":1743523160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30947-2_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642309465","9783642309472"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30947-2_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}