{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:28:16Z","timestamp":1759638496382,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030945824"},{"type":"electronic","value":"9783030945831"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_5","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"93-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["EPMC Gets Knowledge in Multi-agent Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0397-7656","authenticated-orcid":false,"given":"Chen","family":"Fu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-7684","authenticated-orcid":false,"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7301-9234","authenticated-orcid":false,"given":"Yong","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9093-9518","authenticated-orcid":false,"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6550-7396","authenticated-orcid":false,"given":"Meng","family":"Sun","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-9323","authenticated-orcid":false,"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3692-2088","authenticated-orcid":false,"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"unstructured":"Apache Ant\u2122 website. http:\/\/ant.apache.org\/","key":"5_CR1"},{"unstructured":"Apache Maven website. http:\/\/maven.apache.org\/","key":"5_CR2"},{"unstructured":"Java Native Access (JNA) website. https:\/\/github.com\/java-native-access\/jna","key":"5_CR3"},{"unstructured":"JavaCC\u2122: The Java Compiler Compiler\u2122 website. http:\/\/javacc.org\/","key":"5_CR4"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60692-0_70"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R Bloem","year":"2006","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in $$n \\log n$$ symbolic steps. Formal Methods Syst. Des. 28(1), 37\u201356 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P \u010cerm\u00e1k","year":"2014","unstructured":"\u010cerm\u00e1k, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525\u2013532. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_34"},{"doi-asserted-by":"crossref","unstructured":"Cerm\u00e1k, P., Lomuscio, A., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: AAAI, pp. 2038\u20132044 (2015)","key":"5_CR9","DOI":"10.1609\/aaai.v29i1.9444"},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10703-012-0180-2","volume":"42","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Henzinger, M., Joglekar, M., Shah, N.: Symbolic algorithms for qualitative analysis of Markov decision processes with B\u00fcchi objectives. Formal Methods Syst. Des. 42(3), 301\u2013327 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185\u2013191. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_13"},{"doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: Liquor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131\u2013132 (2006)","key":"5_CR12","DOI":"10.1109\/QEST.2006.25"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"unstructured":"Cohen, H., Whaley, J., Wildt, J., Gorogiannis, N.: BuDDy. http:\/\/sourceforge.net\/p\/buddy\/","key":"5_CR14"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-04143-3_3","volume-title":"Multiagent System Technologies","author":"C Delgado","year":"2009","unstructured":"Delgado, C., Benevides, M.: Verification of epistemic properties in probabilistic multi-agent systems. In: Braubach, L., van der Hoek, W., Petta, P., Pokahr, A. (eds.) MATES 2009. LNCS (LNAI), vol. 5774, pp. 16\u201328. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04143-3_3"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T van Dijk","year":"2015","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60"},{"key":"5_CR18","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"2004","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (2004)"},{"unstructured":"Fu, C., Turrini, A., Huang, X., Song, L., Feng, Y., Zhang, L.: Model checking for probabilistic multiagent systems under uniform schedulers, submitted for publication, shared by the authors","key":"5_CR19"},{"doi-asserted-by":"crossref","unstructured":"Fu, C., Turrini, A., Huang, X., Song, L., Feng, Y., Zhang, L.: Model checking probabilistic epistemic logic for probabilistic multiagent systems. In: IJCAI, pp. 4757\u20134763 (2018)","key":"5_CR20","DOI":"10.24963\/ijcai.2018\/661"},{"key":"5_CR21","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. 3114, pp. 479\u2013483. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_41"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-41540-6_16","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 291\u2013311. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_16"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-319-52234-0_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"EM Hahn","year":"2017","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 266\u2013287. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_15"},{"issue":"5","key":"5_CR25","first-page":"512","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512\u2013535 (1994)","journal-title":"FAC"},{"doi-asserted-by":"crossref","unstructured":"Huang, X., Luo, C., van der Meyden, R.: Symbolic model checking of probabilistic knowledge. In: TARK, pp. 177\u2013186 (2011)","key":"5_CR26","DOI":"10.1145\/2000378.2000399"},{"doi-asserted-by":"crossref","unstructured":"Huang, X., van der Meyden, R.: Symbolic model checking epistemic strategy logic. In: AAAI, pp. 1426\u20131432 (2014)","key":"5_CR27","DOI":"10.1609\/aaai.v28i1.8894"},{"unstructured":"Jansen, D.N.: Understanding Fox and Glynn\u2019s \u201cComputing Poisson probabilities\u201d. Technical report. ICIS-R11001, Institute for Computing and Information Sciences, Radboud Universiteit (2011)","key":"5_CR28"},{"issue":"1\u20134","key":"5_CR29","first-page":"313","volume":"85","author":"M Kacprzak","year":"2008","unstructured":"Kacprzak, M., et al.: Verics 2007 - a model checker for knowledge and real-time. Fundam. Informaticae 85(1\u20134), 313\u2013328 (2008)","journal-title":"Fundam. Informaticae"},{"doi-asserted-by":"crossref","unstructured":"Katoen, J., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244 (2005)","key":"5_CR30","DOI":"10.1109\/QEST.2005.2"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11871842_29","volume-title":"Machine Learning: ECML 2006","author":"L Kocsis","year":"2006","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282\u2013293. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11871842_29"},{"doi-asserted-by":"crossref","unstructured":"Kong, J., Lomuscio, A.: Model checking multi-agent systems against LDLK specifications. In: IJCAI, pp. 1138\u20131144 (2017)","key":"5_CR32","DOI":"10.24963\/ijcai.2017\/158"},{"doi-asserted-by":"crossref","unstructured":"Kong, J., Lomuscio, A.: Model checking multi-agent systems against LDLK specifications on finite traces. In: AAMAS, pp. 166\u2013174 (2018)","key":"5_CR33","DOI":"10.24963\/ijcai.2017\/158"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-319-96145-3_30","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567\u2013577. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"unstructured":"Lomuscio, A., Paquet, H.: Verification of multi-agent systems via SDD-based model checking. In: AAMAS, pp. 1713\u20131714 (2015)","key":"5_CR36"},{"unstructured":"Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic verification of knowledge and time with NuSMV. In: Veloso, M.M. (ed.) IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, 6\u201312 January 2007, pp. 1384\u20131389 (2007)","key":"5_CR37"},{"doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Pirovano, E.: Verifying emergence of bounded time properties in probabilistic swarm systems. In: IJCAI, pp. 403\u2013409 (2018)","key":"5_CR38","DOI":"10.24963\/ijcai.2018\/56"},{"unstructured":"Lomuscio, A., Pirovano, E.: A counter abstraction technique for the verification of probabilistic swarm systems. In: AAMAS, pp. 161\u2013169 (2019)","key":"5_CR39"},{"unstructured":"Lomuscio, A., Pirovano, E.: Parameterised verification of strategic properties in probabilistic multi-agent systems. In: AAMAS, pp. 762\u2013770 (2020)","key":"5_CR40"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_55"},{"issue":"1","key":"5_CR42","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2015","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transfer 19(1), 9\u201330 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: mcmas: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450\u2013454. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_31"},{"key":"5_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39799-8_15","volume-title":"Computer Aided Verification","author":"G Lv","year":"2013","unstructured":"Lv, G., Su, K., Xu, Y.: CacBDD: a BDD package with dynamic cache management. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 229\u2013234. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_15"},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3) (2007)","key":"5_CR46","DOI":"10.2168\/LMCS-3(3:5)2007"},{"unstructured":"PRISM web site. http:\/\/www.prismmodelchecker.org","key":"5_CR47"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-00596-1_13","volume-title":"Foundations of Software Science and Computational Structures","author":"S Schewe","year":"2009","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167\u2013181. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13"},{"key":"5_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-33386-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"S Schewe","year":"2012","unstructured":"Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised B\u00fcchi automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 42\u201356. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_5"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46520-3_9","volume-title":"Automated Technology for Verification and Analysis","author":"S Sickert","year":"2016","unstructured":"Sickert, S., K\u0159et\u00ednsk\u00fd, J.: MoChiBA: probabilistic LTL model checking using limit-deterministic B\u00fcchi automata. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 130\u2013137. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_9"},{"unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 2.5.0. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/","key":"5_CR51"},{"issue":"4","key":"5_CR52","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","volume":"50","author":"K Su","year":"2007","unstructured":"Su, K., Sattar, A., Luo, X.: Model checking temporal logics of knowledge via OBDDs. Comput. J. 50(4), 403\u2013420 (2007)","journal-title":"Comput. J."},{"issue":"2","key":"5_CR53","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"unstructured":"Vahidi, A.: JDD, a pure Java BDD and Z-BDD library. http:\/\/javaddlib.sourceforge.net\/jdd\/","key":"5_CR54"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,16]],"date-time":"2024-09-16T07:23:49Z","timestamp":1726471429000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}