Automatically Verifying Expressive Epistemic Properties of Programs
Automatically Verifying Expressive Epistemic Properties of Programs
复制标题
DOI：
10.1609/aaai.v37i5.25769
复制
发表时间：
2023-06
期刊：
影响因子：
--
通讯作者：
F. Belardinelli;Ioana Boureanu;Vadim Malvone;Fortunat Rajaona
中科院分区：
文献类型：
--
作者：
F. Belardinelli;Ioana Boureanu;Vadim Malvone;Fortunat Rajaona
我们提出了一种新的方法来验证程序的认知属性。首先，我们介绍了新的“程序认知”逻辑L_PK，这是严格丰富和更普遍的比类似的形式主义出现在文献中。为了以一种有效的方式解决验证问题，我们引入了从我们的语言L_PK到一阶逻辑的翻译。然后，我们展示并证明了正确的减少从模型检查问题的程序认知公式的可满足性，他们的一阶翻译。我们的逻辑和翻译都可以处理更丰富的规范w.r.t.现有技术，允许我们表达代理关于与程序有关的事实的知识（即，代理在程序执行之前和执行之后的知识）。此外，我们以一般的方式在Haskell中实现我们的翻译（即，独立于逻辑语句中的程序），并且我们使用现有的SMT求解器来检查AI/代理领域中的基准示例上的L_PK公式的满意度。
We propose a new approach to the verification of epistemic properties of programmes. First, we introduce the new ``program-epistemic'' logic L_PK, which is strictly richer and more general than similar formalisms appearing in the literature. To solve the verification problem in an efficient way, we introduce a translation from our language L_PK into first-order logic. Then, we show and prove correct a reduction from the model checking problem for program-epistemic formulas to the satisfiability of their first-order translation. Both our logic and our translation can handle richer specification w.r.t. the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (i.e., agents' knowledge before a program is executed as well as after is has been executed). Furthermore, we implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and we use existing SMT-solvers to check satisfaction of L_PK formulas on a benchmark example in the AI/agency field.