混合系统验证：多项式phase-portrait近似方法

"这篇论文探讨了混合自动机的多项式phase-portrait近似技术，由刘保罗、裴海龙和他们的同事共同撰写。混合自动机是验证混合系统安全性的重要工具，而模型转换则是构建可判定或半判定的混合自动机以近似原始混合自动机的过程。论文扩展了线性phase-portrait近似，介绍了如何自动生成多项式phase-portrait近似自动机以及如何优化近似模型。研究背景是混合系统，它们是结合了连续变量和离散事件的动态系统，如数字嵌入式系统。安全性验证是关键，但可达集的精确计算在大多数情况下是不可判定的。因此，研究人员采用抽象近似和模型转换策略，如几何体外近似和模拟自动机。论文中提到的方法属于后者，基于Thomas A. Henzinger的phase-portrait近似思想，提出了一种新的多项式phase-portrait近似方法，以提高对非线性自动机的模拟精度。" 这篇学术论文主要关注的是混合自动机的验证技术，特别是在混合系统安全性分析中的应用。混合自动机是一种模型，用于表示同时包含连续和离散行为的复杂系统，例如嵌入式系统。由于这些系统的复杂性，精确计算其可达集通常是不可行的，这直接影响到安全性的验证。为了解决这个问题，研究者采用了抽象近似的方法，即通过构建一个简化版的模型来近似原模型的行为。 文章特别强调了phase-portrait近似，这是一种模拟非线性行为的技术。传统的线性phase-portrait近似在某些情况下可能不够准确，因此论文提出了将其扩展到多项式phase-portrait近似。这种方法允许更精确地模拟非线性混合自动机，通过构造多项式phase-portrait近似自动机，可以更好地估计系统的可达状态集，从而提高验证的准确性。论文详细描述了如何自动构造这样的近似模型以及如何逐步细化以提升近似质量。 这篇论文贡献了一种新的工具和技术，用于处理混合系统验证中的挑战，特别是针对那些难以精确计算可达集的复杂系统。通过多项式phase-portrait近似，研究者提供了一条更有效和精确的路径，以评估混合系统的安全性。这项工作对于混合系统的设计和分析具有重要的理论和实践价值。