混合系统是嵌入在模拟环境中的数字实时系统。混合系统的一个典型例子是用于模拟工厂环境（如熔炉或飞机）的数字嵌入式控制程序：控制器状态在控制模式之间离散移动，在每种控制模式下，工厂状态根据物理定律连续演变。这些系统结合了离散和连续动态。这些方面已在计算机科学和控制理论中得到研究。计算机科学家引入了混合自动机 [Hen00]，这是一种将离散控制图（通常称为有限状态自动机）与连续演变变量相结合的形式化模型。混合自动机表现出两种状态变化：离散跳跃转换瞬间发生，连续流转换随时间流逝而发生。混合系统通常是安全关键系统。因此，它们的可靠性是一个核心问题。例如，监测核反应堆温度的数字控制器的正确性至关重要。我们将混合自动机作为定义混合系统轨迹（行为）的形式模型。混合系统的属性为其轨迹分配值：例如，它们可以将轨迹分类为好或坏。混合自动机的行为通常很复杂，因此很难对其进行推理。这就是为什么自早期关于混合自动机的研究以来，重点一直是