{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T05:22:56Z","timestamp":1739942576627,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540244226"},{"type":"electronic","value":"9783540309604"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-30960-4_13","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T19:19:26Z","timestamp":1267125566000},"page":"189-212","source":"Crossref","is-referenced-by-count":13,"title":["Verifying Multi-agent Systems via Unbounded Model Checking"],"prefix":"10.1007","author":[{"given":"M.","family":"Kacprzak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Lomuscio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"\u0141asica","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Szreter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","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., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR2","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol.\u00a053. Cambridge University Press, Cambridge (2001)"},{"key":"13_CR3","series-title":"Massachusetts","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. Massachusetts. The MIT Press, Cambridge (1999)"},{"issue":"7","key":"13_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Journal of the ACM"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-36577-X_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Dembi\u0144ski","year":"2003","unstructured":"Dembi\u0144ski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS: A tool for verifying Timed Automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003, vol.\u00a02619, pp. 278\u2013283. Springer, Heidelberg (2003)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"issue":"3","key":"13_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"key":"13_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":"13_CR9","first-page":"151","volume-title":"Model checking vs. theorem proving: a manifesto","year":"1991","unstructured":"Halpern, J., Vardi, M. (eds.): Model checking vs. theorem proving: a manifesto. Artificial Intelligence and Mathematical Theory of Computation, pp. 151\u2013176. Academic Press Inc., London (1991)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-45133-4_10","volume-title":"Formal Approaches to Agent-Based Systems","author":"A. Lomuscio","year":"2003","unstructured":"Lomuscio, A., \u0141asica, T., Penczek, W.: Bounded model checking for interpreted systems: Preliminary experimental results. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A., Gordon-Spears, D.F. (eds.) FAABS 2002. LNCS, vol.\u00a02699, pp. 115\u2013125. Springer, Heidelberg (2003)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"13_CR12","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, H.: 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)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference (DAC 2001), June 2001, pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"13_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"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25927-5_15","volume-title":"Deontic Logic in Computer Science","author":"F. Raimondi","year":"2004","unstructured":"Raimondi, F., Lomuscio, A.: Symbolic model checking of deontic interpreted systems via OBDD\u2019s. In: Lomuscio, A., Nute, D. (eds.) DEON 2004. LNCS, vol.\u00a03065, Springer, Heidelberg (2004)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30960-4_14","volume-title":"Formal Approaches to Agent-Based Systems","author":"F. Raimondi","year":"2004","unstructured":"Raimondi, F., Lomuscio, A.: Towards model checking for multiagent systems via OBDD\u2019s. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS, vol.\u00a03228, Springer, Heidelberg (2004)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Agent-Mediated Electronic Commerce VI. Theories for and Engineering of Distributed Mechanisms and Systems","author":"F. Raimondi","year":"2006","unstructured":"Raimondi, F., Lomuscio, A.: Verification of multiagent systems via ordered binary decision diagrams: an algorithm and its implementation. In: Faratin, P., Rodr\u00edguez-Aguilar, J.-A. (eds.) AMEC 2004. LNCS, vol.\u00a03435, Springer, Heidelberg (2006)"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics\u00a05, 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"13_CR19","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":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1007\/3-540-47833-7","volume-title":"Agent-Mediated Electronic Commerce IV. Designing Mechanisms and Systems","author":"W. Hoek van der","year":"2002","unstructured":"van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: Padget, J., Shehory, O., Parkes, D.C., Sadeh, N.M., Walsh, W.E. (eds.) AMEC 2002. LNCS, vol.\u00a02531, pp. 1167\u20131174. Springer, Heidelberg (2002)"},{"key":"13_CR21","volume-title":"Proceedings of ICMAS, International Conference of Multi-Agent Systems","author":"M. Wooldridge","year":"2000","unstructured":"Wooldridge, M.: Computationally grounded theories of agency. In: Durfee, E. (ed.) Proceedings of ICMAS, International Conference of Multi-Agent Systems, IEEE Press, Los Alamitos (2000)"},{"key":"13_CR22","volume-title":"An introduction to multi-agent systems","author":"M. Wooldridge","year":"2002","unstructured":"Wooldridge, M.: An introduction to multi-agent systems. John Wiley, Chichester (2002)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-70657-7","volume-title":"Agent-Mediated Electronic Commerce IV. Designing Mechanisms and Systems","author":"M. Wooldridge","year":"2002","unstructured":"Wooldridge, M., Fisher, M., Huget, M., Parsons, S.: Model checking multiagent systems with mable. In: Padget, J., Shehory, O., Parkes, D.C., Sadeh, N.M., Walsh, W.E. (eds.) AAMAS 2002. LNCS, vol.\u00a02531, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Agent-Based Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30960-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T21:58:05Z","timestamp":1739915885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30960-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540244226","9783540309604"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30960-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}