Büchi自动机状态空间的化简
文献类型：学位论文
| 作者 | 易锦 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-03 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 模型检测 状态爆炸 LTL Büchi自动机 公平模拟 |
| 其他题名 | State Space Reduction of Büchi Automata |
| 中文摘要 | 模型检测是形式化验证的一种重要方法。它主要是通过对状态空间的穷尽搜索来检查系统是否满足给定的性质。因此，状态爆炸是模型检测所面临的一个重要问题。 在LTL（Linear Temporal Logic）模型检测方法中，由于系统模型和LTL公式所描述的性质都需要转换为Büchi自动机并求交，因此如何有效地化简Büchi自动机的状态空间，对缓解状态爆炸问题有着重要的意义。 本文主要包含两个方面的工作： （1）针对LTL到Büchi的转换过程进行化简。 （2）对给定的Büchi自动机进行化简。 目前，从LTL到Büchi自动机的转换算法主要分为两类：基于tableua规则的算法和alternaing自动机的算法。而在这两类方法中，都存在以基于迁移的扩展自动机（TGBA）作为中间转换结果的算法，因此化简TGBA到BA的转换过程可以提高整个转换算法的化简效果。在本文，我们根据自动机可接受语言的特点，重新定义了转换过程中的求交运算，使转换后所得Büchi自动机具有较少的状态和迁移个数。 给定一个Büchi自动机，我们可以根据状态间的语言包含关系或是自动机的各种模拟关系来化简自动机。在本文，我们将自动机上所有具有相同可接受语言的状态集合称为语言等价类，并说明如何在等价类上删除状态。等价类的定义有利于尽可能多地减少自动机状态个数。 在基于语言包含关系和自动机公平模拟关系化简自动机的基础上，我们提出了一个有效的化简Büchi自动机的算法。该方法既可以利用状态之间的可达关系来直接化简状态和迁移，也可以在利用公平模拟关系时，根据一个更严格的检查化简正确性条件来化简自动机。这样，该方法不但可以保证每个状态在化简前后的可接受语言保持不变，而且还实现了一旦找到合适的候选状态对，就立即进行化简的方式。这样我们总是从化简了的自动机上查找状态对，而不必在原自动机上找到所有的候选对后，才能进行化简。 由于两个状态具有公平模拟关系是这两个状态具有语言包含关系的充分而非必要条件，因此，为了使公平模拟关系更接近语言包含关系，我们定义了标记-k-子集构造法，它限制了每个子集的状态个数最多为k。给定一个Büchi自动机，根据该构造法我们可以生成了一个新的Büchi自动机，该自动机不但可以保持原自动机的可接收语言，而且其结构有利于找到更多具有模拟关系的状态对，从而使得公平模拟关系更接近语言包含关系。最后，我们证明了该方法是对公平-k-模拟方法的一个改进。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 122 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7324]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 易锦. Büchi自动机状态空间的化简[D]. 软件研究所. 中国科学院软件研究所. 2007. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。