Page 121 - 《软件学报》2020年第12期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2020,31(12):3787−3796 [doi: 10.13328/j.cnki.jos.005888] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
面向完美回忆的时态认知逻辑

张玉志, 唐晓嘉

(西南大学 逻辑与智能研究中心,重庆 400715)
通讯作者: 唐晓嘉, E-mail: tangxj@swu.edu.cn

摘 要: 传统时态认知逻辑对完美回忆的刻画是狭隘的,并不能完整表达主体记得自己先前的认知状态.新系统
t
t
t
t
S5 C 将认知与时态融合进同一个算子中,个体知识、普遍知识和公共知识都被时间点所标注.S5 C 系统从技术上实
t
t
现了每个个体(群体)都可以完美回忆自己在之前所有时刻上的认知状态.利用典范模型技术可以证明,S5 C 系统在
等价且单调递减的框架类上是完全的.
t
t
关键词: 时态认知逻辑; S5 C 系统;完美回忆;记忆公理
中图法分类号: TP18
中文引用格式: 张玉志,唐晓嘉.面向完美回忆的时态认知逻辑.软件学报,2020,31(12):3787−3796. http://www.jos.org.cn/1000-
9825/5888.htm
英文引用格式: Zhang YZ, Tang XJ. Temporal epistemic logic for perfect recall. Ruan Jian Xue Bao/Journal of Software, 2020,
31(12):3787−3796 (in Chinese). http://www.jos.org.cn/1000-9825/5888.htm
Temporal Epistemic Logic for Perfect Recall

ZHANG Yu-Zhi, TANG Xiao-Jia
(Institute for Logic and Intelligence, Southwest University, Chongqing 400715, China)
Abstract: Traditional temporal epistemic logic is defective to express perfect recall. It cannot express the memories of individuals’
t
t
knowledge. Time and knowledge are integrated into a single operator in the new system S5 C , such that individual knowledge, general
knowledge and common knowledge can be indicated by certain time. With this simple setting, each agent (individual or group) can recall
all of their historical knowledge and has memories. The main result of the study is completeness, and it can be proved by using canonical
t
t
model that S5 C is complete with respect to the class of all equivalence and monotone decreasing frames.
t
t
Key words: temporal epistemic logic; system S5 C ; perfect recall; recall axioms
诞生于 20 世纪 60 年代的认知逻辑(epistemic logic),是刻画多主体关于知识推理的有力工具.从语义上看,
认知逻辑仅仅是对模态逻辑中的必然算子进行了新的解释,在模型上并未涉及到变化,因而它是一种静态的逻
辑刻画.然而世界本身是变化的,主体对于世界的认识也会随着时间发生变化.如何刻画多主体关于世界认识的
动态变化?其中一种方法是在认知逻辑的基础上加入时间部分,由此形成了时态认知逻辑(temporal epistemic
logic,简称 TEL),其动态性特点体现为在不同的时间点上成立不同的公式.广义上的 TEL 可以分为两类:第 1 类
[1]
是为每个认知算子加入一个绝对时间点,代表人物是日本学者 Sato ,他首次给出一个结合时间与认知的正规
化形式系统;第 2 类是将各种类型的时态算子,如 F(future),O(next time),□(always),U(until)等,与认知算子置于
同一个逻辑中,但两类算子均独立出现 [2−7] .TEL 的应用领域主要在分布式系统、人工智能、信息安全和博弈论
[8]
等 .20 世纪 90 年代,计算机界开始关注 TEL 的模型检测问题,如今已经形成 MCK,MCMAS,OBDD,DEMO 等

∗ 基金项目: 国家社会科学基金(14ZDB016)
Foundation item: National Social Science Foundation of China (14ZDB016)
收稿时间: 2018-12-16; 修改时间: 2019-05-05; 采用时间: 2019-06-20; jos 在线出版时间: 2019-12-05
CNKI 网络优先出版: 2019-12-05 14:53:15, http://kns.cnki.net/kcms/detail/11.2560.TP.20191205.1453.001.html