时间自动机可达性分析中的状态空间约减技术综述

被引：3

作者：

陈铭松

赵建华

李宣东

郑国梁

机构：

[1] 南京大学计算机软件新技术国家重点实验室,南京大学计算机科学与技术系

来源：

计算机科学 | 2006年 / 06期

关键词：

实时系统; 时间自动机; 状态空间爆炸; 可达性分析;

D O I：

暂无

中图分类号：

TP301.1 [自动机理论];

学科分类号：

081202 ;

摘要：

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可达性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。

引用

页码：1 / 6+100 +100

页数：7

共 12 条

[1]

Partial-order methods for the verification of concur-rent systems:an approach to the state-explosion problem. Godefroid P. LNCS1032 . 1996

[2]

Removing Ir-relevant Atomic Formulas for Checking Ti med Automata Effi-ciently. ZHAOJianhua,LI Xuandong,ZHENG Tao,et al. Proc.of First International Workshop on Formal Modeling and Analysis of Ti med Systems(FORMATS) . 2003

[3]

Graph-Based Algorithms for Boolean Function Ma-nipulation. Bryant R E. IEEE Transactions on Communications . 1986

[4]

Partial order reductions for ti med systems. Bengtsson J,Jonsson B,Lilius J,et al. Proc.of9th International Conference on Concurrency Theory(CONCUR’98) . 1998

[5]

RED:Model-Checker for Ti med Automata with Clock-Restriction Diagram. Wang Farn. Proc.of Workshop on Real-Ti me Tools,Aalborg University . 2001

[6]

RED:Model-Checker for Ti med Automata with Clock-Restriction Diagram. Wang Farn. Proc.of Workshop on Real-Ti me Tools,Aalborg University . 2001

[7]

Reducing the number of clock variables of ti med automata. Daws C,,Yovine S. Proc.of the17thIEEE Real-Ti me Systems Symposium(RTSS’96) . 1996

[8]

Clock Difference Dia-grams. Larsen K G,Weise C,Wang Yi,et al. Nordic Journal of computing . 1999

[9]

Uppaal-Present and Future. Behrmann G,David A,Larsen K G,et al. Proc.of the40thIEEE Conference on Decision and Control(CDC’2001) . 2001

[10]

Atheory of ti med automata. Alur R,Dill D. Theoretical Com-puter Science(TCS) . 1994

← 1 2 →