一种动态消减时间自动机可达性搜索空间的方法

计算机科学 ›› 2007, Vol. 34 ›› Issue (1): 213-218.

• 计算机网络与信息安全 • 上一篇下一篇

一种动态消减时间自动机可达性搜索空间的方法

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本课题研究得到国家自然科学基金（No.60573085）和国家重点基础研究973计划（No.2002CB312001）的资助.

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成，时间区域用形如x-y≤（〈）n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中，分析算法将生成大量的符号状态，往往导致对计算机内存的需求超出了可行的范围。本文给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析，在不影响分析结果的前提下消去某些时间区域的原子公式，从而扩展符号状态。扩展后的符号状态包含有更加多的其它的状态，通过删除掉那些被包含的符号状态可以减少算法存储的状态

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

Abstract: The reachability analysis algorithm explores the state space of a timed automaton by enumeration of symbolic states. Each symbolic state consists of a location and a time zone which are conjunctions of automatic formulae in the form x-y≤（〈）n. Sometimes th

Key words: Timed automata, Model checking, Symbolic state,Time zone

. 一种动态消减时间自动机可达性搜索空间的方法[J]. 计算机科学, 2007, 34(1): 213-218. https://doi.org/