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

  • Authors:
    Sumanth Dathathri (Caltech), Richard Murray (Caltech)
    Publication ID:
    P090651
    Publication Type:
    Paper
    Received Date:
    4-Apr-2017
    Last Edit Date:
    5-Apr-2017
    Research:
    2386.004 (University of California/Berkeley)

Abstract

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

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.