Difference between revisions of "Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States"

From MurrayWiki
Jump to: navigation, search
(Created page with "{{Paper |Title=Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States |Authors=Sumanth Dathathri, Ioannis Filippidis and Richard M....")
 
 
(One intermediate revision by the same user not shown)
Line 2: Line 2:
 
|Title=Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States
 
|Title=Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States
 
|Authors=Sumanth Dathathri, Ioannis Filippidis and Richard M. Murray
 
|Authors=Sumanth Dathathri, Ioannis Filippidis and Richard M. Murray
|Source=Submitted, 2017 Internationl Symposium on Robotics Research (ISRR)
+
|Source=Submitted, 2017 International Symposium on Robotics Research (ISRR)
 
|Abstract=For the synthesis of correct-by-construction control policies from temporal logic specifications the scalability of the synthesis algorithms is often a bottleneck. In this paper, we parallelize synthesis from specifications in the GR(1) fragment of linear temporal logic by introducing a hierarchical procedure that allows decoupling of the fixpoint computations. The state space is partitioned into equicontrollable sets using solutions to parameterized reachability games that arise from decomposing the original GR(1) game into smaller reachability games. Following the partitioning, another synthesis problem is formulated for composing the strategies from the decomposed reachability games. The formulation guarantees that composing the synthesized controllers ensures satisfaction of the given GR(1) property. Benchmarking experiments with robot planning problems demonstrate good scalability of the approach.
 
|Abstract=For the synthesis of correct-by-construction control policies from temporal logic specifications the scalability of the synthesis algorithms is often a bottleneck. In this paper, we parallelize synthesis from specifications in the GR(1) fragment of linear temporal logic by introducing a hierarchical procedure that allows decoupling of the fixpoint computations. The state space is partitioned into equicontrollable sets using solutions to parameterized reachability games that arise from decomposing the original GR(1) game into smaller reachability games. Following the partitioning, another synthesis problem is formulated for composing the strategies from the decomposed reachability games. The formulation guarantees that composing the synthesized controllers ensures satisfaction of the given GR(1) property. Benchmarking experiments with robot planning problems demonstrate good scalability of the approach.
 
|URL=http://www.cds.caltech.edu/~murray/preprints/dfm17-isrr_s.pdf
 
|URL=http://www.cds.caltech.edu/~murray/preprints/dfm17-isrr_s.pdf
 
|Type=Conference paper
 
|Type=Conference paper
|ID=2017c
+
|ID=2017d
 
|Tag=dfm17-isrr
 
|Tag=dfm17-isrr
 
|Funding=SRC TerraSwarm
 
|Funding=SRC TerraSwarm
 
}}
 
}}

Latest revision as of 17:04, 23 July 2017

Title Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States
Authors Sumanth Dathathri, Ioannis Filippidis and Richard M. Murray
Source Submitted, 2017 International Symposium on Robotics Research (ISRR)
Abstract For the synthesis of correct-by-construction control policies from temporal logic specifications the scalability of the synthesis algorithms is often a bottleneck. In this paper, we parallelize synthesis from specifications in the GR(1) fragment of linear temporal logic by introducing a hierarchical procedure that allows decoupling of the fixpoint computations. The state space is partitioned into equicontrollable sets using solutions to parameterized reachability games that arise from decomposing the original GR(1) game into smaller reachability games. Following the partitioning, another synthesis problem is formulated for composing the strategies from the decomposed reachability games. The formulation guarantees that composing the synthesized controllers ensures satisfaction of the given GR(1) property. Benchmarking experiments with robot planning problems demonstrate good scalability of the approach.
Type Conference paper
URL http://www.cds.caltech.edu/~murray/preprints/dfm17-isrr_s.pdf
Tag dfm17-isrr
ID 2017d
Funding SRC TerraSwarm
Flags