CaltechAUTHORS
  A Caltech Library Service

Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States

Dathathri, Sumanth and Filippidis, Ioannis and Murray, Richard M. (2019) Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States. In: Robotics Research: The 18th International Symposium ISRR. Springer Proceedings in Advanced Robotics. No.10. Springer , Cham, pp. 827-842. ISBN 978-3-030-28618-7. https://resolver.caltech.edu/CaltechAUTHORS:20171102-092833279

[img] PDF - Accepted Version
See Usage Policy.

215Kb

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20171102-092833279

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 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.


Item Type:Book Section
Related URLs:
URLURL TypeDescription
https://doi.org/10.1007/978-3-030-28619-4_57DOIArticle
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email Address:sdathath@caltech.edu
Additional Information:© 2020 Springer Nature Switzerland AG. First Online: 28 November 2019. This work is sponsored in part by TerraSwarm, a funded center of STARnet, a Semiconductor Research Corporation (SRC) program sponsored by MARCO and DARPA.
Funders:
Funding AgencyGrant Number
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
STARnetUNSPECIFIED
Subject Keywords:Synthesis; Temporal logic; Generalized reactivity; Binary-Decision diagrams; Formal methods; Discrete event systems
Series Name:Springer Proceedings in Advanced Robotics
Issue or Number:10
Record Number:CaltechAUTHORS:20171102-092833279
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20171102-092833279
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:82883
Collection:CaltechAUTHORS
Deposited By: Sumanth Dathathri
Deposited On:02 Nov 2017 17:18
Last Modified:31 Jan 2020 23:03

Repository Staff Only: item control page