论文部分内容阅读
由于经典的线性时序逻辑表达能力有限,设计并开发了基于交替投影时序逻辑(alternating projectiontemporal logic,简称APTL)的模型检测工具.根据王海洋等人提出的APTL 符号模型检测方法,设计并实现了APTL模型检测器MCMAS_APTL.该工具可用于多智能体系统(multi-agent system,简称MAS)的性质验证.MCMAS_APTL 检查MAS 是否满足具体性质的过程如下:首先,用解释系统编程语言(interpreted system programming