Hybrid Systems (Discrete Logic + Continuous Dynamics)
Automatic Discovery of Safety Violations
Hybrid systems play an increasingly important role in transportation networks as part of embedded controllers used in the automotive industry and air-traffic management, or in manufacturing processes, robotics, and even medicine as part of medical devices monitoring health conditions. A hybrid system is a formal model that combines discrete logic and continuous dynamics. Continuous dynamics are associated with each mode, and discrete logic determines how to switch between modes. A hybrid system may model air traffic control, where the modes correspond to the cruising of the planes and the discrete logic models conflict-resolution protocols. As another example, a hybrid system may model a vehicle whose underlying dynamics varies discretely depending on terrain conditions.
Verification of Safety Properties: As hybrid systems are often part of devices operating in safety-critical situations, the verification of safety properties becomes increasingly important. Safety properties assert that nothing "bad" happens, e.g., air-traffic control guarantees that planes do not come too close to one another. Verification approaches generally rely on approximations of reachable states or the use of abstractions to obtain finite-state models that capture the safety properties of the hybrid system. Due to the computational complexity of the problem, verification approaches have an exponential dependency on the dimension of the state space and are limited in practicality to low-dimensional systems.
From Verification to Falsification: To handle more complex hybrid systems, alternative approaches have been proposed that shift from verification to falsification, which is often the focus of model checking in industrial applications. Even though falsification methods cannot determine that a hybrid system is safe, they can compute witness trajectories when the hybrid system is unsafe. Witness trajectories, similar to error traces in model checking, indicate flaws, which can then be corrected.
Combining Motion Planning and Model Checking for the Falsification of Safety Properties: This work approaches hybrid-system falsification from a robotics perspective. Initially, it exploits the insight that hybrid-system falsification is in many respects related to motion planning, which is a search problem for a witness trajectory that satisfies certain invariants, such as ensuring that the robot motion respects the underlying dynamics and avoids collision with obstacles. While in motion planning the search takes place in a continuous space, in hybrid-system falsification the search for a witness trajectory takes place in a space consisting of discrete and continuous components.
Model checking guides motion planning by providing discrete witnesses along which to extend a search tree T. A discrete witness is a sequence of propositional assignments that violates the safety property. Motion planning extends the search tree T by adding new trajectories using the discrete witness as a guide so that more and more of the propositional assignments associated with the discrete witness are satisfied. As motion planning extends the search tree, it also gathers information to estimate the progress made in the search for a witness trajectory. This information is fed back to model checking to select in future iterations alternative discrete witnesses that could expand the search along new directions. This interplay between model checking and motion planning is a crucial component that allows the approach to effectively search for a witness trajectory.
- Plaku E, Kavraki LE, and Vardi MY (2013): “Falsification of LTL Safety Properties in Hybrid Systems with Nonlinear Dynamics.” Springer International Journal on Software Tools for Technology Transfer, vol. 15, pp. 305–320 [publisher] [preprint]
- Plaku E, Kavraki LE, and Vardi MY (2009): "Hybrid Systems: From Verification to Falsification by Combining Motion Planning and Discrete Search." Formal Methods in System Design, 2009, vol. 34(2), pp. 157--182 [publisher] [preprint]
- Plaku E, Kavraki LE, and Vardi MY (2009): "Falsification of LTL Safety Properties in Hybrid Systems." Springer LNCS Tools and Algorithms for the Construction and Analysis of Systems, vol. 5505, pp. 368--382 [publisher] [preprint]
- Plaku E, Kavraki LE, and Vardi MY (2007): "Hybrid Systems: From Verification to Falsification." Springer LNCS Computer Aided Verification, vol. 4590, pp. 468--481 [publisher] [preprint]