时间自动机可达性检测方法研究

来源 :郑州大学 | 被引量 : 0次 | 上传用户:yanji0708
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
时间自动机是具有时间约束的有限状态转换系统,在实时系统进行形式化证明的过程中,先用它建模,然后再检验某些不安全状态是否可达。所以研究时间自动机及其验证技术,主要研究它的状态可达性问题。然而由于在它的语义描述中时间自动机的状态是无穷的,因而计算它的状态可达性关系显得尤为复杂。时间自动机中各时钟的值可以取连续的正实数值,为状态可达性关系的计算带来了许多不便,所以本文在R.Alur和D.L.Dill提出的时间转换系统等价转化的基础上给出了在时间自动机中可以通过等价转化将所有的时钟约束转化为仅含有整数值约束常量的约束,并且分析了这种转化对时间自动机两类转换的影响及其等价性证明。求解时间自动机状态可达性关系的关键问题在于对各个时钟的时间约束关系的处理。R.Alur和D.L.Dill提出的域自动机构造方法通过对状态空间进行等价划分构造有限自动机,然后通过对有限自动机的分析求解状态可达性关系。JohanBengtsson提出了含有形如x-y~n(其中,~∈{<,>,=,≤,≥})的时间自动机状态可达性关系的计算方法。Felice Balarin提出的近似计算方法实际上计算出的只是可达状态集的超集,这种超集有时候会证明一个正确的系统是不正确的,但是它不会使得一个不正确的系统被证明是正确的。Catalin Dima将复位点语义应用于时间自动机,通过对原子关系的合成、并和自反传递闭包进行运算求解可达状态集。本文研究分析了上述几种求解方法。然后针对符号化的时间自动机语义在对所有大于时钟约束常量最大值的那些时钟值进行等价处理时不能处理形如x-y~n的时钟约束这种情况,提出了一种改进算法,这种算法将两个不同时钟之间的相互约束看成一个独立的时钟来处理,在进行等价处理之前,首先求出所有任意两个时钟之间的约束的最大常量矩阵,然后据此矩阵再求解时间自动机的可达状态集便可以得出正确的结果。本文通过分析指出了这种改进算法的可行性及正确性。这种算法的优点在于,它不仅考虑到了任意两个时钟约束的最大常量,而且此算法还具有一定的通用性。
其他文献
未登录词的识别是汉语自动分词的难点之一,而中文机构名是未登录词的一个重要部分,涉及广泛,种类繁多,形态各异,且绝大多数未收入到词典中。中文机构名的自动识别对提高汉语自动分
有时间窗约束的车辆路径问题(VRPTW)是近几十年来运筹学、应用数学、网络分析、图论、计算机应用及交通运输等学科研究的一个热点问题。VRPTW问题作为一个NP(Non-determinist
可扩展访问控制标记语言XACML(eXtendible Access Control Markup Language)是一种专门用于描述安全访问控制策略,具有可扩展性、可重用性、分布式和描述能力强等特点的语言
随着网络的迅猛发展,计算机技术的不断革新,以及PC机的普及,通过网络,计算机共享信息已经成为可能,但是由于信息化发展的不平衡,造成了信息资源的不一致,加上网络本身的复杂性给信息
在自然语言处理中,词性标注是最基础的课题。由于基于统计的方法具有不需要人工总结语言学规则、识别正确率高等优点,已逐渐成为研究的热点。在基于统计的方法中,隐马尔可夫模型
随着微电子技术和计算机技术的发展,实时电路可重构技术(动态重构)逐渐成为国际上计算系统研究中的一个新热点。它的出现使过去传统意义上硬件与软件的界限变得模糊,让软件拥
随着机器人技术的不断发展,对于移动机器人的研究也越来越多。同步定位和地图构建(Simultaneous Localization and Mapping,SLAM)问题是移动机器人实现真正自主的基础。目前
在电信事业蓬勃发展的今天,综合化、分布化、智能化已经成为电信网络管理技术发展的方向。电信管理网(Telecommunications Management Network,TMN)作为一个国际通行的电信管理
对于人员聚集场所,人员疏散的过程中存在很大的安全引患。采用最佳疏散方案在最短时间让人员到达安全场所,才能让更多的人避免死亡。对公共场所的人群疏散进行计算机仿真是具有
无线移动自组网(Ad Hoc)是一种特殊的无线移动通信网络,网络中的所有移动终端地位平等、自组织、无需事先布置任何网络设施或中心控制节点,具有网络拓扑结构动态变化、网络带宽