LTL Realizability via Safety and Reachability Games

LTL Realizability via Safety and Reachability Games

Alberto Camacho, Christian Muise, Jorge A. Baier, Sheila A. McIlraith

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 4683-4691. https://doi.org/10.24963/ijcai.2018/651

In this paper, we address the problem of LTL realizability and synthesis. State of the art techniques rely on so-called bounded synthesis methods, which reduce the problem to a safety game. Realizability is determined by solving synthesis in a dual game. We provide a unified view of duality, and introduce novel bounded realizability methods via reductions to reachability games. Further, we introduce algorithms, based on AI automated planning, to solve these safety and reachability games. This is the the first complete approach to LTL realizability and synthesis via automated planning. Experiments illustrate that reductions to reachability games are an alternative to reductions to safety games, and show that planning can be a competitive approach to LTL realizability and synthesis.
Keywords:
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Planning and Scheduling: Applications of Planning
Planning and Scheduling: Planning under Uncertainty
Planning and Scheduling: Planning and Scheduling