和与积数迷的符号化模型检测

和与积是一个著名的数迷问题。采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解。在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解。实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势。

离散实时线性动态逻辑的符号化模型检测

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。

基于符号化模型检测的对弈必胜策略验证

在对弈的研究中,验证对弈双方是否存在必胜策略的问题一直没能很好地解决,因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展,大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法,并给出了一个井字棋必胜策略验证的实例。

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK2.0.0.完成了MCTK与著名的符号化模型检测工具nu Xmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nu Xmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

基于UPPAAL的认知机器人控制行为建模与验证

随着机器人技术的高速发展,越来越多的人开始聚焦到认知机器人领域的研究,机器人系统中的两大研究领域主要是路径规划和任务规划,而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上,提出机器人系统的任务规划层次框架.认知机器人的大部分的控制行为需要人的参与,这就要求这类机器人系统具有在线自适应的能力,而采用传统的验证方法验证其正确性和实时性上存在一定的局限性.采用形式化方法对认知机器人系统的简单实例建模并验证几个重要的属性,采用时间自动机对系统进行形式化的描述,并结合符号化模型检测工具Uppaal进行验证.针对系统的重要属性采用计算树逻辑的形式表述.