# Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis

arXiv: https://arxiv.org/abs/1709.07094 · HTML: https://mlsanity.com/paper/1709.07094/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Sep 2017.

## Built on by (most cited first, 1 of 1)

- [Monitoring of Perception Systems: Deterministic, Probabilistic, and Learning-based Fault Detection and Identification](https://mlsanity.com/paper/2205.10906/) (2022)

## Abstract (arXiv)

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.