Algorithmic Verification and Synthesis of Hybrid Control Systems

混合控制系统的算法验证与综合

• 批准号: 9986918
• 负责人: Michael Lemmon
• 金额: $ 15万
• 依托单位: University of Notre Dame
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2000
• 资助国家: 美国
• 起止时间: 2000-09-01 至 2003-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9986918&HistoricalAwards=false
• 关键词: Algorithmic; Verification; Synthesis; Hybrid; Control

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.

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