Please wait a minute...
 首页  期刊介绍 期刊订阅 联系我们 横山亮次奖 百年刊庆
 
最新录用  |  预出版  |  当期目录  |  过刊浏览  |  阅读排行  |  下载排行  |  引用排行  |  横山亮次奖  |  百年刊庆
清华大学学报(自然科学版)  2014, Vol. 54 Issue (2): 281-288    
  论文 本期目录 | 过刊浏览 | 高级检索 |
线性时序逻辑转换Büchi自动机的按需即时算法
单来祥1,覃征1,2(),卢欣晔3,卢正才1
2. 清华大学 软件学院, 北京 100084
3. 中国科学院 软件研究所, 北京 100190
On-the-fly translation algorithm from linear temporal logic to Büchi automata
Laixiang SHAN1,Zheng QIN1,2(),Xinye LU3,Zhengcai LU1
1. Tsinghua National Laboratory for Information Science and Technology, Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
2. School of Software, Tsinghua University, Beijing 100084, China
3. Institute of Software Chinese Academy of Sciences, Beijing 100190, China
全文: PDF(1206 KB)   HTML
输出: BibTeX | EndNote (RIS)       背景资料
文章导读  
摘要 

将线性时序逻辑公式转换成Büchi自动机是显式模型检测中的关键环节, Tableau规则是常用转换算法。该文提出了基于Tableau规则的改进算法,将线性时序逻辑公式转换成基于迁移的Büchi 自动机。通过在状态和迁移中加入U公式的满足信息,实现了用一个接受条件集合判断执行序列是否可接受,避免了使用多个接受条件集合进行判断。改进算法引入了按需即时(on-the-fly)去扩展化机制,算法展开状态节点的同时进行状态有效性检测,删除无效节点,合并等价状态和迁移,避免了后置化简。与其他转换工具进行比较实验表明,该算法具有执行速度快、生成自动机的状态数和迁移数少的特征。

服务
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章
单来祥
覃征
卢欣晔
卢正才
关键词 线性时序逻辑基于迁移的Büchi自动机按需即时    
Abstract

Translations of linear temporal logic to Büchi automata are key to explicit model checking, with the Tableau-based algorithm commonly used for the translation. This paper describes an improved Tableau-based algorithm which converts linear temporal logic to transition-based Büchi automata. The satisfaction information of the U-formula for the states and transitions is used to judge whether the automata is acceptable using only one acceptance condition set, rather than multiple sets. Thus, the algorithm gives an on-the-fly degeneralization mechanism that can expand the state nodes while detecting their validity and removing invalid nodes. The algorithm combines equivalent states and transitions and avoids simplifications after forming the final automata. Comparisons with other conversion tools show that this algorithm runs faster with less states and transitions in the automaton.

Key wordslinear temporal logic    transition-based Büchi automata    on-the-fly
收稿日期: 2013-04-25      出版日期: 2015-04-16
ZTFLH:     
基金资助:国防“十二五”预研基金重点项目 (9140A1550212JW01047);高等学校博士学科点专项科研基金优先发展领域课题 (20120002130007)
引用本文:   
单来祥, 覃征, 卢欣晔, 卢正才. 线性时序逻辑转换Büchi自动机的按需即时算法[J]. 清华大学学报(自然科学版), 2014, 54(2): 281-288.
Laixiang SHAN, Zheng QIN, Xinye LU, Zhengcai LU. On-the-fly translation algorithm from linear temporal logic to Büchi automata. Journal of Tsinghua University(Science and Technology), 2014, 54(2): 281-288.
链接本文:  
http://jst.tsinghuajournals.com/CN/  或          http://jst.tsinghuajournals.com/CN/Y2014/V54/I2/281
  Tableau规则
  LTTB算法
  无效节点
  (ab)∪c展开为TGBA
  (ab)∪c展开为TBA
LTL
公式
LTL3BA SPOT LTTB 转换时间/s
状态数 迁移数 状态数 迁移数 状态数 迁移数
φG5 36 441 36 441 36 441 0.031
φG6 49 784 49 784 49 784 0.471
φG7 64 1 296 64 1 296 64 1 296 0.915
φG8 81 2 025 81 2 025 1.128
φG9 100 3 025 1.691
φS5 5 15 5 15 5 15 0.002
φS6 6 21 6 21 6 21 0.003
φS7 7 28 7 28 7 28 0.004
φS8 8 36 8 36 8 36 0.004
φS9 9 45 9 45 9 45 0.005
φO5 25 225 25 225 25 225 0.027
φO6 36 441 36 441 36 441 0.170
φO7 49 784 49 784 0.341
φO8 64 1 296 64 1 296 0.946
φO9 81 2 025 1.733
φP5 6 11 6 11 6 11 0.001
φP6 7 13 7 13 7 13 0.002
φP7 8 15 8 15 8 15 0.002
φP8 9 17 9 17 9 17 0.003
φP9 10 19 10 19 10 19 0.003
φC5 6 26 6 26 5 10 0.020
φC6 7 34 7 34 6 12 0.036
φC7 8 43 8 43 7 14 0.070
φC8 9 53 9 53 8 16 0.136
φC9 10 64 10 64 9 18 0.359
  LTL3BA、SPOT与LTTB比较实验结果
[1] Gerth R, Peled D, Vardi M Y, et al.Simple on-the-fly automatic verification of linear temporal logic [C]//Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification. Seneca, USA: IFIP, 1995.
[2] Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295.
[3] Daniele M, Giunchiglia F, Vardi M Y. Improved automata generation for linear temporal logic [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer 1999: 249-260.
[4] Giannakopoulou D, Lerda F. From states to transitions: Improving translation of LTL formulae to Büchi automata [C]//Formal Techniques for Networked and Distributed Sytems, FORTE 2002. Berlin, Heidelberg, Germany: Springer, 2002: 308-326.
[5] Duret-Lutz A. LTL translation improvements in spot [C]//Proceedings of the 5th International Conference on Verification and Evaluation of Computer and Communication Systems. Swinton, UK: British Computer Society, 2011: 72-83.
[6] Shoshmina I V, Belyaev A B. Symbolic algorithm for generation Büchi automata from LTL formulas [C]//Parallel Computing Technologies. Berlin, Heidelberg, Germany: Springer, 2011: 98-109.
[7] Gastin P, Oddoux D. Fast LTL to Büchi automata translation [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2001: 53-65.
[8] Babiak T, Kretínsky M, Rehák V, et al.LTL to Büchi automata translation: Fast and more deterministic [C]//Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg, Germany: Springer, 2012: 95-109.
[9] Fritz C. Concepts of automata construction from LTL [C]//Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg, Germany: Springer, 2005: 728-742.
[10] Boker U, Kupferman O, Rosenberg A. Alternation removal in Büchi automata [C]//Automata, Languages and Programming. Berlin, Heidelberg, Germany: Springer, 2010: 76-87.
[11] Juvekar S, Piterman N. Minimizing generalized Büchi automata [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2006: 45-58.
[12] Somenzi F, Bloem R. Efficient Büchi automata from LTL formulae [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2000: 248-263.
[13] Etessami K, Holzmann G J. Optimizing Büchi automata [C]//CONCUR 2000: Concurrency Theory. Berlin, Heidelberg, Germany: Springer, 2000: 153-168.
[14] Yin C, Luo G. Efficient translation of LTL to Büchi automata[J].Tsinghua Science & Technology, 2009, 14(1): 75-82.
[15] Sebastiani R, Tonetta S. “More deterministic” vs.“smaller” Büchi automata for efficient LTL model checking [C]//Correct Hardware Design and Verification Methods. Berlin, Heidelberg, Germany: Springer, 2003: 126-140.
[16] Ehlers R, Finkbeiner B. On the virtue of patience: Minimizing Büchi automata [C]//Model Checking Software. Berlin, Heidelberg, Germany: Springer, 2010: 129-145.
[17] Lu X, Luo G. Direct translation of LTL formulas to Büchi automata [C]//2012 IEEE 11th International Conference on Cognitive Informatics & Cognitive Computing (ICCI*CC). Bratislava, Slovak: IEEE Press, 2012: 323-328.
[1] 龙奋杰, 龙振兴, 王萧濛. 产权约束对景气市场住房报价的影响——基于Stein模型的改进与数值模拟[J]. 清华大学学报(自然科学版), 2014, 54(5): 596-601.
[2] 杨宏伟, 王昊宇, 刘云霞, 刘文君, 杨少霞. O3-BAC工艺对含溴水体消毒副产物生成势的影响[J]. 清华大学学报(自然科学版), 2014, 54(5): 607-612.
[3] 林朋飞, 张晓健, 陈超, 汪隽. 含钼废水处理及饮用水应急处理技术及工艺[J]. 清华大学学报(自然科学版), 2014, 54(5): 613-618.
[4] 闵琪, 段远源, 王晓东. 格子Boltzmann模型结合MPR方程模拟流体饱和气液密度[J]. 清华大学学报(自然科学版), 2014, 54(5): 619-623.
[5] 郝琛, 李富, 郭炯. 球床式高温气冷堆球流混流的模拟[J]. 清华大学学报(自然科学版), 2014, 54(5): 624-628.
[6] 江锋, 庄子威, 张振中, 尉继英. 用于HEPA滤料效率检测的蒸发冷凝技术[J]. 清华大学学报(自然科学版), 2014, 54(5): 629-632.
[7] 邓可欣. 基于超边图匹配的视网膜眼底图像配准算法[J]. 清华大学学报(自然科学版), 2014, 54(5): 568-574.
[8] 杨汉波, 吕华芳, 胡庆芳, 雷慧闽, 杨大文. 华北平原的大气逆辐射参数化方法比较[J]. 清华大学学报(自然科学版), 2014, 54(5): 590-595.
[9] 曹欣荣, 刘蕾, 蔡东阳, 郭鹏, 唐劲天. 心冲击图特征统计及其医学诊断应用[J]. 清华大学学报(自然科学版), 2014, 54(5): 633-637.
[10] 张明立, 任淑霞. 参与情境下顾客心理感知对关系利益的实证检验[J]. 清华大学学报(自然科学版), 2014, 54(5): 664-671.
[11] 何平, 吴添, 姜磊, 伍良杰. 投资者情绪与个股波动关系的微观检验[J]. 清华大学学报(自然科学版), 2014, 54(5): 655-663.
[12] 徐悟, 于清, 尧国皇. 初应力对钢管混凝土叠合柱轴压性能影响[J]. 清华大学学报(自然科学版), 2014, 54(5): 556-562.
[13] 魏亚, 姚湘杰. 约束状态下混凝土拉伸徐变模型[J]. 清华大学学报(自然科学版), 2014, 54(5): 563-567.
[14] 王振波, 张君, 罗孙一鸣. 喷水法成型纤维网增强水泥基板材抗弯性能[J]. 清华大学学报(自然科学版), 2014, 54(5): 551-555.
[15] 赵娜, 王兆印, 潘保柱, 李志威, 段学花. 小江流域不同强度河床结构的生态学作用[J]. 清华大学学报(自然科学版), 2014, 54(5): 584-589.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
版权所有 © 《清华大学学报(自然科学版)》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn