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

TL;DR

This paper introduces a decomposition method for a specific class of GR(1) LTL synthesis problems, enabling parallelization and efficiency improvements, demonstrated through multi-agent robot coordination examples.

Contribution

It identifies a class of GR(1) synthesis problems that can be decomposed for parallel processing, reducing complexity and improving scalability.

Findings

Decomposition enables parallel synthesis of GR(1) games.

Reduced alternation depth leads to more efficient synthesis.

Empirical analysis shows improved performance in multi-agent scenarios.

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.