A Caltech Library Service

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

Dathathri, Sumanth and Murray, Richard M. (2017) Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis. , Pasadena, CA. (Unpublished)

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


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.

Item Type:Report or Paper (Technical Report)
Murray, Richard M.0000-0002-5785-7481
Additional Information:Extended version of paper to appear at Conference on Decision and Control 2017.
Group:Control and Dynamical Systems Technical Reports
Record Number:CaltechAUTHORS:20170920-152025463
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:81642
Deposited By: Sumanth Dathathri
Deposited On:20 Sep 2017 22:28
Last Modified:03 Oct 2019 18:45

Repository Staff Only: item control page