Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis
Abstract
Temporal logic based synthesis approaches are often used to find trajectories that are correct-by-construction for tasks in systems with complex behavior. Some examples of such tasks include synchronization for multi-agent hybrid systems, reactive motion planning for robots. However, the scalability of such approaches is of concern and at times a bottleneck when transitioning from theory to practice. In this paper, we identify a class of problems in the GR(1) fragment of linear-time temporal logic (LTL) where the synthesis problem allows for a decomposition that enables easy parallelization. This decomposition also reduces the alternation depth, resulting in more efficient synthesis. A multi-agent robot gridworld example with coordination tasks is presented to demonstrate the application of the developed ideas and also to perform empirical analysis for benchmarking the decomposition-based synthesis approach.
Keywords
Cite
@article{arxiv.1709.07094,
title = {Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis},
author = {Sumanth Dathathri and Richard M. Murray},
journal= {arXiv preprint arXiv:1709.07094},
year = {2017}
}