线性时序关系下推理的概率计量化模型

Reasoning about Uncertainty is one of the core research topics for Artificial Intelligence. As two commonly used logical deduction approaches for reasoning, Probabilistic Logic and Quantitative Logic both have limitations when dealing with complex knowledge that represents randomness as well as fuzziness. Besides, most existing reasoning mechanisms adopt propositional logic or two-valued deduction mode as their logical frames, which cannot be sufficient for the need of complex reasoning. This project aims to simultaneously introduce probabilistic and quantitative approaches into reasoning under linear time sequence. Based on random Kripke structures and dynamic model sequences, suitable measures are adopted in order to construct a method of gradedly judging validness for specifications. It includes the following special subjects: (i) Normal form and formulae simplification for linear temporal logic. (ii) Graded models for judging validness of specifications under linear time sequence. (iii) Discussion about the safety, fairness and liveness properties for reasoning systems.

不确定性推理是人工智能的核心研究课题之一。从推理的研究方法看，概率逻辑与计量逻辑是处理知识的不确定性问题时常用的逻辑推理方法，但二者面对同时带有模糊性与随机性的复杂知识时均显出各自的局限性；从推理依据的逻辑框架看，现有的推理机制多采用命题逻辑或二值式的推理模式，其表达能力已不能满足复杂推理的需要。本项目拟将概率、计量方法结合引入到时序逻辑中，针对随机Kripke语义结构构建适当的概率测度，并利用动态模型序列的时序特点给出判断规约语句有效性的程度化方法，最终建立基于线性时序关系下推理的概率计量化模型，使推理机制随时间的推进呈现动态化的特点，从而在更为宽泛的框架下展开不确定性推理研究。具体包括以下专题研究：(i)针对线性时序逻辑构造范式表示并化简公式构成；(ii)基于线性时序关系建立判断规约语句有效性的程度化模型；(iii)讨论推理系统的安全性、公平性及活跃性。

本项目针对线性时序逻辑的时序化、动态化特点，借助随机Kripke结构上的概率测度建立了时序逻辑公式的满足度理论，为时序语义背景下的逻辑推理提供了某种可行的量化手段。本项目的相关研究论文已正式发表5篇，其中SCI收录2篇、EI收录1篇，另有2篇SCI期刊论文将于2016年发表。具体研究进展与成果包括以下内容：. (i) 为了降低推理模型的复杂度，项目组针对线性时序逻辑中时态词的递归语义分别定义了公式的特征与满足集概念，以特征为指标将公式进行分类，给出了各类公式特征与满足集的递归计算方法，基于此为线性时序逻辑公式建立了统一的范式表示，从而化简了其公式构成；. (ii) 将线性时序逻辑的Kripke结构进行了随机化，为Kripke结构中的初始状态及状态间的迁移关系建立了某种适当的概率分布，引入了全体无穷初始路径之集上的概率测度，并借助该概率测度将时序公式的满足集进行了量化，最终建立了判断规约语句有效性的程度化方法；. (iii) 针对上述线性时序逻辑Kripke语义的量化框架，在满足度的基础上引入了公式间的相似度与伪距离，建立了线性时序语义的逻辑度量空间，研究了该度量空间的内蕴结构与近似推理，并将其量化方法推广至模糊度量空间上。