定时器连续系统分析：阈值切换面划分的离散近似法

"具有定时器连续系统的阈值切换面划分离散近似 (2001年)" 这篇2001年的论文"有定时器连续系统的阈值切换面划分离散近似"着重研究了混合系统中包含定时器的连续部分的验证问题。混合系统是由离散事件和连续动态组成的复杂系统，它们在现代工业自动化、机器人控制和嵌入式系统等领域中广泛应用。在这些系统中，定时器用于控制和协调不同组件的操作。 传统上，基于阈值切换面划分的验证方法对于没有定时器的连续部分非常有效，但当连续部分存在定时器时，这种方法不再适用。论文首次提出了一种创新的解决策略，它综合了流管道近似（Segmenting Approximation of Flow Pipe, SAFP）和阈值切换面划分（Partition of Threshold Switching Surfaces, PTSS）两种方法。这种结合考虑了定时器的影响，引入了过渡状态（interim states）的概念。 在流管道近似中，系统的行为被分割成一系列连续的子区间（或“管道”），每个子区间代表系统状态的特定变化。过渡状态集合则表示系统在不同阶段之间的中间状态。论文提出，在近似过渡状态集合时，通过对时间域的扩展，可以自动确定定时器的合理设定范围。这种方法允许更精确地分析含有定时器的连续部分，从而扩大了分析的适用性。 通过一个化学过程控制的实例，论文展示了上述方法的可行性和优势。形式验证（formal verification）方法，即使用数学和逻辑工具来证明系统行为的正确性，相比于传统的仿真方法，能够提供更严格、更全面的分析。仿真方法虽然直观，但在处理复杂的定时逻辑时可能会遇到困难，而形式验证则可以提供一种确定性的保证。 这篇论文为混合系统中包含定时器的连续部分的分析提供了新的理论基础，促进了混合系统验证技术的发展，对于确保系统的可靠性和安全性具有重要意义。通过将流管道近似与阈值切换面划分相结合，研究人员能够更好地理解和控制那些依赖于定时器的复杂系统行为。