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 proposal 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.
Hybrid systems, which combine discrete and continuous dynamics, provide sophisticated mathematical models for automated highway systems, air traffic control, biological systems, power networks, 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 on their behavior 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, which makes it possible to express temporal safety properties. This grant developed a multi-layered approach that synergistically combines discrete search techniques for digital systems with state-of-the-art search algorithms for continuous systems for the falsification of safety problems of hybrid systems. Our proposed approach comprises of three layers: the high-level search layer, the intermediate synergy layer and the low-level search layer. The high-level layer handles most of the discrete nature of the problem by using a suitably constructed abstraction of the system model together with the specifications. The high-level layer suggests promising high-level guides for further exploration to the low-level layer. The low-level layer explores the state-space of the system guided by the high-level guide and using sampling-based algorithms that are inspired by motion planning algorithms from robotics. A synergistic interaction between the two layers is facilitated by the synergy layer which is responsible for aggregating the information provided by the low-level search layer to information that can be used by the high-level search layer. The construction of discrete abstractions that encode the robot and the specifications and safety properties, the use of synergy between the high-level and low-level layers, issues related to the appropriate choice of search methods for the different layers, scalability, and semantics are critical to the performance of the proposed scheme were developed. The synergistic framework was applied to falsifying properties of cars modeled as hybrid systems. The framework can also be used to find motions of the cars that satisfy a complex specification. The capabilities of the framework as well as its limitations, scalability, and efficiency were demonstrated. The grant also contributed to the education of graduate and postdoctoral students. All students were co-advised by the PIs and were immersed in the activities of the two groups. This resulted in the involvement of a much larger set of students (actually all the students in the groups of the PIs) with the project. One of the PIs included material developed in this project in an undergraduate class taught yearly at Rice and attended each year by more than 30 students. The results have been disseminated through open source code, lectures and colloquia, material developed and used in an undergraduate class, and publications and presentations at conferences and workshops.
