Symbolic model checking of public announcement protocols. (10th December 2019)

• Record Type: Journal Article
• Authors: Charrier, Tristan; Pinchinat, Sophie; Schwarzentruber, FranÇois
• Is Part Of: Journal of logic and computation. Volume 29:Number 8(2019)
• Page Start: 1211
• Page End: 1249
• Publication Date: 2019-12-10
• Subjects: epistemic logic -- model checking -- symbolic models -- arbitrary public announcements; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exz023
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: We study the symbolic model checking problem against public announcement protocol logic (PAPL), featuring protocols with public announcements, arbitrary public announcements and group announcements. Technically, symbolic models are Kripke models whose accessibility relations are presented as programs described in a dynamic logic style with propositional assignments. We highlight the relevance of such symbolic models and show that the symbolic model checking problem against PAPL is A$_{\textrm{pol}}$ Exptime -complete as soon as announcement protocols allow for either arbitrary announcements or iteration of public announcements. However, when both options are discarded, the complexity drops to Pspace -complete.