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.