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.

翻译：基于知识的程序通过认知防护（epistemic guards）规定多智能体协议，这些防护抽象了智能体如何学习并记录关于其他智能体及环境的事实或信息。其解释涉及认知防护在可达状态上的评估与依赖认知防护评估结果的可达状态推导之间的非单调互依赖关系。我们将为同步编程语言设计的must/cannot分析技术应用于基于知识的程序的解释问题，证明由此产生的构造性解释是单调的且具有最小不动点。我们将该方法与现有的同步及异步程序解释方案进行关联。最后，我们描述了构造性解释的实现，并通过多个示例及其在Java内存模型中的应用展示了该过程。