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

  • Authors:
    Sumanth Dathathri (Caltech), Richard Murray (Caltech)
    Publication ID:
    Publication Type:
    Received Date:
    Last Edit Date:
    2386.004 (University of California/Berkeley)


Temporal logic based synthesis approaches are often used to find trajectories that are correct-by-construction in systems - e.g. 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 grid world 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.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450