多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。

多视点间不一致性的认知推理

需求工程可以认为是一个知识表示,知识获取和知识分析的过程.多视点需求工程就是希望复杂系统中的不同参与者分别从自己的角度出发对预期系统进行描述,从而形成更完备的需求规约.由于多视点方法的这种特性,导致多个涉众有可能对同一问题进行描述,从而形成重叠的需求.这些重叠的需求就是涉众之间的公共知识,对公共知识的不同解释是导致需求规约中不一致问题的根源.本文对基于问题域的多视点需求建模框架进行基于时序认知逻辑的解释和推理,期望达到以下目的:1)使用户陈述的需求更加结构化;2)使用形式化的方法帮助涉众发现那些重叠的需求.