NSF SHF 1018798:
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.

Related Publications

  1. M. Lahijanian, M. R. Maly, D. Fried, L. E. Kavraki, H. Kress-Gazit, and M. 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 2015 IEEE Intl. Conf. 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 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 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 IEEE International Conference on Robotics and Automation, Hong Kong, China, 2014, pp. 3013–3019.
    Details
  6. D. K. Grady, “Motion Planning with Uncertain Information in Robotic Tasks,” PhD thesis, Rice University, Department of Computer Science, Houston, Texas, 2014.
    pdf publisher details
    Details
  7. R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki, “Asymptotically Optimal Stochastic Motion Planning with Temporal Goals,” in Workshop on the Algorithmic Foundations of Robotics, Istanbul, Turkey, 2014.
    Details
  8. M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “A Sampling-Based Strategy Planner for Nondeterministic Hybrid Systems,” in International Conference on Robotics and Automation, Hong Kong, China, 2014, pp. 3005–3012.
    Details
  9. D. K. Grady, M. Moll, and L. E. Kavraki, “Combining a POMDP Abstraction with Replanning to Solve Complex, Position-Dependent Sensing Tasks,” in AAAI Fall Symposium, Arlington, Virginia, 2013.
    Details
  10. R. Luna, I. A. Şucan, M. Moll, and L. E. Kavraki, “Anytime Solution Optimization for Sampling-Based Motion Planning,” in IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 5053–5059.
    Details
  11. D. K. Grady, M. Moll, and L. E. Kavraki, “Automated Model Approximation for Robotic Navigation with POMDPs,” in IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, 2013, pp. 78–84.
    Details
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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