{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,27]],"date-time":"2024-07-27T00:14:43Z","timestamp":1722039283237},"reference-count":76,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T00:00:00Z","timestamp":1612137600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"ANR","doi-asserted-by":"publisher","award":["ANR-16-CE40-0021"],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005632","name":"National Centre for Research and Development","doi-asserted-by":"publisher","award":["POLLUX-IV\/1\/2016"],"id":[{"id":"10.13039\/501100005632","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":[[2021,2]]},"DOI":"10.1016\/j.ic.2020.104552","type":"journal-article","created":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T10:59:09Z","timestamp":1585565949000},"page":"104552","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":4,"special_numbering":"C","title":["Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol"],"prefix":"10.1016","volume":"276","author":[{"given":"Francesco","family":"Belardinelli","sequence":"first","affiliation":[]},{"given":"Rodica","family":"Condurache","sequence":"additional","affiliation":[]},{"given":"C\u0103t\u0103lin","family":"Dima","sequence":"additional","affiliation":[]},{"given":"Wojciech","family":"Jamroga","sequence":"additional","affiliation":[]},{"given":"Michal","family":"Knapik","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.ic.2020.104552_br0010","series-title":"Specification and Verification of Multi-Agent Systems","first-page":"125","article-title":"Model checking logics of strategic ability: complexity","author":"Bulling","year":"2010"},{"issue":"3","key":"10.1016\/j.ic.2020.104552_br0020","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/s10458-013-9231-3","article-title":"Comparing variants of strategic ability: how uncertainty and memory influence general properties of games","volume":"28","author":"Bulling","year":"2014","journal-title":"Auton. Agents Multi-Agent Syst."},{"issue":"2","key":"10.1016\/j.ic.2020.104552_br0030","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1023\/B:SYNT.0000024915.66183.d1","article-title":"Comparing semantics for logics of multi-agent systems","volume":"139","author":"Goranko","year":"2004","journal-title":"Synthese"},{"key":"10.1016\/j.ic.2020.104552_br0040","series-title":"Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS97)","first-page":"100","article-title":"Alternating-time temporal logic","author":"Alur","year":"1997"},{"issue":"5","key":"10.1016\/j.ic.2020.104552_br0050","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"},{"key":"10.1016\/j.ic.2020.104552_br0060","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1016\/j.ic.2014.12.020","article-title":"Augmenting atl with strategy contexts","volume":"245","author":"Laroussinie","year":"2015","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2020.104552_br0070","series-title":"Proceedings of the 18th International Conference on Concurrency Theory (CONCUR07)","first-page":"59","article-title":"Strategy logic","volume":"vol. 4703","author":"Chatterjee","year":"2007"},{"issue":"4","key":"10.1016\/j.ic.2020.104552_br0080","doi-asserted-by":"crossref","first-page":"34:1","DOI":"10.1145\/2631917","article-title":"Reasoning about strategies: on the model-checking problem","volume":"15","author":"Mogavero","year":"2014","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"10.1016\/j.ic.2020.104552_br0090","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","article-title":"A modal logic for coalitional power in games","volume":"12","author":"Pauly","year":"2002","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.ic.2020.104552_br0100","series-title":"Proceedings of Logic in Computer Science (LICS)","first-page":"379","article-title":"An abstraction-refinement framework for multi-agent systems","author":"Ball","year":"2006"},{"key":"10.1016\/j.ic.2020.104552_br0110","series-title":"Proceedings of the 4th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS05)","first-page":"157","article-title":"A logic for strategic reasoning","author":"van der Hoek","year":"2005"},{"key":"10.1016\/j.ic.2020.104552_br0120","first-page":"133","article-title":"Reasoning About Strategies","volume":"vol. 8","author":"Mogavero","year":"2010"},{"key":"10.1016\/j.ic.2020.104552_br0130","series-title":"Proceedings of 16th International Conference on Computer Aided Verification (CAV04)","first-page":"479","article-title":"MCK: model checking the logic of knowledge","volume":"vol. 3114","author":"Gammie","year":"2004"},{"issue":"1","key":"10.1016\/j.ic.2020.104552_br0140","first-page":"313","article-title":"Verics 2007 - a model checker for knowledge and real-time","volume":"85","author":"Kacprzak","year":"2008","journal-title":"Fundam. Inform."},{"key":"10.1016\/j.ic.2020.104552_br0150","author":"Lomuscio"},{"key":"10.1016\/j.ic.2020.104552_br0160","series-title":"Proceedings of the 4th European Workshop on Multi-Agent Systems EUMAS'06","first-page":"14","article-title":"Model checking abilities under incomplete information is indeed \u03b4p2-complete","author":"Jamroga","year":"2006"},{"key":"10.1016\/j.ic.2020.104552_br0170","author":"Dima"},{"key":"10.1016\/j.ic.2020.104552_br0180","series-title":"AAMAS'17","first-page":"1268","article-title":"Verification of multi-agent systems with imperfect information and public actions","author":"Belardinelli","year":"2017"},{"key":"10.1016\/j.ic.2020.104552_br0190","series-title":"IJCAI'17","first-page":"91","article-title":"Verification of broadcasting multi-agent systems against an epistemic strategy logic","author":"Belardinelli","year":"2017"},{"issue":"Part","key":"10.1016\/j.ic.2020.104552_br0200","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1016\/j.ic.2017.09.011","article-title":"Practical verification of multi-agent systems against slk specifications","volume":"261","author":"Cerm\u00e1k","year":"2018","journal-title":"Inf. Comput."},{"key":"10.1016\/j.ic.2020.104552_br0210","series-title":"Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017","first-page":"1241","article-title":"Fixpoint approximation of strategic abilities under imperfect information","author":"Jamroga","year":"2017"},{"key":"10.1016\/j.ic.2020.104552_br0220","series-title":"Conference Record of the Fourth ACM Symposium on Principles of Programming Languages","first-page":"238","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"issue":"5","key":"10.1016\/j.ic.2020.104552_br0230","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstractions","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.ic.2020.104552_br0240","series-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV00)","first-page":"154","article-title":"Counterexample-guided abstraction refinement","volume":"vol. 1855","author":"Clarke","year":"2000"},{"key":"10.1016\/j.ic.2020.104552_br0250","series-title":"Proceedings of Logic in Computer Science (LICS)","first-page":"170","article-title":"Three-valued abstractions of games: uncertainty, but with precision","author":"de Alfaro","year":"2004"},{"key":"10.1016\/j.ic.2020.104552_br0260","series-title":"Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS)","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.2020.104552_br0270","series-title":"Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS)","first-page":"1259","article-title":"Agent-based abstractions for verifying alternating-time temporal logic with imperfect information","author":"Belardinelli","year":"2017"},{"key":"10.1016\/j.ic.2020.104552_br0280","article-title":"Modal Logic","volume":"vol. 53","author":"Blackburn","year":"2001"},{"key":"10.1016\/j.ic.2020.104552_br0290","series-title":"Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR'98)","first-page":"163","article-title":"Alternating refinement relations","volume":"vol. 1466","author":"Alur","year":"1998"},{"key":"10.1016\/j.ic.2020.104552_br0300","series-title":"Proceedings of CONCUR '92","first-page":"222","article-title":"Propositional temporal logics and equivalences","author":"Goltz","year":"1992"},{"key":"10.1016\/j.ic.2020.104552_br0310","series-title":"Proceedings of TARK XI","first-page":"15","article-title":"Alternating-time temporal logics with irrevocable strategies","author":"\u00c5gotnes","year":"2007"},{"key":"10.1016\/j.ic.2020.104552_br0320","series-title":"Logical Methods for Specification and Verification of Multi-Agent Systems","author":"Jamroga","year":"2015"},{"key":"10.1016\/j.ic.2020.104552_br0330","series-title":"Formal Methods: State of the Art and New Directions","first-page":"148","article-title":"The computer ate my vote","author":"Ryan","year":"2009"},{"issue":"3","key":"10.1016\/j.ic.2020.104552_br0340","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1109\/MSP.2015.54","article-title":"End-to-end verifiability in voting systems, from theory to practice","volume":"13","author":"Ryan","year":"2015","journal-title":"IEEE Secur. Priv."},{"issue":"2","key":"10.1016\/j.ic.2020.104552_br0350","first-page":"115","article-title":"Verifying voting schemes","volume":"19","author":"Beckert","year":"2014","journal-title":"J. Inf. Secur. Appl."},{"issue":"1","key":"10.1016\/j.ic.2020.104552_br0360","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/2728816.2728823","article-title":"Formal verification of e-voting: solutions and challenges","volume":"2","author":"Cortier","year":"2015","journal-title":"ACM SIGLOG News"},{"issue":"4","key":"10.1016\/j.ic.2020.104552_br0370","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","article-title":"Verifying privacy-type properties of electronic voting protocols","volume":"17","author":"Delaune","year":"2009","journal-title":"J. Comput. Secur."},{"issue":"8","key":"10.1016\/j.ic.2020.104552_br0380","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Commun. ACM"},{"key":"10.1016\/j.ic.2020.104552_br0390","series-title":"Proceedings of the 1996 European Symposium on Research in Computer Security (ESORICS'96)","first-page":"198","article-title":"CSP and anonymity","volume":"vol. 1146","author":"Schneider","year":"1996"},{"key":"10.1016\/j.ic.2020.104552_br0400","series-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99)","first-page":"55","article-title":"A meta-notation for protocol analysis","author":"Cervesato","year":"1999"},{"key":"10.1016\/j.ic.2020.104552_br0410","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/S1571-0661(05)82527-7","article-title":"Modeling group communication protocols using multiset term rewriting","volume":"71","author":"Denker","year":"2002","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2020.104552_br0420","series-title":"Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS'12)","first-page":"1141","article-title":"Automatic verification of epistemic specifications under convergent equational theories","author":"Boureanu","year":"2012"},{"key":"10.1016\/j.ic.2020.104552_br0430","series-title":"Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016","first-page":"1:1","article-title":"Expressing receipt-freeness and coercion-resistance in logics of strategic ability: preliminary attempt","author":"Tabatabaei","year":"2016"},{"key":"10.1016\/j.ic.2020.104552_br0440","author":"Rivest"},{"key":"10.1016\/j.ic.2020.104552_br0450","series-title":"Proceedings of USENIX\/ACCURATE Electronic Voting Technology Workshop (EVT)","article-title":"Three voting protocols: ThreeBallot, VAV, and Twin","author":"Rivest","year":"2007"},{"issue":"1","key":"10.1016\/j.ic.2020.104552_br0460","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s00165-012-0268-x","article-title":"Verifying anonymity in voting systems using csp","volume":"26","author":"Moran","year":"2014","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"10.1016\/j.ic.2020.104552_br0470","doi-asserted-by":"crossref","first-page":"1049","DOI":"10.1007\/s10270-014-0445-x","article-title":"Automated anonymity verification of the ThreeBallot and VAV voting systems","volume":"15","author":"Moran","year":"2016","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.ic.2020.104552_br0480","series-title":"Proc. of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS17)","first-page":"1286","article-title":"Bisimulations for verifying strategic abilities with an application to threeballot","author":"Belardinelli","year":"2017"},{"key":"10.1016\/j.ic.2020.104552_br0490","series-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference","first-page":"425","article-title":"Bisimulations for logics of strategies: a study in expressiveness and verification","author":"Belardinelli","year":"2018"},{"key":"10.1016\/j.ic.2020.104552_br0500","series-title":"Proceedings of AAMAS2010","first-page":"625","article-title":"Reasoning about strategies of multi-agent programs","author":"Dastani","year":"2010"},{"key":"10.1016\/j.ic.2020.104552_br0510","series-title":"Game theory and logic for non-repudiation protocols and attack analysis","author":"Melissen","year":"2013"},{"key":"10.1016\/j.ic.2020.104552_br0520","series-title":"Verification and composition of security protocols with applications to electronic voting","author":"Ciob\u00e2c\u0103","year":"2011"},{"issue":"9","key":"10.1016\/j.ic.2020.104552_br0530","doi-asserted-by":"crossref","first-page":"1262","DOI":"10.4304\/jnw.6.9.1262-1271","article-title":"Automatic verification of remote Internet voting protocol in symbolic model","volume":"6","author":"Meng","year":"2011","journal-title":"JNW"},{"issue":"4","key":"10.1016\/j.ic.2020.104552_br0540","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","article-title":"Verifying privacy-type properties of electronic voting protocols","volume":"17","author":"Delaune","year":"2009","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.ic.2020.104552_br0550","series-title":"VoteID, E-Voting and Identity - Third International Conference","first-page":"53","article-title":"Linear logical voting protocols","volume":"vol. 7187","author":"DeYoung","year":"2011"},{"key":"10.1016\/j.ic.2020.104552_br0560","series-title":"Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid","first-page":"135","article-title":"Analysing vote counting algorithms via logic - and its application to the CADE election scheme","volume":"vol. 7898","author":"Beckert","year":"2013"},{"key":"10.1016\/j.ic.2020.104552_br0570","series-title":"AI 2015: Advances in Artificial Intelligence - 28th Australasian Joint Conference","first-page":"464","article-title":"Vote counting as mathematical proof","volume":"vol. 9457","author":"Pattinson","year":"2015"},{"key":"10.1016\/j.ic.2020.104552_br0580","series-title":"E-Vote-ID, Electronic Voting - Second International Joint Conference","first-page":"110","article-title":"Towards a mechanized proof of selene receipt-freeness and vote-privacy","volume":"vol. 10615","author":"Bruni","year":"2017"},{"key":"10.1016\/j.ic.2020.104552_br0590","series-title":"Vote-ID, E-Voting and Identify - 4th International Conference","first-page":"25","article-title":"On the specification and verification of voting schemes","volume":"vol. 7985","author":"Beckert","year":"2013"},{"issue":"2","key":"10.1016\/j.ic.2020.104552_br0600","first-page":"115","article-title":"Verifying voting schemes","volume":"19","author":"Beckert","year":"2014","journal-title":"J. Inf. Sec. Appl."},{"key":"10.1016\/j.ic.2020.104552_br0610","series-title":"E-Vote-ID, Electronic Voting - First International Joint Conference","first-page":"192","article-title":"A risk-limiting audit in Denmark: a pilot","volume":"vol. 10141","author":"Sch\u00fcrmann","year":"2016"},{"key":"10.1016\/j.ic.2020.104552_br0620","series-title":"ITP, Interactive Theorem Proving - 4th International Conference","first-page":"17","article-title":"Certifying voting protocols","volume":"vol. 7998","author":"Sch\u00fcrmann","year":"2013"},{"issue":"1","key":"10.1016\/j.ic.2020.104552_br0630","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/2728816.2728823","article-title":"Formal verification of e-voting: solutions and challenges","volume":"2","author":"Cortier","year":"2015","journal-title":"SIGLOG News"},{"key":"10.1016\/j.ic.2020.104552_br0640","series-title":"Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID)","first-page":"100","article-title":"Model checking the SELENE e-voting protocol in multi-agent logics","volume":"vol. 11143","author":"Jamroga","year":"2018"},{"key":"10.1016\/j.ic.2020.104552_br0650","first-page":"1","article-title":"Agents that know how to play","volume":"62","author":"Jamroga","year":"2004","journal-title":"Fundam. Inform."},{"issue":"2","key":"10.1016\/j.ic.2020.104552_br0660","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1016\/S1571-0661(05)82604-0","article-title":"Alternating-time logic with imperfect recall","volume":"85","author":"Schobbens","year":"2004","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.ic.2020.104552_br0670","series-title":"Proceedings of IJCAI-11","first-page":"109","article-title":"Alternating epistemic mu-calculus","author":"Bulling","year":"2011"},{"key":"10.1016\/j.ic.2020.104552_br0680","series-title":"Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing","first-page":"544","article-title":"Receipt-free secret-ballot elections","author":"Benaloh","year":"1994"},{"key":"10.1016\/j.ic.2020.104552_br0690","series-title":"Proceedings of the Workshop Frontiers in Electronic Elections (FEE 2005)","article-title":"Receipt-freeness: formal definition and fault attacks","author":"Delaune","year":"2005"},{"key":"10.1016\/j.ic.2020.104552_br0700","series-title":"Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society","first-page":"61","article-title":"Coercion-resistant electronic elections","author":"Juels","year":"2005"},{"key":"10.1016\/j.ic.2020.104552_br0710","series-title":"Proceedings of the 1st International Workshop on AI for Privacy and Security PrAISe 2016","first-page":"1:1","article-title":"Expressing receipt-freeness and coercion-resistance in logics of strategic ability: preliminary attempt","author":"Tabatabaei","year":"2016"},{"key":"10.1016\/j.ic.2020.104552_br0720","series-title":"Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS06)","first-page":"548","article-title":"The complexity of model checking concurrent programs against CTLK specifications","author":"Lomuscio","year":"2006"},{"key":"10.1016\/j.ic.2020.104552_br0730","series-title":"Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 2, AAMAS '09, International Foundation for Autonomous Agents and Multiagent Systems","first-page":"945","article-title":"Abstraction in model checking multi-agent systems","author":"Cohen","year":"2009"},{"key":"10.1016\/j.ic.2020.104552_br0740","author":"Belardinelli"},{"key":"10.1016\/j.ic.2020.104552_br0750","series-title":"Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS06)","first-page":"201","article-title":"On the complexity of practical atl model checking knowledge, strategies, and games in multi-agent systems","author":"van der Hoek","year":"2006"},{"key":"10.1016\/j.ic.2020.104552_br0760","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1016\/j.ic.2015.03.014","article-title":"Reasoning about memoryless strategies under partial observability and unconditional fairness constraints","volume":"242","author":"Busard","year":"2015","journal-title":"Inf. Comput."}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540120300407?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540120300407?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T09:46:28Z","timestamp":1610099188000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540120300407"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2]]},"references-count":76,"alternative-id":["S0890540120300407"],"URL":"https:\/\/doi.org\/10.1016\/j.ic.2020.104552","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2021,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol","name":"articletitle","label":"Article Title"},{"value":"Information and Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.ic.2020.104552","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2020 Elsevier Inc. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"104552"}}