定性推理在矩形phase-portrait近似中应用.pdfVIP

定性推理在矩形phase-portrait 近似中的应用1 刘保罗，裴海龙，李坚强 华南理工大学自动化科学与工程学院，广州（510640 ） E-mail：ieliubl@163.com 摘 要：抽象近似是验证混合系统安全性的主要方法，矩形phase-portrait 近似是通过构造简 单的线性混合自动机来近似原混合自动机。phase-portrait 近似的关键步骤是如何划分状态空 间，本文采用定性推理的方法，叙述了如何根据系统动态特征来划分状态空间及如何精化抽 象模型。 关键词：混合自动机；phase-portrait 近似；李导数 中图分类号：TP27 1. 引 言 混合系统是连续变量过程和离散事件过程并存且相互交换信息的动态系统，如数字嵌入 式系统。安全性保证是混合系统设计的主要要求之一，由于混合系统涉及复杂的连续动态及 离散动态，安全性验证的可判定性仅限于一些简单混合系统，如时间自动机，矩形自动机等， 对于大多数混合系统，安全性问题是不可判定的[1] 。基于这个问题，研究者提出了许多种方 法，旨在寻找验证安全性的充分条件。T.A. Henzinger 提出phase-portrait 近似概念，这种方 法是利用抽象的方法将复杂的混合动态模型转化为简单的可计算自动机模型, 如线性自动 机(LHA) 。 Phase-portrait近似的关键是控制模态空间的划分，它直接影响着近似自动机模拟原系统 的程度。虽然文献[4] 中给出了Phase-portrait近似的完备性，但盲目的划分可能由于抽象模型 的精化而引起模态数目的剧增，因此如何划分是运用这种方法的关键。本文基于这种考虑， 采用定性推理[2] 的方法，叙述了一种基于动态特性的模态空间划分方法。本文所考虑的对象 为分段仿射混合系统。 2. 基本术语 X {x ,,x } y ≡a +Σ a x i x ∈X i i 假定 1 n 是有限变量集，X 上的线性项定义为表达式 i ，其 中ai ∈Q。线性项集合表示为L Term( X ) 。线性约束为公式y ~ 0 ，其中y ∈Lterm (X ) ， ~∈≤≥={ , , , , } 。线性谓词定义为线性约束的合取。X 上的线性谓词集表示为Lin( X ) 。实 l ≤x ≤r l ∈R r ∈R 数域上的闭区间I 定义为公式 I I ，其中 I ， I 分别称为区间的左端点和右 ∧ x ∈I I (x ∈X ) x ∈X i x x i 端点。X 上的矩形谓词定义为公式 i i ，其中 i 是实数域上的闭区间。X Re ct( X ) ∧ x t x ∈X i x 上的矩形谓词公式集表示为 。 X 的仿射动态定义为： i i ，其中