实时随机系统的分析诊断与控制研究

发布时间：2022-01-01 19:06

　　保证计算机系统的正确性和可靠性是计算机研究和开发人员的首要任务。模型检测是保证计算机系统正确性和可靠性的有力手段。当人们对复杂系统进行建模和分析时,往往需要考虑到事件发生的不确定性、发生事件的时限和完成事件所付出的代价等因素,实时随机系统模型检测就是研究这类情况下的模型检测问题。实时随机系统模型检测是诞生于二十世纪九十年代的一个活跃的研究领域,目前已取得很多重要的理论研究成果,并取得广泛的实际应用。为验证实时随机系统的行为是否满足一定性质的要求,可以采用模型检测的方法。如果系统的行为不满足性质的要求,可生成相应的反例。进一步地,为控制含不确定性的系统的行为,可以根据系统的模型和性质的要求,合成适当的控制器,以控制系统的运行。本文正是围绕实时随机系统的分析、诊断与控制,开展了一定的研究。实时随机系统的典型模型包括离散（连续）时间Markov链、离散（连续）时间Markov决策过程、概率时间自动机。本文围绕离散（连续）时间Markov决策过程、概率时间自动机及其扩展模型,开展了如下研究:1、面向概率时间自动机的两个扩展模型—代价概率时间自动机和区间概率时间自动机,研究了模型检测问题:（1）... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：88 页

【学位级别】：博士

【部分图文】：

一个建模网络协议的概率时间自动机

使用连续时间 Markov 链表示一个数据传输系统某节点的工路径 CTMC 中的一条无限路径σ 是一个状态和22...ts → ，其中对于 i ∈ ，is ∈ S，且i0t>∈ ，使CPath 描述 CTMC C 中路径的集合。当ks 为一个吸收状条有限路径。允许范围。令 [ ]iσ i = s， ( , )iδ σ i ∈ I。用,0 1( ,..., , )k kC s I I s 区间为 Ii的有限路径。以 Ω ( Path)表示包含各个,0 ( ,..C s I 由一个初始分布α 在路径上产生的概率度量记为Prα。地定义为[4]：0( s)= α，( ) ( , , 0 0,..., ', ')) Pr ( ( ,..., )) ( , ') ( k E s a E sk k k s I s C s I s P s s e eα = sup I'。（当b = ∞且 λ > 0时，令 e0 λ ∞= ）率分为瞬态概率和稳态概率两种。瞬态概率是系统在给定在达到平衡时的概率。瞬态概率的定义可形式化地描述为'C C

' [ : 0]( , ')X rp r lυ υ ∧ = =。自动机的语法定义和语义描述可见，一个代价概率概率分支扩展，也可看作是概率时间自动机的概率示为一个具有时钟 x的 P2TA。其中，每个圆圈代表的代价变化速率和不变式，包含在圆圈中。从一个或单一的边。基于概率的边，包含若干概率分支。选上。每个边上包含卫士、代价和待复位时钟变量。当率为 1 时，也忽略不写。设自动机的初始位置为 l0位于一个位置时，若满足该位置的不变式条件，可代价也相应增加。设停留时间为d ，代价变化速率上的卫士时，自动机从一个位置跃迁到下一个位置的增长为h。

【参考文献】：
期刊论文
[1]模型检测基于概率时间自动机的反例产生研究[J]. 张君华,黄志球,曹子宁.  计算机研究与发展. 2008(10)
[2]基于Horn逻辑扩展模型的安全协议反例的自动构造[J]. 周倜,李梦君,李舟军,陈火旺.  计算机研究与发展. 2007(09)



本文编号：3562658