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, Jun. 2016.
    Details
  2. K. He, M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “Towards Manipulation Planning with Temporal Logic Specifications,” in 2015 IEEE International Conference on Robotics and Automation (ICRA), Seattle, WA, USA, 2015, pp. 346–352.
    Details
  3. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Asymptotically Optimal Stochastic Motion Planning with Temporal Goals,” in Springer Tracts in Advanced Robotics, Istanbul, Turkey, 2015, pp. 335–352.
    Details
  4. 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
  5. 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
  6. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Fast Stochastic Motion Planning with Optimality Guarantees using Local Policy Reconfiguration,” in 2014 IEEE International Conference on Robotics and Automation (ICRA), Hong Kong, China, 2014, pp. 3013–3019.
    Details
  7. M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “A Sampling-Based Strategy Planner for Nondeterministic Hybrid Systems,” in 2014 IEEE International Conference on Robotics and Automation (ICRA), 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. D. K. Grady, M. Moll, and L. E. Kavraki, “Automated Model Approximation for Robotic Navigation with POMDPs,” in 2013 IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 78–84.
    Details
  10. B. Gipson, M. Moll, and L. E. Kavraki, “Resolution Independent Density Estimation for Motion Planning in High-Dimensional Spaces,” in 2013 IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 2429–2435.
    Details
  11. 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 Proceedings of the 16th international conference on Hybrid systems: computation and control - HSCC ’13, Philadelphia, Pennsylvania, USA, 2013, pp. 353–362.
    Details
  12. 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 2012 IEEE International Symposium on Safety, Security, and Rescue Robotics (SSRR), College Station, TX, USA, 2012, pp. 1–6.
    Details
  13. 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 2012 IEEE International Symposium on Safety, Security, and Rescue Robotics (SSRR), College Station, TX, USA, 2012, pp. 1–6.
    Details
  14. M. R. Maly and L. E. Kavraki, “Low-Dimensional Projections for SyCLoP,” in 2012 IEEE/RSJ International Conference on Intelligent Robots and Systems, Vilamoura-Algarve, Portugal, 2012, pp. 420–425.
    Details
  15. 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, vol. 15, no. 4, pp. 305–320, May 2012.
    Details
  16. I. A. Sucan and L. E. Kavraki, “Accounting for Uncertainty in Simultaneous Task and Motion Planning Using Task Motion Multigraphs,” in 2012 IEEE International Conference on Robotics and Automation, Saint Paul, MN, 2012, pp. 4822–4828.
    Details
  17. K. E. Bekris, D. K. Grady, M. Moll, and L. E. Kavraki, “Safe Distributed Motion Coordination for Second-Order Systems With Different Planning Cycles,” The International Journal of Robotics Research, vol. 31, no. 2, pp. 129–150, Feb. 2012.
    Details
  18. A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi, “Motion Planning with Complex Goals,” IEEE Robotics and Automation Magazine, vol. 18, no. 3, pp. 55–64, Sep. 2011.
    Details
  19. I. A. Sucan and L. E. Kavraki, “Mobile Manipulation: Encoding Motion Planning Options Using Task Motion Multigraphs,” in 2011 IEEE International Conference on Robotics and Automation, Shanghai, China, 2011, pp. 5492–5498.
    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