A Synergistic Multi-Layered Approach for Falsification of Specifications for Hybrid Systems

Hybrid systems, which combine discrete and continuous dynamics, provide sophisticated mathematical models for automated highway systems, air traffic control, biological systems, and other applications. A key feature of such systems is that they are often deployed in safety-critical scenarios and hence designing such systems with provable guarantees is very important. This is usually done through analysis of such systems with regard to a given set of safety properties that assert that nothing ‘bad’ happens during the operation of the system. As more complex hybrid systems are considered, limiting safety properties to a set of unsafe states, as in current methods, considerably restricts the ability of designers to adequately express the desired safe behavior of the system. To allow for more sophisticated properties, researchers have advocated the use of linear temporal logic (LTL), which makes it possible to express temporal safety properties. This project develops algorithmic tools for safety analysis of embedded and hybrid systems operating under the effect of exogenous inputs and for LTL specifications. The problem addressed is the following: Given a hybrid system and a safety specification described using LTL, can a feasible trajectory be constructed for the system that violates the specification, when such a trajectory exists? The problem is called the falsification problem. The broader impact of the project is implemented through course development, involvement in research activities of undergraduate, graduate and postdoctoral students, efforts to mentor underrepresented groups, and dissemination of concepts through educational software developed at Rice.