{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T04:14:38Z","timestamp":1749096878248,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319448312"},{"type":"electronic","value":"9783319448329"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-44832-9_9","type":"book-chapter","created":{"date-parts":[[2016,8,9]],"date-time":"2016-08-09T10:24:12Z","timestamp":1470738252000},"page":"149-167","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Agnieszka M.","family":"Zbrzezny","sequence":"first","affiliation":[]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,10]]},"reference":[{"key":"9_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9_CR2","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories (chap. 26). In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. In: Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"9_CR4","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85\u201396. Springer, Heidelberg (2004)"},{"key":"9_CR6","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"EA Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic (chap. 16). In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 996\u20131071. Elsevier Science Publishers, Amsterdam (1990)"},{"issue":"4","key":"9_CR7","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"EA Emerson","year":"1992","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Syst. 4(4), 331\u2013352 (1992)","journal-title":"Real-Time Syst."},{"key":"9_CR8","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.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"9_CR10","unstructured":"Jones, A.V., Lomuscio, A.: Distributed BDD-based BMC for the verification of multi-agent systems. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), pp. 675\u2013682. IFAAMAS (2010)"},{"issue":"1\u20134","key":"9_CR11","first-page":"313","volume":"85","author":"M Kacprzak","year":"2008","unstructured":"Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1\u20134), 313\u2013328 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"9_CR12","unstructured":"Levesque, H.: A Logic of implicit and explicit belief. In: Proceedings of the 6th National Conference of the AAAI, pp. 198\u2013202. Morgan Kaufman, Palo Alto (1984)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"9_CR14","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1026176900459","volume":"75","author":"A Lomuscio","year":"2003","unstructured":"Lomuscio, A., Sergot, M.: Deontic interpreted systems. Stud. Logica. 75(1), 63\u201392 (2003)","journal-title":"Stud. Logica."},{"issue":"4","key":"9_CR15","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1007\/s10458-013-9232-2","volume":"28","author":"A M\u0229ski","year":"2014","unstructured":"M\u0229ski, A., Penczek, W., Szreter, M., Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.: BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton. Agents and Multi-agent Syst. 28(4), 558\u2013604 (2014)","journal-title":"Auton. Agents and Multi-agent Syst."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"issue":"2","key":"9_CR18","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 55(2), 167\u2013185 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"9_CR19","volume-title":"An Introduction to Multi-agent Systems","author":"M Wooldridge","year":"2009","unstructured":"Wooldridge, M.: An Introduction to Multi-agent Systems, 2nd edn. Wiley, Hoboken (2009)","edition":"2"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/978-3-642-40669-0_38","volume-title":"Progress in Artificial Intelligence","author":"B Wo\u017ana-Szcze\u015bniak","year":"2013","unstructured":"Wo\u017ana-Szcze\u015bniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. In: Correia, L., Reis, L.P., Cascalho, J. (eds.) EPIA 2013. LNCS, vol. 8154, pp. 444\u2013455. Springer, Heidelberg (2013)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/978-3-642-24769-9_40","volume-title":"Progress in Artificial Intelligence","author":"B Wo\u017ana-Szcze\u015bniak","year":"2011","unstructured":"Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A., Zbrzezny, A.: The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In: Antunes, L., Pinto, H.S. (eds.) EPIA 2011. LNCS, vol. 7026, pp. 551\u2013565. Springer, Heidelberg (2011)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.: Checking EMTLK properties of timed interpreted systems via bounded model checking. Studia Logica, 1\u201338 (2015)","DOI":"10.1007\/s11225-015-9637-9"},{"issue":"1\u20134","key":"9_CR23","doi-asserted-by":"crossref","first-page":"513","DOI":"10.3233\/FUN-2008-851-435","volume":"85","author":"A Zbrzezny","year":"2008","unstructured":"Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1\u20134), 513\u2013531 (2008)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","PRIMA 2016: Princiles and Practice of Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44832-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T16:26:57Z","timestamp":1749054417000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44832-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319448312","9783319448329"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44832-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}