Interpreting Knowledge-based Programs (Extended Version with Proofs)

TL;DR

This paper presents a novel constructive interpretation method for knowledge-based programs, ensuring monotonicity and fixed-point properties, with applications demonstrated through examples and Java memory model analysis.

Contribution

It introduces a must/cannot analysis approach to interpret knowledge-based programs, addressing non-monotonic dependencies and relating to existing schemes.

Findings

Constructive interpretation is monotone and has a least fixed point.

The approach effectively models multi-agent protocols with epistemic guards.

Application to Java memory model demonstrates practical relevance.

Abstract

Knowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.