Advertisement

Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States

  • Sumanth DathathriEmail author
  • Ioannis Filippidis
  • Richard M. Murray
Conference paper
Part of the Springer Proceedings in Advanced Robotics book series (SPAR, volume 10)

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.

Keywords

Synthesis Temporal logic Generalized reactivity Binary-Decision diagrams Formal methods Discrete event systems 

Notes

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.

References

  1. 1.
    Alur, R., Moarref, S., Topcu, U.: Compositional synthesis with parametric reactive controllers. In: Proceedings of HSCC, pp. 215–224 (2016)Google Scholar
  2. 2.
    Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78, 911–938 (2012)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)CrossRefGoogle Scholar
  4. 4.
    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)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefGoogle Scholar
  6. 6.
    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)MathSciNetzbMATHGoogle Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Cohen, A., Namjoshi, K.S., Sa’ar, Y.: SPLIT: a compositional LTL verifier. In: CAV, pp. 558–561 (2010)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Dathathri, S., Murray, R.M.: Decomposing GR(1) games with singleton liveness guarantees for efficient synthesis. In: Proceedings of CDC, pp. 911–917 (2017)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Proceedings of CAV, pp. 333–339 (2016)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200, 35–61 (2005)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Proceedings of HVC, pp. 161–181 (2010)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    Lamport, L.: The temporal logic of actions. TOPLAS 16(3), 872–923 (1994)CrossRefGoogle Scholar
  20. 20.
    Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)Google Scholar
  21. 21.
    Majumdar, R.: Robots at the edge of the cloud. In: Proceedings of TACAS, pp. 3–13 (2016)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of PODC, pp. 377–408 (1990)Google Scholar
  24. 24.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–57 (1977)Google Scholar
  25. 25.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179–190 (1989)Google Scholar
  26. 26.
    Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of ICCAD, pp. 42–47 (1993)Google Scholar
  27. 27.
    van Dijk, T., Laarman, A., van de Pol, J.: Multi-core BDD operations for symbolic reachability. ENTCS (PDMC’12) 296, 127–143 (2013)Google Scholar
  28. 28.
    Wolff, E.M., Murray, R.M.: Optimal control of nonlinear systems with temporal logic specifications. In: Proceedings of ISRR, pp. 21–37 (2013)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Sumanth Dathathri
    • 1
    Email author
  • Ioannis Filippidis
    • 2
  • Richard M. Murray
    • 2
  1. 1.CMS, California Institute of TechnologyPasadenaUSA
  2. 2.CDS, California Institute of TechnologyPasadenaUSA

Personalised recommendations