Algorithmic Verification and Synthesis of Hybrid Control Systems

监视混合系统是产生连续值和离散值信号混合的系统。当计算机监督或控制复杂的动态装置时，这种系统就出现了。近年来，人们对使用算法方法来验证和综合混合控制系统非常感兴趣。算法方法使用算法，这些算法的成功执行为系统满足期望行为的能力提供了必要和充分的条件。混合自动机的符号模型检验是一种众所周知的混合系统验证算法。不幸的是，对于许多类型的混合系统来说，混合系统模型校验是不可确定的，这一消极结果极大地限制了算法方法在分析和综合混合控制系统方面的实际潜力。该项目提出了一种范式转换，其中我们使用算法方法来验证满足期望行为的“受控”混合系统的存在。这种验证方法对于一大类实际系统是可确定的，因此提供了一个突破，使算法方法的发展成为可能，为混合控制系统的验证和综合提供了实用的手段。

A supervisory hybrid system is a system generating a mixture of discrete-valued and continuous-valued signals. Such systems arise when computers supervise or control complex dynamical plants. In recent years, there has been significant interest in the use of algorithmic methods for the verification and synthesis of hybrid control systems. Algorithmic methods use algorithms whose successful execution provide necessary and sufficient conditions on the system's ability to satisfy a desired behavior. Symbolic model checking for hybrid automata represent a well-known algorithmic approach to hybrid system verification. Hybrid system model checking, unfortunately, has been shown to be undecidable for many classes of hybrid systems and this negative result has greatly limited the practical potential of algorithmic methods in analyzing and synthesizing hybrid control systems. This project proposes a paradigm shift in which we use algorithmic methods to verify the existence of 'controlled' hybrid systems satisfying desired behaviors. This approach to verification is decidable for a large class of practical systems and therefore provides a breakthrough making possible the development of algorithmic methods that provide a practical means for the verification and synthesis of hybrid control systems.