Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
No edit summary |
||
| Line 2: | Line 2: | ||
|Title=Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis | |Title=Decomposing GR(1) Games with Singleton Liveness Guarantees for Efficient Synthesis | ||
|Authors=Sumanth Dathathri and Richard M. Murray | |Authors=Sumanth Dathathri and Richard M. Murray | ||
|Source= | |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. | |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. | ||
|URL=http://www.cds.caltech.edu/~murray/preprints/dm17- | |URL=http://www.cds.caltech.edu/~murray/preprints/dm17-cdc.pdf | ||
|Type=Conference paper | |Type=Conference paper | ||
|ID=2017b | |ID=2017b | ||
Latest revision as of 03:10, 25 September 2017
| 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 |
| DOI | |
| Tag | dm17-cdc |
| ID | 2017b |
| Funding | SRC TerraSwarm |
| Flags |
