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 parametrized games that arise from decomposing the original GR(1) game into smaller reachability-persistence 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. Experiments with robot planning problems demonstrate good performance of the approach.
CITATION STYLE
Dathathri, S., Filippidis, I., & Murray, R. M. (2020). Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States. In Springer Proceedings in Advanced Robotics (Vol. 10, pp. 827–842). Springer Science and Business Media B.V. https://doi.org/10.1007/978-3-030-28619-4_57
Mendeley helps you to discover research relevant for your work.