首页 | 官方网站   微博 | 高级检索  
     

一种动态消减时间自动机可达性搜索空间的方法
引用本文:陈铭松,赵建华,李宣东,郑国梁.一种动态消减时间自动机可达性搜索空间的方法[J].计算机科学,2007,34(1):213-218.
作者姓名:陈铭松  赵建华  李宣东  郑国梁
作者单位:南京大学计算机软件新技术国家重点实验室,南京大学计算机科学与技术系,南京,210093
基金项目:国家自然科学基金 , 国家重点基础研究发展计划(973计划)
摘    要:时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成,时间区域用形如x-y≤(〈)n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中,分析算法将生成大量的符号状态,往往导致对计算机内存的需求超出了可行的范围。本文给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析,在不影响分析结果的前提下消去某些时间区域的原子公式,从而扩展符号状态。扩展后的符号状态包含有更加多的其它的状态,通过删除掉那些被包含的符号状态可以减少算法存储的状态个数,节省存储空间。本文最后给出了相关的案例分析,结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间。

关 键 词:时间自动机  模型检验  符号状态  时间区域

An Algorithm to Dynamically Reduce the State Space of Timed Automata during the Reachability Analysis
CHEN Ming-Song,ZHAO Jian-Hua,LI Xuan-Dong,ZHENG Guo-Liang.An Algorithm to Dynamically Reduce the State Space of Timed Automata during the Reachability Analysis[J].Computer Science,2007,34(1):213-218.
Authors:CHEN Ming-Song  ZHAO Jian-Hua  LI Xuan-Dong  ZHENG Guo-Liang
Affiliation:National Laboratory of Novel Software Technology, Department of Computer Science and Technology, Nanjing University, Nanjing 210093
Abstract:
Keywords:Timed automata  Model checking  Symbolic state  Time zone
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司    京ICP备09084417号-23

京公网安备 11010802026262号