混合自动机多项式phase-portrait近似.pdfVIP

混合自动机的多项式phase-portrait 近似1 1 1 1,2 1 刘保罗 ，裴海龙 ，张胜祥 ，李坚强 1 华南理工大学自动化科学与工程学院，广州（510640 ） 2 华南农业大学应用数学系，广州（510640 ） E-mail：ieliubl@163.com 摘 要：抽象近似是验证混合系统安全性的主要方法，模型转换是构造一个可判定的（或半 判定的）混合自动机来近似原混合自动机。本文将线性 phase-portrait 近似推广到多项式 phase-portrait 近似，叙述了如何自动构造多项式 phase-portrait 近似自动机及如何精化近似 模型。 关键词：混合自动机；弱时间模拟；phase-portrait 近似 中图分类号：TP27 1. 引 言 混合系统是连续变量过程和离散事件过程并存且相互交换信息的动态系统,如数字嵌入 式系统。安全性保证是混合系统设计的主要要求之一，使用混合自动机做验证模型时，安全 性验证可归结为自动机的求空问题，即自动机的可达状态集与不安全区域的交集是零，因此 可达集的计算至关重要。然而，可达集的精确计算仅局限于一些简单混合系统，如时间混合 自动机，矩形自动机。对于大多数混合系统，可达集的精确计算是不可判定的，甚至是不可 计算的[5] 。基于这个问题，研究者提出了许多种方法，旨在寻找验证安全性的充分条件，这 些方法大致可分为两类，一类是从语义上求解可达集的近似，如用简单的几何体外近似可达 集[1][7] [2] ；另一类是模型转化 ，是从语法上构造原系统的模拟自动机， 要求所构造的模拟器 其可达集是可判定的，或者是可计算的。本文所叙述的方法归属于这一类。 Thomos.A.Henzinger 提出了phase-portrait 近似概念，文献[2] 构造线性 phase-portrait 自动 [6] 机来模拟非线性自动机， 文献 使用泰勒公式构造多项式自动机，但这种近似不是 phase-portrait 近似，因此仅依赖增大多项式的幂级数来提高近似的精确有一定的局限性，基 于这点考虑，本文将线性 phase-portrait 近似 推广到多项式phase-portrait 近似，并给出了多 项式phase-portrait 近似自动机的构造方法。 2. 混合自动机 混合自动机是研究混合系统的常用模型，混合自动机的语法及语义定义如下所述。 2.1 多项式及一阶谓词公式 L {=+−, , ,0,1} 0 语言是符号的集合，包括关系，函数，和常数，如 ，其中 是关系，+ 、 F (θ, θ ) 1 m F - 是函数，0，1是常数。语言的项递归定义为:项是变量、常数，或者 其中 是 θ,i 1,,m L {=+−, , ,0,1} L {=+−, , ,i,0,1} m元的函数，i 是项。语言 0 的项为线性项，语言 R θ θ R (θ, ,θ ) θ,i 1, , m 1 2 1 n i