A Novel Symbolic Approach to Verifying Epistemic Properties of Programs
Abstract
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.
Cite
Text
Gorogiannis et al. "A Novel Symbolic Approach to Verifying Epistemic Properties of Programs." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/30Markdown
[Gorogiannis et al. "A Novel Symbolic Approach to Verifying Epistemic Properties of Programs." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/gorogiannis2017ijcai-novel/) doi:10.24963/IJCAI.2017/30BibTeX
@inproceedings{gorogiannis2017ijcai-novel,
title = {{A Novel Symbolic Approach to Verifying Epistemic Properties of Programs}},
author = {Gorogiannis, Nikos and Raimondi, Franco and Boureanu, Ioana},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {206-212},
doi = {10.24963/IJCAI.2017/30},
url = {https://mlanthology.org/ijcai/2017/gorogiannis2017ijcai-novel/}
}