混合系统的近似形式化验证

• 作 者: 余琼
• 出 处: 广西民族大学
• 发表日期: 2016年01期
• 关键词: 特殊标记 等价的标记转换系统 近似标记转换系统 齐次线性多项式微分混合系统 误差分析

混合系统是由连续子系统和离散子系统构成,且这两个子系统相互作用相互影响,从而使得混合系统表现出更加复杂的动态行为。而混合系统中研究的一个重点内容是系统的形式化验证。但是由于系统的形式化验证条件非常苛刻,从而很难对系统进行形式化验证。为了验证混合系统,了解混合系统的一些特性,我们对混合系统采取近似形式化验证。因此,我们主要研究了特殊混合系统的语义模型及其近似语义模型,并进行了误差分析。我们是通过不完全矩阵分解法和特殊标记来研究混合系统,即把系统的标记特殊化为齐次线性多项式微分方程组,利用不完全矩阵分解法得到此方程组矩阵的预处理矩阵,并根据预处理矩阵建立了标记的等价标记和等价标记集。根据标记的等价语义模型以及不完全矩阵分解法,我们构造了状态的近似状态,并且建立了标记转换系统的等价标记转换系统语义模型和近似标记转换系统语义模型。根据标记特殊化为齐次线性多项式微分方程组,提出了齐次线性多项式微分混合系统语义模型。齐次线性多项式微分混合系统不仅刻画了状态之间的转换行为,而且还描述了状态转换的细节。本论文还构造了齐次线性多项式微分混合系统的近似状态轨迹和近似动作序列以及近似语义模型。而且也构建了系统的离散转换关系的近似转换关系。随后,本论文对系统进行了误差分析。从而我们得出了状态及其近似状态、状态轨迹到达状态及其近似状态轨迹到达状态、标记及其近似标记、动作序列及其近似动作序列、状态轨迹及其近似状态轨迹之间的绝对误差。