主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
易锦,张文辉.从基于迁移的扩展Büchi自动机到Büchi自动机.软件学报,2006,17(4):720-728
从基于迁移的扩展Büchi自动机到Büchi自动机
Efficient Translation from Transition-Based Generalized Büchi Automata to Büchi Automata
投稿时间:2004-11-22  修订日期:2005-10-27
DOI:
中文关键词:  模型检测  Büchi自动机  LTL(linear temporal logic)公式  TGBA(transition-based generalized Büchi automaton)
英文关键词:model checking  Büchi automata  LTL (linear temporal logic)  TGBA (transition-based generalized Büchi automaton)
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60223005, 60373050, 60421001, 60573012 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973))
作者单位
易锦 中国科学院,软件研究所,计算机科学重点实验室,北京,100080
中国科学院,研究生院,信息与工程学院,北京,100049 
张文辉 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
摘要点击次数: 3077
全文下载次数: 3236
中文摘要:
      目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.
英文摘要:
      The automata-theoretic approach is one of the state-of-the-art model-checking methods, which consists of the following steps: use a Büchi automaton to represent the abstract system model; use an LTL formula to express the properties to be verified; translate the negation of the LTL formula to a Büchi automaton and check whether the intersection of sentences accepted by the two automata is non-empty. One type of methods for translating LTL formulas to Büchi automata has one step for calculating transition-based generalized Büchi automata (TGBA) and another step for translating TGBA to Büchi automata. This paper redefines the product operation of TGBA according to the characteristics of the accepting language of Büchi automata. This leads to the reduction of the number of states that need to be copied and therefore smaller Büchi automata. The experimental results given at the end of this paper demonstrate the advantage of the approach based on test cases with randomly generated formulas.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利