{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T22:15:05Z","timestamp":1765232105381,"version":"3.40.4"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,8,31]],"date-time":"2013-08-31T00:00:00Z","timestamp":1377907200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2014,7]]},"DOI":"10.1007\/s10458-013-9232-2","type":"journal-article","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T14:38:54Z","timestamp":1377873534000},"page":"558-604","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance"],"prefix":"10.1007","volume":"28","author":[{"given":"Artur","family":"M\u0229ski","sequence":"first","affiliation":[]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[]},{"given":"Maciej","family":"Szreter","sequence":"additional","affiliation":[]},{"given":"Bo\u017cena","family":"Wo\u017ana-Szcze\u015bniak","sequence":"additional","affiliation":[]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,8,31]]},"reference":[{"key":"9232_CR1","unstructured":"Abdulla, P. A., Bjesse, P., & E\u00e9n, N. (2000). Symbolic reachability analysis based on SAT-solvers. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201900). Lecture Notes in Computer Science, (Vol. 1785, pp. 411\u2013425). Berlin: Springer."},{"key":"9232_CR2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A. (2008). PicoSAT essentials. Journal on Satisfiability Boolean Modeling and Computation (JSAT), 4, 75\u201397.","journal-title":"Journal on Satisfiability Boolean Modeling and Computation (JSAT)"},{"key":"9232_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the ACM\/IEEE Design Automation Conference (DAC\u201999) (pp. 317\u2013320).","DOI":"10.1145\/309847.309942"},{"key":"9232_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, & Y. Zhu. (1999). Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999). Lecture Notes in Computer Science (Vol. 1579, pp. 193\u2013207). Berlin: Springer.","DOI":"10.21236\/ADA360973"},{"issue":"5:5","key":"9232_CR5","first-page":"1","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., & Schuppan, V. (2006). Linear encodings of bounded LTL model checking. Logical Methods in Computer Science, 2(5:5), 1\u201364.","journal-title":"Logical Methods in Computer Science"},{"key":"9232_CR6","doi-asserted-by":"crossref","unstructured":"R. Bordini, M. Fisher, C. Pardavila, W. Visser, & M. Wooldridge. (2003). Model checking multi-agent programs with CASP. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV\u201903). Lecture Notes in Computer Science (Vol. 2725, pp. 110\u2013113). Springer.","DOI":"10.1007\/978-3-540-45069-6_10"},{"issue":"6","key":"9232_CR7","doi-asserted-by":"crossref","first-page":"1385","DOI":"10.1093\/logcom\/exp029","volume":"19","author":"RH Bordini","year":"2009","unstructured":"Bordini, R. H., Fisher, M., Wooldridge, M., & Visser, W. (2009). Property-based slicing for agent verification. Journal of Logic and Computation, 19(6), 1385\u20131425.","journal-title":"Journal of Logic and Computation"},{"key":"9232_CR8","unstructured":"N. Bulling & W. Jamroga. (2010). Model checking agents with memory is harder than it seemed. In Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS\u201910) (pp. 633\u2013640). International Foundation for Autonomous Agents and Multiagent Systems."},{"key":"9232_CR9","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., & Quer, S. (2002). Can BDD compete with SAT solvers on bounded model checking?. In Proceedings of the 39th Design Automation Conference (DAC\u201902) (pp. 117\u2013122).","DOI":"10.1109\/DAC.2002.1012605"},{"issue":"1","key":"9232_CR10","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D Chaum","year":"1988","unstructured":"Chaum, D. (1988). The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology, 1(1), 65\u201375.","journal-title":"Journal of Cryptology"},{"key":"9232_CR11","unstructured":"Clarke, E., Grumberg, O., & Hamaguchi, K. (1994). Another look at LTL model checking. In Proceedings of the 6th International Conference on Computer Aided Verification (CAV\u201994). Lecture Notes in Computer Science (Vol. 818, pp. 415\u2013427). Berlin: Springer."},{"key":"9232_CR12","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge: MIT Press."},{"key":"9232_CR13","unstructured":"Copty, F., Fix, L., Fraer, R.., Giunchiglia, E., Kamhi, G.., Tacchella, A., & Vardi, M. (2001). Benefits of bounded model checking at an industrial setting. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901). Lecture Notes in Computer Science (Vol. 2102, pp. 436\u2013453). Berlin: Springer."},{"issue":"1","key":"9232_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L. A., Fisher, M., Webster, M. P., & Bordini, R. H. (2012). Model checking agent programming languages. Automated Software Engineering, 19(1), 5\u201363.","journal-title":"Automated Software Engineering"},{"key":"9232_CR15","unstructured":"Etessami, K., & Holzmann, G. J. (2000). Optimizing b\u00fcchi automata. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR\u201900). Lecture Notes in Computer Science (Vol. 1877, pp. 153\u2013167). Berlin: Springer."},{"key":"9232_CR16","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. (1995). Reasoning about Knowledge. Cambridge: MIT Press."},{"key":"9232_CR17","unstructured":"Gammie, P., & Meyden, R. (2004). MCK: Model checking the logic of knowledge. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201904). Lecture Notes in Computer Science (Vol. 3114, pp. 479\u2013483). Berlin: Springer."},{"key":"9232_CR18","unstructured":"Gastin, P., & Oddoux, D. (2001). Fast LTL to B\u00fcchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901). Lecture Notes in Computer Science (Vol. 2102, pp. 53\u201365). Berlin: Springer."},{"key":"9232_CR19","unstructured":"Gerth, R., Peled, D., Vardi, M., & Wolper, P. (1995). Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of IFIP\/WG6.1 Symposium. Protocol Specification, Testing and Verification (PSTV\u201995) (pp. 3\u201318). Chapman & Hall."},{"key":"9232_CR20","unstructured":"Halpern, J., & Vardi, M. (1991). Model checking vs. theorem proving: A manifesto. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR\u201991) (pp. 325\u2013334). Cambridge: Morgan Kaufmann."},{"issue":"1","key":"9232_CR21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1026185103185","volume":"75","author":"W Hoek","year":"2003","unstructured":"Hoek, W., & Wooldridge, M. (2003). Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, 75(1), 125\u2013157.","journal-title":"Studia Logica"},{"key":"9232_CR22","unstructured":"Hoek, W. V., & Wooldridge, M. (2002). Model checking knowledge and time. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software (SPIN\u20192002). Lecture Notes in Computer Science (Vol. 2318, pp. 95\u2013111). Berlin: Springer."},{"key":"9232_CR23","unstructured":"Huang, X., Luo, C., & van der Meyden, R. (2011). Improved bounded model checking for a fair branching-time temporal epistemic logic. In Proceedings of the 6th Workshop on Model Checking and Artificial Intelligence (MoChArt\u20192010), LNAI (Vol. 6572, pp. 95\u2013111). Berlin: Springer."},{"issue":"3","key":"9232_CR24","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s00224-007-9080-z","volume":"42","author":"W Jamroga","year":"2008","unstructured":"Jamroga, W., & Dix, J. (2008). Model checking abilities of agents: A closer look. Theory of Computing Systems, 42(3), 366\u2013410.","journal-title":"Theory of Computing Systems"},{"key":"9232_CR25","unstructured":"Jamroga, W., & Penczek, W. (2012). Specification and verification of multi-agent systems. In Lectures on Logic and Computation (ESSLLI\u20192010, ESSLLI\u20192011). Lecture Notes in Computer Science (Vol. 7388, pp. 210\u2013263). Berlin: Springer."},{"key":"9232_CR26","unstructured":"Jones, A. V., & Lomuscio, A. (2010). Distributed BDD-based BMC for the verification of multi-agent systems. In Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS\u20192010) (pp. 675\u2013682). Toronto: IFAAMAS Press."},{"issue":"1\u20132","key":"9232_CR27","first-page":"215","volume":"72","author":"M Kacprzak","year":"2006","unstructured":"Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., & Szreter, M. (2006). Comparing BDD and SAT based techniques for model checking Chaum\u2019s dining cryptographers protocol. Fundamenta Informaticae, 72(1\u20132), 215\u2013234.","journal-title":"Fundamenta Informaticae"},{"issue":"1\u20134","key":"9232_CR28","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., et al. (2008). Verics 2007\u2014a model checker for knowledge and real-time. Fundamenta Informaticae, 85(1\u20134), 313\u2013328.","journal-title":"Fundamenta Informaticae"},{"key":"9232_CR29","unstructured":"Lomuscio, A., Lasica, T., & Penczek, W. (2003). Bounded model checking for interpreted systems: Preliminary experimental results. In Proceedings of the 2nd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS\u201902), LNAI (Vol. 2699, pp. 115\u2013125). Berlin: Springer."},{"key":"9232_CR30","unstructured":"Lomuscio, A., Pecheur, C., & Raimondi, F. (2007). Automatic verification of knowledge and time with nusmv. In Proceedings of International Conference on Artificial Intelligence (IJCAI\u201907) ( pp. 1384\u20131389)."},{"key":"9232_CR31","unstructured":"Lomuscio, A., Penczek, W., & Qu, H. (2010). Partial order reduction for model checking interleaved multi-agent systems. In Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS\u20192010) (pp. 659\u2013666). Toronto: FAAMAS Press."},{"key":"9232_CR32","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.1016\/j.artint.2007.05.005","volume":"171","author":"A Lomuscio","year":"2007","unstructured":"Lomuscio, A., Penczek, W., & Wo\u017ana, B. (2007). Bounded model checking for knowledge and real time. Artificial Intelligence, 171, 1011\u20131038.","journal-title":"Artificial Intelligence"},{"key":"9232_CR33","unstructured":"M\u0229ski, A., Penczek, W., & Szreter, M. (2011). Bounded model checking linear time and knowledge using decision diagrams. In Proceedings of the International Workshop on Concurrency, Specification and Programming (CS &P\u201911) (pp. 363\u2013375)."},{"key":"9232_CR34","unstructured":"M\u0229ski, A., Penczek, W., & Szreter, M. (2012). BDD-based bounded model checking for LTLK over two variants of interpreted systems. In Proceedings of 5th International Workshop on Logics, Agents, and Mobility (pp. 35\u201350)."},{"key":"9232_CR35","unstructured":"M\u0229ski, A., Penczek, W., Szreter, M., Wo\u017ana-Szcze\u015bniak, B., & Zbrzezny, A. (2012). Bounded model checking for knowledge and linear time. In Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS\u20192012) (pp. 1447\u20131448). Toronto: IFAAMAS Press."},{"key":"9232_CR36","unstructured":"M\u0229ski, A., Penczek, W., Szreter, M., Wo\u017ana-Szcze\u015bniak, B., & Zbrzezny, A. (2012). Two approaches to bounded model checking for linear time logic with knowledge. In The Proceedings of the 6th KES International Conference on Agent and Multi-Agent Systems, Technologies and Applications (KES-AMSTA\u20192012). Lecture Notes in Computer Science (Vol. 7327, pp. 514\u2013523). Berlin: Springer."},{"key":"9232_CR37","unstructured":"M\u0229ski, A., Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A. M., & Zbrzezny, A. (2013). Two approaches to bounded model checking for a soft real-time epistemic computation tree logic. In Proceedings of the 10th International Symposium on Distributed Computing and Artificial Intelligence (DCAI\u20192013), Advances in Intelligent and Soft-Computing, (Vol. 217, pp. 483\u2013492). Berlin: Springer."},{"key":"9232_CR38","unstructured":"Meyden, R., & Shilov, N. V. (1999). Model checking knowledge and time in systems with perfect recall. In Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201999). Lecture Notes in Computer Science (Vol. 1738, pp. 432\u2013445). Berlin: Springer."},{"key":"9232_CR39","unstructured":"Meyden, R., & Su, K. (2004). Symbolic model checking the knowledge of the dining cryptographers. In Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW-17) (pp. 280\u2013291). IEEE Computer Society."},{"key":"9232_CR40","unstructured":"Peled D. (1993). All from one, one for all: On model checking using representatives. in Proceedings of the 5th International Conference on Computer Aided Verification (CAV\u201993). Lecture Notes in Computer Science (Vol. 697, pp. 409\u2013423). Berlin: Springer."},{"issue":"2","key":"9232_CR41","first-page":"167","volume":"55","author":"W Penczek","year":"2003","unstructured":"Penczek, W., & Lomuscio, A. (2003). Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2), 167\u2013185.","journal-title":"Fundamenta Informaticae"},{"issue":"3\u20134","key":"9232_CR42","doi-asserted-by":"crossref","first-page":"373","DOI":"10.3233\/FI-2012-743","volume":"119","author":"W Penczek","year":"2012","unstructured":"Penczek, W., Wo\u017ana-Szcze\u015bniak, B., & Zbrzezny, A. (2012). Towards SAT-based BMC for LTLK over interleaved interpreted systems. Fundamenta Informaticae, 119(3\u20134), 373\u2013392.","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"9232_CR43","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.jal.2005.12.010","volume":"5","author":"F Raimondi","year":"2007","unstructured":"Raimondi, F., & Lomuscio, A. (2007). Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 5(2), 235\u2013251.","journal-title":"Journal of Applied Logic"},{"key":"9232_CR44","unstructured":"Somenzi, F. CUDD: CU decision diagram package\u2014release 2.3.1. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html ."},{"key":"9232_CR45","unstructured":"Somenzi, F., Bloem, R. (2000). Efficient B\u00fcchi automata from LTL formulae. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV\u201900). Lecture Notes in Computer Science (Vol. 1855, pp. 248\u2013263). Berlin: Springer."},{"issue":"4","key":"9232_CR46","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","volume":"50","author":"K Su","year":"2007","unstructured":"Su, K., Sattar, A., & Luo, X. (2007). Model checking temporal logics of knowledge via OBDDs. The Computer Journal, 50(4), 403\u2013420.","journal-title":"The Computer Journal"},{"key":"9232_CR47","unstructured":"Troquard, N., Hoek, W. V. D., & Wooldridge, M. (2009). Model checking strategic equilibria. In Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence (MOCHART\u20192008), LNAI (Vol. 5348, pp. 166\u2013188). Berlin: Springer."},{"key":"9232_CR48","volume-title":"An introduction to multiagent systems","author":"M Wooldridge","year":"2002","unstructured":"Wooldridge, M. (2002). An introduction to multiagent systems. Chichester: Wiley."},{"key":"9232_CR49","unstructured":"Wo\u017ana, B., Lomuscio, A., & Penczek, W. (2005). Bounded model checking for deontic interpreted systems. In Proceedings of the 2nd International Workshop on Logic and Communication in Multi-Agent Systems (LCMAS\u201904), ENTCS (Vol. 126, pp. 93\u2013114). Amsterdam: Elsevier."},{"issue":"2","key":"9232_CR50","first-page":"223","volume":"55","author":"B Wo\u017ana","year":"2003","unstructured":"Wo\u017ana, B., Zbrzezny, A., & Penczek, W. (2003). Checking reachability properties for timed automata via SAT. Fundamenta Informaticae, 55(2), 223\u2013241.","journal-title":"Fundamenta Informaticae"},{"key":"9232_CR51","unstructured":"Wo\u017ana-Szcze\u015bniak, B., & Zbrzezny, A. (2012). Sat-based bounded model checking for deontic interleaved interpreted systems. In The Proceedings of the 6th KES International Conference on Agent and Multi-Agent Systems, Technologies and Applications (KES-AMSTA\u20192012). Lecture Notes in Computer Science (Vol. 7327, pp. 494\u2013503). Berlin: Springer."},{"key":"9232_CR52","unstructured":"Wo\u017ana-Szcze\u015bniak, B., & Zbrzezny, A. (2013). SAT-based bmc for deontic metric temporal logic and deontic interleaved interpreted systems. In Declarative Agent Languages and Technologies X. The 10th International Workshop (DALT\u20192012), LNAI (Vol. 7784, pp. 70\u2013189). Berlin: Springer."},{"key":"9232_CR53","unstructured":"Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A. M., & Zbrzezny, A. (2011). The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In In Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA\u20192011), LNAI (Vol. 7026, pp. 551\u2013565). Berlin: Springer."},{"issue":"1\u20134","key":"9232_CR54","doi-asserted-by":"crossref","first-page":"513","DOI":"10.3233\/FUN-2008-851-435","volume":"85","author":"A Zbrzezny","year":"2008","unstructured":"Zbrzezny, A. (2008). Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1\u20134), 513\u2013531.","journal-title":"Fundamenta Informaticae"},{"issue":"3\u20134","key":"9232_CR55","first-page":"377","volume":"120","author":"A Zbrzezny","year":"2012","unstructured":"Zbrzezny, A. (2012). A new translation from $$\\text{ ECTL }^{*}$$ ECTL \u2217 to SAT. Fundamenta Informaticae, 120(3\u20134), 377\u2013397.","journal-title":"Fundamenta Informaticae"}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-013-9232-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10458-013-9232-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-013-9232-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T14:19:15Z","timestamp":1746022755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10458-013-9232-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,31]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["9232"],"URL":"https:\/\/doi.org\/10.1007\/s10458-013-9232-2","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"type":"print","value":"1387-2532"},{"type":"electronic","value":"1573-7454"}],"subject":[],"published":{"date-parts":[[2013,8,31]]}}}