有限状态机逻辑阻塞检测

统一判据与搜索算法

基于半张量积将有限状态机建模为逻辑系统，首次给出可计算判定准则并搜索全部逻辑阻塞。

闫永义 · Penglei, Hao · 岳菊梅 · 李海涛 · 冯俊

Science China Information Sciences 2024

技术优势

阻塞可判定

对给定有限状态机，通过检验环路结构即可判断是否存在逻辑阻塞。

全部阻塞可枚举

若存在阻塞，设计的算法能找出所有逻辑阻塞，而不是只给出一个例子。

非确定 FSMs 也适用

结果扩展至非确定有限状态机乃至 FSM 网络，覆盖面更广。

应用场景

• 离散事件系统：用代数判据分析事件序列驱动的系统阻塞，替代仿真试错。
• 可编程控制器验证：将 PLC 程序建模为 FSM，系统搜索无法继续的逻辑状态。
• 通信协议分析：检测状态机协议中可能进入的阻塞状态，确保消息序列可行。
• 机器人任务规划：检查任务规划中的 FSM 模型是否有无法继续执行的逻辑阻塞。