混合系统模型检测：基于混合时序逻辑的研究

"这篇论文是关于混合系统的模型检测技术，主要关注如何在混合时序逻辑框架下进行这一过程。作者张海宾通过将问题转化为区间时序逻辑的问题，解决了时间自动机的模型检测，进一步处理了多速率混合系统的模型检测，并提出了针对矩形混合系统基于线性命题逻辑的模型检测算法。这项研究得到了国家自然科学基金和高等学校博士学科点专项基金的支持。" 混合系统是结合离散和连续行为的复杂动态系统，它们在自动化、控制理论和计算机科学等领域有着广泛的应用。模型检测是验证这些系统是否满足特定规范的重要工具，可以用于找出设计中的错误或证明其正确性。 时序逻辑是一种形式逻辑，专门用于描述和验证系统的动态行为。混合时序逻辑在此文中被用作描述混合系统的动态特性和验证条件，它扩展了传统的时序逻辑，能够处理连续时间的演进和离散事件的交互。 文章的核心贡献在于将混合时序逻辑下的模型检测问题转换为区间时序逻辑问题。区间时序逻辑使用时间区间来表示时间的流逝，这对于处理连续时间的行为特别有用。通过这种转换，作者解决了时间自动机的模型检测，这是模型检测中的一个关键步骤，因为时间自动机是描述混合系统行为的有效模型。 接下来，论文解决了多速率混合系统的模型检测问题。在这些系统中，不同的组件可能以不同的速度运行，这增加了验证的复杂性。通过转换为时间自动机的模型检测问题，作者能够处理这种异步行为。 最后，张海宾提出了一种针对矩形混合系统（具有矩形区域状态空间的混合系统）的模型检测算法，该算法专注于基于线性命题逻辑的属性检查。线性命题逻辑是一种简化版的时序逻辑，仅包含基本的逻辑运算和命题变量，使得模型检测更加高效和可管理。 这篇论文深入探讨了混合系统的模型检测技术，提供了解决方案和新的算法，对于混合系统的形式验证领域有重要的理论和实践价值。它不仅推动了理论研究的进步，也为实际系统的设计和验证提供了工具支持。