A Novel Symbolic Approach to Verifying Epistemic Properties of Programs

A Novel Symbolic Approach to Verifying Epistemic Properties of Programs

Nikos Gorogiannis, Franco Raimondi, Ioana Boureanu

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 206-212. https://doi.org/10.24963/ijcai.2017/30

We introduce a framework for the symbolic verification of epistemic properties of programs expressed in a class of general-purpose programming languages. To this end, we reduce the verification problem to that of satisfiability of first-order formulae in appropriate theories. We prove the correctness of our reduction and we validate our proposal by applying it to two examples: the dining cryptographers problem and the ThreeBallot voting protocol. We put forward an implementation using existing solvers, and report experimental results showing that the approach can perform better than state-of-the-art symbolic model checkers for temporal-epistemic logic.
Keywords:
Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
Multidisciplinary Topics and Applications: Validation and Verification