An SMT-based approach to the verification of knowledge-based programs
File(s)
Published version
Author(s)
Belardinelli, Francesco
Boureanu, Ioana
Malvone, Vadim
Rajaona, Fortunat
Type
Journal Article
Abstract
We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a “program epistemic” logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex, including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can “see” only a part of the global space of variables. We verify program-epistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers.
Date Issued
2025-03-01
Date Acceptance
2024-09-24
Citation
Formal Aspects of Computing, 2025, 37 (1)
ISSN
0934-5043
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
Formal Aspects of Computing
Volume
37
Issue
1
Copyright Statement
© 2024 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License.
License URL
Identifier
10.1145/3700150
Subjects
CCS Concepts: • Theory of computation → Logic and verification
Verification by model checking
Hoare logic
Model Checking, Epistemic Logic, Epistemic Predicate Transformers, Program Semantics This work is licensed under a Creative Commons Attribution International 4.0 License
Publication Status
Published
Article Number
3
Date Publish Online
2024-12-27