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

From MurrayWiki
Jump to: navigation, search
Title Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis
Authors Sumanth Dathathri and Richard M. Murray
Source 2017 Conference on Decision and Control (CDC)
Abstract Temporal logic based synthesis approaches are often used to find trajectories that are correct-by-construction in systems–eg. 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.
Type Conference paper
URL http://www.cds.caltech.edu/~murray/preprints/dm17-cdc.pdf
Tag dm17-cdc
ID 2017b
Funding SRC TerraSwarm
Flags