{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:35Z","timestamp":1760202755849,"version":"build-2065373602"},"reference-count":53,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"publisher","award":["EP\/I00520X"],"award-info":[{"award-number":["EP\/I00520X"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003852","name":"Regione Campania","doi-asserted-by":"publisher","award":["B25B09090 100007"],"award-info":[{"award-number":["B25B09090 100007"]}],"id":[{"id":"10.13039\/501100003852","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011102","name":"FP7","doi-asserted-by":"publisher","award":["600958-SHERPA"],"award-info":[{"award-number":["600958-SHERPA"]}],"id":[{"id":"10.13039\/100011102","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003407","name":"MIUR","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1016\/j.ic.2017.09.011","type":"journal-article","created":{"date-parts":[[2017,9,18]],"date-time":"2017-09-18T17:47:29Z","timestamp":1505756849000},"page":"588-614","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":12,"special_numbering":"P3","title":["Practical verification of multi-agent systems against Slk specifications"],"prefix":"10.1016","volume":"261","author":[{"given":"Petr","family":"\u010cerm\u00e1k","sequence":"first","affiliation":[]},{"given":"Alessio","family":"Lomuscio","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Mogavero","sequence":"additional","affiliation":[]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"year":"2009","series-title":"An Introduction to MultiAgent Systems","author":"Wooldridge","key":"10.1016\/j.ic.2017.09.011_br0010"},{"year":"1995","series-title":"Reasoning About Knowledge","author":"Fagin","key":"10.1016\/j.ic.2017.09.011_br0020"},{"issue":"1","key":"10.1016\/j.ic.2017.09.011_br0030","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1026176900459","article-title":"Deontic interpreted systems","volume":"75","author":"Lomuscio","year":"2003","journal-title":"Stud. Log."},{"key":"10.1016\/j.ic.2017.09.011_br0040","series-title":"Intelligent Agents II","first-page":"33","article-title":"Decision procedures for propositional linear-time Belief-Desire-Intention logics","volume":"vol. 1037","author":"Rao","year":"1996"},{"key":"10.1016\/j.ic.2017.09.011_br0050","series-title":"Current Trends in Concurrency, Overviews and Tutorials","first-page":"510","article-title":"Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends","volume":"vol. 224","author":"Pnueli","year":"1986"},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0060","first-page":"167","article-title":"Verifying epistemic properties of multi-agent systems via bounded model checking","volume":"55","author":"Penczek","year":"2003","journal-title":"Fundam. Inform."},{"issue":"1\u20134","key":"10.1016\/j.ic.2017.09.011_br0070","doi-asserted-by":"crossref","first-page":"313","DOI":"10.3233\/FUN-2008-851-422","article-title":"Verics 2007 \u2014 a model checker for knowledge and real-time","volume":"85","author":"Kacprzak","year":"2008","journal-title":"Fundam. Inform."},{"issue":"8","key":"10.1016\/j.ic.2017.09.011_br0080","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"Trans. Comput."},{"key":"10.1016\/j.ic.2017.09.011_br0090","series-title":"Proceedings of 16th International Conference on Computer Aided Verification (CAV'04)","first-page":"479","article-title":"MCK: model checking the logic of knowledge","volume":"vol. 3114","author":"Gammie","year":"2004"},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0100","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.jal.2005.12.010","article-title":"Automatic verification of multi-agent systems by model checking via OBDDs","volume":"5","author":"Raimondi","year":"2005","journal-title":"J. Appl. Log."},{"key":"10.1016\/j.ic.2017.09.011_br0110","series-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI'09), Pasadena, USA","first-page":"721","article-title":"A symmetry reduction technique for model checking temporal-epistemic logic","author":"Cohen","year":"2009"},{"key":"10.1016\/j.ic.2017.09.011_br0120","series-title":"Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'09)","first-page":"945","article-title":"Abstraction in model checking multi-agent systems","author":"Cohen","year":"2009"},{"key":"10.1016\/j.ic.2017.09.011_br0130","series-title":"Proc. of the 15th Int. Conference on Autonomous Agents and Multiagent Systems (AAMAS'16)","first-page":"662","article-title":"Verification of multi-agent systems via predicate abstraction against ATLK specifications","author":"Lomuscio","year":"2016"},{"key":"10.1016\/j.ic.2017.09.011_br0140","series-title":"Proceedings of the 23rd International Conference on Software Engineering (ICSE'01)","first-page":"835","article-title":"jMocha: a model checking tool that exploits design structure","author":"Alur","year":"2001"},{"issue":"1","key":"10.1016\/j.ic.2017.09.011_br0150","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1026185103185","article-title":"Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications","volume":"75","author":"Hoek","year":"2003","journal-title":"Stud. Log."},{"key":"10.1016\/j.ic.2017.09.011_br0160","series-title":"Proceedings of the International Workshop on Formal Approaches to Multi-Agent Systems (FAMAS'03)","first-page":"133","article-title":"Some remarks on alternating temporal epistemic logic","author":"Jamroga","year":"2004"},{"key":"10.1016\/j.ic.2017.09.011_br0170","series-title":"Handbook of Logics for Knowledge and Belief","article-title":"Knowledge and ability","author":"\u00c5gotnes","year":"2015"},{"key":"10.1016\/j.ic.2017.09.011_br0180","series-title":"Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'16), IFAAMAS","first-page":"257","article-title":"Rational play and rational beliefs under uncertainty","author":"Bulling","year":"2009"},{"key":"10.1016\/j.ic.2017.09.011_br0190","series-title":"Proceedings of the 5th International Joint Conference on Autonomous agents and Multi-Agent Systems (AAMAS'06)","first-page":"161","article-title":"Model checking knowledge, strategies, and games in multi-agent systems","author":"Lomuscio","year":"2006"},{"key":"10.1016\/j.ic.2017.09.011_br0200","unstructured":"A. Lomuscio, H. Qu, F. Raimondi, MCMAS: a model checker for the verification of multi-agent systems, Software Tools for Technology Transfer."},{"issue":"5","key":"10.1016\/j.ic.2017.09.011_br0210","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"J. ACM"},{"year":"2003","series-title":"Feasible Strategies in Alternating-Time Temporal Epistemic Logic","author":"Jonker","key":"10.1016\/j.ic.2017.09.011_br0220"},{"key":"10.1016\/j.ic.2017.09.011_br0230","series-title":"Foundations of Software Technology and Theoretical Computer Science'10","first-page":"133","article-title":"Reasoning about strategies","volume":"vol. 8","author":"Mogavero","year":"2010"},{"key":"10.1016\/j.ic.2017.09.011_br0240","series-title":"Proceedings of the 26th International Conference on Computer Aided Verification (CAV'14)","first-page":"525","article-title":"MCMAS-SLK: A model checker for the verification of strategy logic specifications","volume":"vol. 8559","author":"\u010cerm\u00e1k","year":"2014"},{"issue":"6","key":"10.1016\/j.ic.2017.09.011_br0250","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","article-title":"Strategy logic","volume":"208","author":"Chatterjee","year":"2010","journal-title":"Inf. Comput."},{"issue":"4","key":"10.1016\/j.ic.2017.09.011_br0260","article-title":"Reasoning about strategies: on the model-checking problem","volume":"15","author":"Mogavero","year":"2014","journal-title":"Trans. Comput. Log."},{"issue":"5","key":"10.1016\/j.ic.2017.09.011_br0270","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"J. ACM"},{"year":"1995","series-title":"Reasoning about Knowledge","author":"Fagin","key":"10.1016\/j.ic.2017.09.011_br0280"},{"key":"10.1016\/j.ic.2017.09.011_br0290","series-title":"Foundation of Computer Science'77","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0300","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1145\/359496.359527","article-title":"Knowledge in multi-agent systems: initial configurations and broadcast","volume":"1","author":"Lomuscio","year":"2000","journal-title":"ACM Trans. Comput. Log."},{"year":"1999","series-title":"Knowledge Sharing Among Ideal Agents","author":"Lomuscio","key":"10.1016\/j.ic.2017.09.011_br0310"},{"key":"10.1016\/j.ic.2017.09.011_br0320","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1016\/0166-218X(84)90005-2","article-title":"A note on cake cutting","volume":"7","author":"Even","year":"1984","journal-title":"Discrete Appl. Math."},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0330","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata theoretic approach to branching-time model checking","volume":"47","author":"Kupferman","year":"2000","journal-title":"J. ACM"},{"key":"10.1016\/j.ic.2017.09.011_br0340","series-title":"Logic in Computer Science'86","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986"},{"key":"10.1016\/j.ic.2017.09.011_br0350","series-title":"Specification and Verification of Multi-Agent Systems'10","first-page":"125","article-title":"Model checking logics of strategic ability: complexity","author":"Bulling","year":"2010"},{"key":"10.1016\/j.ic.2017.09.011_br0360","series-title":"Symposium on Theory of Computing'73","first-page":"1","article-title":"Word problems requiring exponential time (preliminary report)","author":"Stockmeyer","year":"1973"},{"issue":"3","key":"10.1016\/j.ic.2017.09.011_br0370","article-title":"Reasoning about substructures and games","volume":"16","author":"Benerecetti","year":"2015","journal-title":"Trans. Comput. Log."},{"key":"10.1016\/j.ic.2017.09.011_br0380","series-title":"Proceedings of the 28th Annual IEEE\/ACM Symposium on Logic in Computer Science (LICS'13)","first-page":"263","article-title":"On the boundary of behavioral strategies","author":"Mogavero","year":"2013"},{"key":"10.1016\/j.ic.2017.09.011_br0390","series-title":"Proceedings of the 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS'06)","first-page":"161","article-title":"Model checking knowledge, strategies, and games in multi-agent systems","author":"Lomuscio","year":"2006"},{"year":"2010","series-title":"Symbolic Controller Synthesis for LTL Specifications","author":"Morgenstern","key":"10.1016\/j.ic.2017.09.011_br0400"},{"year":"2004","series-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"Huth","key":"10.1016\/j.ic.2017.09.011_br0410"},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0420","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inf. Comput."},{"author":"Somenzi","key":"10.1016\/j.ic.2017.09.011_br0440"},{"key":"10.1016\/j.ic.2017.09.011_br0450","series-title":"Proceedings of the 21th International Conference on Computer Aided Verification (CAV'09)","first-page":"682","article-title":"MCMAS: a model checker for the verification of multi-agent systems","volume":"vol. 5643","author":"Lomuscio","year":"2009"},{"issue":"1","key":"10.1016\/j.ic.2017.09.011_br0460","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF00206326","article-title":"The dining cryptographers problem: unconditional sender and recipient untraceability","volume":"1","author":"Chaum","year":"1988","journal-title":"J. Cryptol."},{"issue":"2","key":"10.1016\/j.ic.2017.09.011_br0470","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S1571-0661(05)82606-4","article-title":"A logic for ignorance","volume":"85","author":"van der Hoek","year":"2004","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2017.09.011_br0480","series-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04)","first-page":"280","article-title":"Symbolic model checking the knowledge of the dining cryptographers","author":"van der Meyden","year":"2004"},{"year":"2014","series-title":"A Model Checker for Strategy Logic","author":"\u010cerm\u00e1k","key":"10.1016\/j.ic.2017.09.011_br0490"},{"issue":"6","key":"10.1016\/j.ic.2017.09.011_br0500","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","article-title":"Strategy logic","volume":"208","author":"Chatterjee","year":"2010","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2017.09.011_br0510","series-title":"Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10)","first-page":"120","article-title":"ATL with strategy contexts: expressiveness and model checking","volume":"vol. 8","author":"Lopes","year":"2010"},{"key":"10.1016\/j.ic.2017.09.011_br0520","series-title":"Proceedings of the 28th Conference on Artificial Intelligence (AAAI'14)","first-page":"1426","article-title":"Symbolic model checking epistemic strategy logic","author":"Huang","year":"2014"},{"key":"10.1016\/j.ic.2017.09.011_br0530","series-title":"Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR'14)","first-page":"418","article-title":"A temporal logic of strategic knowledge","author":"Huang","year":"2014"},{"key":"10.1016\/j.ic.2017.09.011_br0540","series-title":"Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI'15)","first-page":"2038","article-title":"Verifying and synthesising multi-agent systems against one-goal strategy logic specifications","author":"\u010cerm\u00e1k","year":"2015"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540117301700?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540117301700?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T13:14:18Z","timestamp":1760188458000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540117301700"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8]]},"references-count":53,"alternative-id":["S0890540117301700"],"URL":"https:\/\/doi.org\/10.1016\/j.ic.2017.09.011","relation":{},"ISSN":["0890-5401"],"issn-type":[{"type":"print","value":"0890-5401"}],"subject":[],"published":{"date-parts":[[2018,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Practical verification of multi-agent systems against Slk specifications","name":"articletitle","label":"Article Title"},{"value":"Information and Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.ic.2017.09.011","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2017 Published by Elsevier Inc.","name":"copyright","label":"Copyright"}]}}