LTL Realizability via Safety and Reachability Games. Camacho, A., Muise, C., Baier, J. A., & McIlraith, S. A. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI), 2018.
LTL Realizability via Safety and Reachability Games [pdf]Paper  LTL Realizability via Safety and Reachability Games [pdf]Poster  abstract   bibtex   
LTL synthesis is the problem of computing a strategy that satisfies a given property expressed in Linear Temporal Logic (LTL). Synthesis provides a means of constructing programs that allow an agent to interact with their environment following a declarative specification of behavior. Modern approaches to LTL synthesis exploit bounded synthesis techniques, reducing the synthesis problem to a series of safety games between the agent and the environment. The same techniques can be used to determine unrealizability of LTL specifications by solving dual games where the order of turn taking is inverted. In the first part of the paper, we investigate the role of this duality in LTL realizability and synthesis. We describe different reductions to automata games that exploit duality to determine realizability, and introduce novel techniques that reduce realizability to a series of reachability games. In the second part of the paper, we introduce algorithms to solve these safety and reachability games via Fully Observable Non-Deterministic (FOND) planning. Our experimental evaluation illustrates that, by reducing the problem to a reachability game we can solve some problems that state-of-the-art synthesis tools cannot solve. Moreover, it shows that planning can be a competitive approach to LTL synthesis and realizability.

Downloads: 0