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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Available from PyPI: https://pypi.org/project/dd/, https://pypi.org/project/omega/, and https://pypi.org/project/tulip/.
References
Alur, R., Moarref, S., Topcu, U.: Compositional synthesis with parametric reactive controllers. In: Proceedings of HSCC, pp. 215–224 (2016)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78, 911–938 (2012)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)
Browne, A., Clarke, E., Jha, S., Long, D., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci. 178(1), 237–255 (1997)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. TOC 40(2), 205–213 (1991)
Chinchali, S., Livingston, S.C., Topcu, U., Burdick, J.W., Murray, R.M.: Towards formal synthesis of reactive controllers for dexterous robotic manipulation. In: Proceedings of ICRA, pp. 5183–5189 (2012)
Cohen, A., Namjoshi, K.S., Sa’ar, Y.: SPLIT: a compositional LTL verifier. In: CAV, pp. 558–561 (2010)
Cohen, A., Namjoshi, K.S., Sa’ar, Y., Zuck, L.D., Kisyova, K.I.: Parallelizing a symbolic compositional model-checking algorithm. In: Proceedings of HVC, pp. 46–59 (2010)
Dathathri, S., Murray, R.M.: Decomposing GR(1) games with singleton liveness guarantees for efficient synthesis. In: Proceedings of CDC, pp. 911–917 (2017)
DeCastro, J.A., Alonso-Mora, J., Raman, V., Rus, D., Kress-Gazit, H.: Collision-free reactive mission and motion planning for multi-robot systems. In: Proceedings of ISRR, pp. 459–476 (2015)
Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Proceedings of CAV, pp. 333–339 (2016)
Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional mu-calculus. In: IEEE Computer Society Press LICS, pp. 267–278 (1986)
Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., Murray, R.M.: Control design for hybrid systems with TuLiP: the temporal logic planning toolbox. In: Proceedings of CCA, pp. 1030–1041 (2016)
Filippidis, I., Murray, R.M., Holzmann, G.J.: A multi-paradigm language for reactive synthesis. In: 4\(^{th}\) work. on synthesis, SYNT, pp. 73–97 (2015)
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200, 35–61 (2005)
Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Proceedings of HVC, pp. 161–181 (2010)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Where’s Waldo? sensor-based temporal logic motion planning. In: Proceedings of ICRA, pp. 3116–3121 (2007)
Lamport, L.: The temporal logic of actions. TOPLAS 16(3), 872–923 (1994)
Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)
Majumdar, R.: Robots at the edge of the cloud. In: Proceedings of TACAS, pp. 3–13 (2016)
Maniatopoulos, S., Schillinger, P., Pong, V., Conner, D.C., Kress-Gazit, H.: Reactive high-level behavior synthesis for an Atlas humanoid robot. In: Proceedings of ICRA, pp. 4192–4199 (2016)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of PODC, pp. 377–408 (1990)
Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–57 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179–190 (1989)
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of ICCAD, pp. 42–47 (1993)
van Dijk, T., Laarman, A., van de Pol, J.: Multi-core BDD operations for symbolic reachability. ENTCS (PDMC’12) 296, 127–143 (2013)
Wolff, E.M., Murray, R.M.: Optimal control of nonlinear systems with temporal logic specifications. In: Proceedings of ISRR, pp. 21–37 (2013)
Acknowledgements
This work is sponsored in part by TerraSwarm, a funded center of STARnet, a Semiconductor Research Corporation (SRC) program sponsored by MARCO and DARPA.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Dathathri, S., Filippidis, I., Murray, R.M. (2020). Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States. In: Amato, N., Hager, G., Thomas, S., Torres-Torriti, M. (eds) Robotics Research. Springer Proceedings in Advanced Robotics, vol 10. Springer, Cham. https://doi.org/10.1007/978-3-030-28619-4_57
Download citation
DOI: https://doi.org/10.1007/978-3-030-28619-4_57
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-28618-7
Online ISBN: 978-3-030-28619-4
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)