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.
翻译:我们给“知识型程序”给出一种关系和最弱的先决条件语义,即限制变量可观察性的方案,以便能或无法观察这些变量的代理方的知识发生大量变化。基于这些知识型程序,我们定义了一种程序-全能逻辑,以模拟执行多试剂系统的复杂认知特性。我们将程序-全能逻辑公式的有效性转化为一阶有效性,使用我们最弱的前提条件语义和奇特的可变任务书记。我们用一般方式(即独立于逻辑语句中的程序)在哈斯凯尔翻译我们,并在一系列已经确立的例子中测试我们新的方案-全能逻辑的新核实方法。