中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
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-模拟方法的一个改进。
英文摘要: Model checking is one of important formal verification methods. The procedure normally uses an exhaustive search of the state space of the system, then determines whether some specification is true or not. So the main disadvantage of model checking is state explosion problem. In the algorithm of LTL model checking, we transform both the model of a system and an LTL formula to Büchi automata, so efficient state space reduction for Büchi automata is very significant to react state explosion problem. The thesis is about how to optimize the procedure from LTL to Büchi automata and how to optimize a given Büchi automaton. From LTL to Büchi automata, there are two types of methods: based on the tableau rule or alternating automata. In each type, there exists the algorithm using transition-based generalized Büchi automaton(TGBA) as a medium. So from TGBA to Büchi automata affects the whole transformation process. In the thesis, we re-define the product operator according to the characteristic of accepting language, and get a Büchi automaton with fewer states and transitions. Given a Büchi automaton, we can optimize it by language containment relation or all kinds of simulation relations for automata. In the thesis, we define language equivalence class which is the set of states with the same language, and show how to use this definition to delete states. In a sense, language equivalence class helps us to reduce the number of states as more as possible. Additionally, based on fair simulation and language containment, we propose an efficient way to reduce state space. It reduces states and transitions according to the reachability of states or by fair simulation method which uses the more restricted criteria to check the correctness. Therefore, we not only preserve the language of each state of the original, but do the reduction as soon as finding one suitable pair of states, so we need not find all candidates in advance before any optimization. Since two states with fair simulation is a sufficient but not necessary condition for language containment.In order to enhance fair simulation for checking language containment, we present an approach by building a Büchi automaton based on marked-k-subset construction which limits the number of states in a subset less than k. The new automaton preserves the language of the original and has a structure that helps identify more pairs of states with fair simulation. This approach is an improvement to the fair-k-simulation method.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7324
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200318015003106易锦_paper.pdf(1395KB)----限制开放-- 联系获取全文

Recommended Citation:
易锦. Büchi自动机状态空间的化简[D]. 软件研究所. 中国科学院软件研究所. 2007-06-03.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[易锦]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[易锦]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace