[00275470]最小不满足树制导的混成系统可达性分析方法
交易价格：
面议
所属行业：
分析仪器
类型：
发明专利
技术成熟度：
正在研发
专利所属地：中国
专利号：CN201310146921.4
交易方式：
技术转让
技术转让
技术入股
联系人：
南京大学
进入空间
所在地：江苏南京市
- 服务承诺
- 产权明晰
-
资料保密
对所交付的所有资料进行保密
- 如实描述
技术详细介绍
本发明提出最小不满足树制导的混成系统可达性分析方法，包括以下步骤：解析混成自动机，生成该混成自动机的图结构；在混成自动机的图结构上，从初始节点开始做深度优先搜索，在每遍历一个节点前，对已遍历的路径与以该节点为根的最小不满足树进行匹配，如果匹配成功，则不遍历该节点并回溯至另外的节点进行深度优先搜索，否则遍历该节点并根据目标节点遍历出一条到达目标节点的目标路径；根据混成自动机的语义对遍历出的目标路径进行编码，形成一组线性约束；调用线性规划求解器对该组线性约束进行求解，如果可解则输出该路径作为结果，否则转下一步骤。
本发明提出最小不满足树制导的混成系统可达性分析方法，包括以下步骤：解析混成自动机，生成该混成自动机的图结构；在混成自动机的图结构上，从初始节点开始做深度优先搜索，在每遍历一个节点前，对已遍历的路径与以该节点为根的最小不满足树进行匹配，如果匹配成功，则不遍历该节点并回溯至另外的节点进行深度优先搜索，否则遍历该节点并根据目标节点遍历出一条到达目标节点的目标路径；根据混成自动机的语义对遍历出的目标路径进行编码，形成一组线性约束；调用线性规划求解器对该组线性约束进行求解，如果可解则输出该路径作为结果，否则转下一步骤。
