Automatically Verifying Expressive Epistemic Properties of Programs


  • Francesco Belardinelli Imperial College London
  • Ioana Boureanu University of Surrey
  • Vadim Malvone Telecom Paris
  • Fortunat Rajaona University of Surrey



KRR: Knowledge Representation Languages


We propose a new approach to the verification of epistemic properties of programmes. First, we introduce the new ``program-epistemic'' logic L_PK, which is strictly richer and more general than similar formalisms appearing in the literature. To solve the verification problem in an efficient way, we introduce a translation from our language L_PK into first-order logic. Then, we show and prove correct a reduction from the model checking problem for program-epistemic formulas to the satisfiability of their first-order translation. Both our logic and our translation can handle richer specification w.r.t. the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (i.e., agents' knowledge before a program is executed as well as after is has been executed). Furthermore, we implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and we use existing SMT-solvers to check satisfaction of L_PK formulas on a benchmark example in the AI/agency field.




How to Cite

Belardinelli, F., Boureanu, I., Malvone, V., & Rajaona, F. (2023). Automatically Verifying Expressive Epistemic Properties of Programs. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6245-6252.



AAAI Technical Track on Knowledge Representation and Reasoning