一种模态逻辑转换成状态迁移系统的方法

摘要

本发明提供一种模态逻辑转换成状态迁移系统的方法，属于计算机系统检测领域。包括：定义一种特殊的公式即交替公式；应用已知的性质以逻辑推导的方式推出其具有推迟的特殊性质；针对这一特殊性质定义一套新的优化规则；应用特殊性质及优化规则应用于线性时序逻辑到状态迁移系统的转换过程的某些步骤之中。在转换过程中逐步实现状态迁移系统的缩小和确定化。相较于传统的转换方法，本方法可以生成更小的状态空间，获得更确定化的迁移关系，尤其当参数较多时，往往拥有更快地转换速度。因此，提高了模型检测在应用到计算机硬件、通信协议、控制系统、安全认证协议等方面进行分析与验证时的速度、效率，保证了其质量，有良好的社会效益。