A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control

  • Robert P. GoldmanEmail author
  • Daniel Bryce
  • Michael J. S. Pelican
  • David J. Musliner
  • Kyungmin Bae
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)


This paper describes Hy-CIRCA, an architecture for verified, correct-by-construction planning and execution for hybrid systems, including nonlinear continuous dynamics. Hy-CIRCA addresses the high computational complexity of such systems by first planning at an abstract level, and then progressively refining the original plan. Hy-CIRCA integrates the dReal nonlinear SMT solver with enhanced versions of the SHOP2 HTN planner and the CIRCA Controller Synthesis Module (CSM). SHOP2 computes a high level nominal mission plan, the CIRCA CSM develops reactive controllers for the mission steps, accounting for disturbances, and dReal verifies that the plans are correct with respect to continuous dynamics. In this way, Hy-CIRCA decomposes reasoning about the plan and judiciously applies the different solvers to the problems they are best at.



Thanks to the anonymous reviewers, Laura Humphrey, Sicun Gao, and Soonho Kong for comments and advice. This material is based upon work supported by the U.S. Air Force (AFRL) under Contract No. FA9550-15-C-0030. Any opinions, findings and conclusions, or recommendations expressed in this material are those of the authors and do not reflect the views of the U.S. Air Force (AFRL).


  1. 1.
    Alur, R., Dang, T., Esposito, J., Fierro, R., Hur, Y., Ivančić, F., Kumar, V., Lee, I., Mishra, P., Pappas, G.J., Sokolsky, O.: Hierarchical hybrid modeling of embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, p. 14. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Bryce, D., Gao, S., Musliner, D.J., Goldman, R.P.: SMT-based nonlinear PDDL+ planning. In: Proceedings National Conference on Artificial Intelligence, pp. 3247–3253 (2015)Google Scholar
  3. 3.
    Cushing, W., Kambhampati, S., Mausam, Weld, D.S.: When is temporal planning really temporal? In: Veloso, M.M. (ed.) Proceedings of the 20th International Joint Conference on Artificial Intelligence, pp. 1852–1859 (2007)Google Scholar
  4. 4.
    Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  5. 5.
    Gat, E.: Three-layer architectures. In: Kortenkamp, D., Bonasso, R.P., Murphy, R. (eds.) Artificial Intelligence and Mobile Robots. AAAI Press/MIT Press, Cambridge, MA (1998)Google Scholar
  6. 6.
    Goldman, R.P., Musliner, D.J., Pelican, M.J.S.: Exploiting implicit representations in timed automaton verification for controller synthesis. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, p. 225. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Goldman, R.P., Pelican, M.J.S., Musliner, D.J.: Guiding planner backjumping using verifier traces. In: Zilberstein, S., Koehler, J., Koenig, S. (eds.) Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling, pp. 279–286, June 2004Google Scholar
  8. 8.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Miller, C.A., Goldman, R.P., Funk, H.B., Wu, P., Pate, B.: A playbook approach to variable autonomy control: application for control of multiple, heterogeneous unmanned air vehicles. In: AHS 60th Annual Forum Proceedings, pp. 2146–2157. American Helicopter Society, Alexandria, VA, June 2004Google Scholar
  10. 10.
    Musliner, D.J., Durfee, E.H., Shin, K.G.: CIRCA: a cooperative intelligent real-time control architecture. IEEE Trans. Syst. Man Cybern. 23(6), 1561–1574 (1993)CrossRefGoogle Scholar
  11. 11.
    Nau, D., Au, T.C., Ilghami, O., Kuter, U., Murdock, J.W., Wu, D., Yaman, F.: SHOP2: an HTN planning system. J. Artif. Intell. Res. 20, 379–404 (2003)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Robert P. Goldman
    • 1
    Email author
  • Daniel Bryce
    • 1
  • Michael J. S. Pelican
    • 1
  • David J. Musliner
    • 1
  • Kyungmin Bae
    • 2
  1. 1.SIFT, LLCMinneapolisUSA
  2. 2.Carnegie-Mellon UniversityPittsburghUSA

Personalised recommendations