Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems

TL;DR

This paper introduces a formal semantics and a verification method for knowledge-based multi-agent programs, enabling the modeling and checking of complex epistemic properties through a novel translation to first-order logic.

Contribution

It develops a relational and weakest precondition semantics for knowledge-based programs and implements a translation for verifying epistemic properties in multi-agent systems.

Findings

Effective translation of epistemic logic validity into first-order logic

Implementation of verification method in Haskell

Successful testing on established multi-agent examples

Abstract

We give a relational and a weakest precondition semantics for "knowledge-based programs", i.e., programs that restrict observability of variables so as to richly express changes in the knowledge of agents who can or cannot observe said variables. Based on these knowledge-based programs, we define a program-epistemic logic to model complex epistemic properties of the execution of multi-agent systems. We translate the validity of program-epistemic logic formulae into first-order validity, using our weakest precondition semantics and an ingenious book-keeping of variable assignment. We implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and test this novel verification method for our new program-epistemic logic on a series of well-established examples.