一种混成系统的可达性分析方法

摘要

本发明提出一种混成系统的可达性分析方法，包括以下步骤：解析混成自动机输入文件，将该自动机的有界图结构编码成一组命题逻辑公式集合；利用SAT求解器对该公式集合进行求解，若不可解则输出结果不可解，如果可解则将可满足赋值解码成输入自动机图结构上的一条路径；根据混成自动机的语义对目标路径进行编码形成线性约束；对该线性约束求解，如果可解则输出该路径作为结果，否则转下一步；给出线性约束的不可约不可解集合；将不可达路径编码成一组命题逻辑公式集合并加到自动机图结构的公式集合里。采用本发明方法可快速找出到达目标节点的候选路径，减少对混成自动机图结构进行搜索的时间。