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.

This work has been supported by grant NSF SHF 1018798.

Related Publications

  1. M. Lahijanian, M. R. Maly, D. Fried, L. E. Kavraki, H. Kress-Gazit, and M. Y. Vardi, “Iterative Temporal Planning in Uncertain Environments with Partial Satisfaction Guarantees,” IEEE Transactions on Robotics, vol. 32, no. 3, pp. 583–599, 2016.
    Details
  2. K. He, M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “Towards Manipulation Planning with Temporal Logic Specifications,” in Proceedings of the 2015 IEEE International Conference on Robotics and Automation (ICRA), Seattle, WA, 2015, pp. 346–352.
    Details
  3. M. Lahijanian, S. Almagor, D. Fried, L. E. Kavraki, and M. Y. Vardi, “This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction,” in Proceedings of The Twenty-Ninth AAAI Conference (AAAI-15), Austin, TX, 2015, pp. 3664–3671.
    Details
  4. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Optimal and Efficient Stochastic Motion Planning in Partially-Known Environments,” in Proceedings of The Twenty-Eighth AAAI Conference on Artificial Intelligence, Quebec City, Canada, 2014, pp. 2549–2555.
    Details
  5. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Fast Stochastic Motion Planning with Optimality Guarantees using Local Policy Reconfiguration,” in Proceedings of the IEEE International Conference on Robotics and Automation, Hong Kong, China, 2014, pp. 3013–3019.
    Details
  6. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Asymptotically Optimal Stochastic Motion Planning with Temporal Goals,” in Proceedings of the Workshop on the Algorithmic Foundations of Robotics, Istanbul, Turkey, 2014.
    Details
  7. M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “A Sampling-Based Strategy Planner for Nondeterministic Hybrid Systems,” in Proceedings of the International Conference on Robotics and Automation, Hong Kong, China, 2014, pp. 3005–3012.
    Details
  8. D. K. Grady, M. Moll, and L. E. Kavraki, “Combining a POMDP Abstraction with Replanning to Solve Complex, Position-Dependent Sensing Tasks,” in Proceedings of the AAAI Fall Symposium, Arlington, Virginia, 2013.
    Details
  9. R. Luna, I. A. Şucan, M. Moll, and L. E. Kavraki, “Anytime Solution Optimization for Sampling-Based Motion Planning,” in Proceedings of the IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 5053–5059.
    Details
  10. D. K. Grady, M. Moll, and L. E. Kavraki, “Automated Model Approximation for Robotic Navigation with POMDPs,” in Proceedings of the IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 78–84.
    Details
  11. E. Plaku, L. E. Kavraki, and M. Y. Vardi, “Falsification of LTL safety properties in hybrid systems,” International Journal on Software Tools for Technology Transfer (STTT), vol. 15, no. 4, pp. 305–320, 2013.
    Details
  12. M. R. Maly, M. Lahijanian, L. E. Kavraki, H. Kress-Gazit, and M. Y. Vardi, “Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments,” in ACM International Conference on Hybrid Systems: Computation and Control (HSCC), Philadelphia, PA, USA, 2013, pp. 353–362.
    Details
  13. B. Gipson, M. Moll, and L. E. Kavraki, “Resolution Independent Density Estimation for Motion Planning in High-Dimensional Spaces,” in IEEE International Conference on Robotics and Automation, 2013, pp. 2429–2435.
    Details
  14. M. R. Maly and L. E. Kavraki, “Low-Dimensional Projections for SyCLoP,” in IEEE/RSJ International Conference on Intelligent Robots and Systems, Vilamoura, Algarve, Portugal, 2012, pp. 420–425.
    Details
  15. I. A. Sucan and L. E. Kavraki, “Accounting for Uncertainty in Simultaneous Task and Motion Planning Using Task Motion Multigraphs,” in IEEE International Conference on Robotics and Automation, St. Paul, 2012, pp. 4822–4828.
    Details
  16. D. K. Grady, M. Moll, C. Hegde, A. C. Sankaranarayanan, R. G. Baraniuk, and L. E. Kavraki, “Multi-Objective Sensor-Based Replanning for a Car-Like Robot,” in IEEE International Symposium on Safety, Security, and Rescue Robotics, College Station, TX, 2012, pp. 1–6.
    Details
  17. D. K. Grady, M. Moll, C. Hegde, A. C. Sankaranarayanan, R. G. Baraniuk, and L. E. Kavraki, “Multi-Robot Target Verification with Reachability Constraints,” in IEEE International Symposium on Safety, Security, and Rescue Robotics, College Station, TX, 2012, pp. 1–6.
    Details
  18. K. E. Bekris, D. K. Grady, M. Moll, and L. E. Kavraki, “Safe Distributed Motion Coordination for Second-Order Systems With Different Planning Cycles,” International Journal of Robotics Research, vol. 31, no. 2, pp. 129–150, 2012.
    Details
  19. A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi, “Motion Planning with Complex Goals,” Robotics Automation Magazine, IEEE, vol. 18, no. 3, pp. 55–64, Sep. 2011.
    Details
  20. I. A. Sucan and L. E. Kavraki, “On the Advantages of Using Task Motion Multigraphs for Efficient Mobile Manipulation,” in IEEE/RSJ International Conference on Intelligent Robots and Systems, San Francisco, CA, 2011, pp. 4621–4626.
    Details
  21. I. A. Sucan and L. E. Kavraki, “Mobile Manipulation: Encoding Motion Planning Options Using Task Motion Multigraphs,” in IEEE International Conference on Robotics and Automation, Shanghai, China, 2011, pp. 5492–5498.
    Details