1932
0
  1. Home
  2. A-Z Publications
  3. Annual Review of Control, Robotics, and Autonomous Systems
  4. Volume 2, 2019
  5. Article

Annual Review of Control, Robotics, and Autonomous Systems

Volume 2, 2019

Formal Methods for Control Synthesis: An Optimization Perspective

Abstract

In control theory, complicated dynamics such as systems of (nonlinear) differential equations are controlled mostly to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimizing a certain cost along the trajectories of a stable system. In formal verification (model checking), simple systems, such as finite-state transition graphs that model computer programs or digital circuits, are checked against rich specifications given as formulas of temporal logics. The formal synthesis problem, in which the goal is to synthesize or control a finite system from a temporal logic specification, has recently received increased interest. In this article, we review some recent results on the connection between optimal control and formal synthesis. Specifically, we focus on the following problem: Given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification. We first provide a short overview of automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification. We then provide a detailed overview of a class of methods that rely on mapping the specification and the dynamics to constraints of an optimization problem. We discuss advantages and limitations of these two types of approaches and suggest directions for future research.

Keyword(s): formal methods, mathematical programming, model predictive control, temporal logics
Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-053018-023717
2019-05-03
2024-05-12
Loading full text...

Full text loading...

/deliver/fulltext/control/2/1/annurev-control-053018-023717.html?itemId=/content/journals/10.1146/annurev-control-053018-023717&mimeType=html&fmt=ahah

Literature Cited

  1. 1.  Baier C, Katoen JP 2008. Principles of Model Checking Cambridge, MA: MIT Press
  2. 2.  Hinton A, Kwiatkowska M, Norman G, Parker D 2006. PRISM: a tool for automatic verification of probabilistic systems. Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006 H Hermanns, J Palsberg441–44 Berlin: Springer
     [Google Scholar]
  3. 3.  Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M et al. 2002. NuSMV version 2: an open source tool for symbolic model checking. Computer Aided Verification: 14th International Conference, CAV 2002 E Brinksma, K Guldstrand Larsen359–64 Berlin: Springer
     [Google Scholar]
  4. 4.  Smith S, Tumova J, Belta C, Rus D 2011. Optimal path planning for surveillance with temporal logic constraints. Int. J. Robot. Res. 30:1695–708
     [Google Scholar]
  5. 5.  Chatterjee K, Doyen L, Henzinger TA, Raskin JF 2006. Algorithms for omega-regular games with imperfect information. Computer Science Logic: 20th International Workshop, CSL 2006 Z Èsik287–302 Berlin: Springer
     [Google Scholar]
  6. 6.  Ding X, Smith SL, Belta C, Rus D 2014. Optimal control of Markov decision processes with linear temporal logic constraints. IEEE Trans. Autom. Control 59:1244–57
     [Google Scholar]
  7. 7.  Tabuada P, Pappas G 2006. Linear time logic control of discrete-time linear systems. Trans. Autom. Control 51:1862–77
     [Google Scholar]
  8. 8.  Gol EA, Lazar M, Belta C 2012. Language-guided controller synthesis for discrete-time linear systems. Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control New York: ACM
     [Google Scholar]
  9. 9.  Wongpiromsarn T, Topcu U, Murray RR 2009. Receding horizon temporal logic planning for dynamical systems. Proceedings of the 48th IEEE Conference on Decision and Control (CDC) Held Jointly with 2009 28th Chinese Control Conference5997–6004 New York: IEEE
     [Google Scholar]
  10. 10.  Kloetzer M, Belta C 2008. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control 53:287–97
     [Google Scholar]
  11. 11.  Yordanov B, Tumova J, Cerna I, Barnat J, Belta C 2012. Temporal logic control of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 57:1491–504
     [Google Scholar]
  12. 12.  Belta C, Yordanov B, Gol EA 2017. Formal Methods for Discrete-Time Dynamical Systems Cham, Switz.: Springer
  13. 13.  Tarjan R 1971. Depth-first search and linear graph algorithms. 12th Annual Symposium on Switching and Automata Theory (SWAT 1971)114–21 New York: IEEE
     [Google Scholar]
  14. 14.  Gol EA, Belta C 2013. Time-constrained temporal logic control of multi-affine systems. Nonlinear Anal. Hybrid Syst. 10:21–23
     [Google Scholar]
  15. 15.  Bertsimas D, Tsitsiklis JN 1997. Introduction to Linear Optimization Belmont, MA: Athena Sci.
  16. 16.  Rawlings JB, Mayne DQ 2009. Model Predictive Control: Theory and Design Madison, WI: Nob Hill
  17. 17.  Bemporad A, Morari M 1999. Control of systems integrating logic, dynamics, and constraints. Automatica 35:407–27
     [Google Scholar]
  18. 18.  Ulusoy A, Belta C 2014. Receding horizon temporal logic control in dynamic environments. Int. J. Robot. Res. 33:1593–607
     [Google Scholar]
  19. 19.  Maler O, Nickovic D 2004. Monitoring temporal properties of continuous signals. Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems Y Lakhnech, S Yovine152–66 Berlin: Springer
     [Google Scholar]
  20. 20.  Koymans R 1990. Specifying real-time properties with metric temporal logic. Real-Time Syst. 2:255–99
     [Google Scholar]
  21. 21.  Jing G, Ehlers R, Kress-Gazit H 2013. Shortcut through an evil door: optimality of correct-by-construction controllers in adversarial environments. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems4796–802 New York: IEEE
     [Google Scholar]
  22. 22.  Svorenova M, Cerna I, Belta C 2015. Optimal temporal logic control for deterministic transition systems with probabilistic penalties. IEEE Trans. Autom. Control 60:1528–41
     [Google Scholar]
  23. 23.  Ding XC, Belta C, Cassandras CG 2010. Receding horizon surveillance with temporal logic specifications. 49th IEEE Conference on Decision and Control256–61 New York: IEEE
     [Google Scholar]
  24. 24.  Ding XC, Lazar M, Belta C 2012. Receding horizon temporal logic control for finite deterministic systems. 12th American Control Conference715–20 New York: IEEE
     [Google Scholar]
  25. 25.  Gol EA, Lazar M, Belta C 2014. Language-guided controller design for linear systems. IEEE Trans. Autom. Control 59:1163–76
     [Google Scholar]
  26. 26.  Pola G, Girard A, Tabuada P 2008. Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44:2508–16
     [Google Scholar]
  27. 27.  Rungger M, Reissig G 2017. Arbitrarily precise abstractions for optimal controller synthesis. 2017 IEEE 56th Annual Conference on Decision and Control1761–68 New York: IEEE
     [Google Scholar]
  28. 28.  Papusha I, Fu J, Topcu U, Murray RM 2016. Automata theory meets approximate dynamic programming: optimal control with temporal logic constraints. 2016 IEEE 55th Conference on Decision and Control434–40 New York: IEEE
     [Google Scholar]
  29. 29.  Horowitz MB, Wolff EM, Murray RM 2014. A compositional approach to stochastic optimal control with co-safe temporal logic specifications. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems1466–73 New York: IEEE
     [Google Scholar]
  30. 30.  Wolff EM, Topcu U, Murray RM 2012. Optimal control with weighted average costs and temporal logic specifications. Robotics: Science and Systems VIII N Roy, P Newman, S Srinivasa449–56 Cambridge, MA: MIT Press
     [Google Scholar]
  31. 31.  Li L, Fu J 2017. Sampling-based approximate optimal temporal logic planning. 2017 IEEE International Conference on Robotics and Automation1328–35 New York: IEEE
     [Google Scholar]
  32. 32.  Donzé A, Maler O 2010. Robust satisfaction of temporal logic over real-valued signals. Formal Modeling and Analysis of Timed Systems: 8th International Conference, FORMATS 2010 K Chatterjee, TA Henzinger92–106 Berlin: Springer
     [Google Scholar]
  33. 33.  Dokhanchi A, Hoxha B, Fainekos G 2014. On-line monitoring for temporal logic robustness. Runtime Verification, 5th International Conference, RV 2014 B Bonakdarpour, SA Smolka1–20 Cham, Switz.: Springer
     [Google Scholar]
  34. 34.  Ouaknine J, Worrell J 2006. Safety metric temporal logic is fully decidable. Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006 H Hermanns, J Palsberg411–25 Berlin: Springer
     [Google Scholar]
  35. 35.  Donzé A 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. Computer Aided Verification: 22nd International Conference, CAV 2010 T Touili, B Cook, P Jackson167–70 Berlin: Springer
     [Google Scholar]
  36. 36.  Donzé A, Ferrère T, Maler O 2013. Efficient robust monitoring for STL. Computer Aided Verification: 25th International Conference, CAV 2013 N Sharygina, H Veith264–79 Berlin: Springer
     [Google Scholar]
  37. 37.  Fainekos GE, Pappas GJ 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410:4262–91
     [Google Scholar]
  38. 38.  Heemels W, Schutter BD, Bemporad A 2001. Equivalence of hybrid dynamical models. Automatica 37:1085–91
     [Google Scholar]
  39. 39.  Bemporad A, Ferrari-Trecate G, Morari M 2000. Observability and controllability of piecewise affine and hybrid systems. IEEE Trans. Autom. Control 45:1864–76
     [Google Scholar]
  40. 40.  De Schutter B, Van den Boom T 2001. Model predictive control for max-min-plus-scaling systems. Proceedings of the 2001 American Control Conference 1319–24 New York: IEEE
     [Google Scholar]
  41. 41.  Heemels W, Schumacher JM, Weiland S 2000. Linear complementarity systems. SIAM J. Appl. Math. 60:1234–69
     [Google Scholar]
  42. 42.  Anitescu M, Potra FA 1997. Formulating dynamic multi-rigid-body contact problems with friction as solvable linear complementarity problems. Nonlinear Dyn. 14:231–47
     [Google Scholar]
  43. 43.  De Schutter B, De Moor B 1997. The extended linear complementarity problem and the modeling and analysis of hybrid systems. Hybrid Systems V P Antsaklis, M Lemmon, W Kohn, A Nerode, S Sastry70–85 Berlin: Springer
     [Google Scholar]
  44. 44.  Richards A, How JP 2002. Aircraft trajectory planning with collision avoidance using mixed integer linear programming. Proceedings of the 2002 American Control Conference 31936–41 New York: IEEE
     [Google Scholar]
  45. 45.  Karaman S, Frazzoli E 2011. Linear temporal logic vehicle routing with applications to multi-UAV mission planning. Int. J. Robust Nonlinear Control 21:1372–95
     [Google Scholar]
  46. 46.  Mellinger D, Kushleyev A, Kumar V 2012. Mixed-integer quadratic program trajectory generation for heterogeneous quadrotor teams. 2012 IEEE International Conference on Robotics and Automation477–83 New York: IEEE
     [Google Scholar]
  47. 47.  Wang Y, De Schutter B, van den Boom TJ, Ning B 2013. Optimal trajectory planning for trains—a pseudospectral method and a mixed integer linear programming approach. Transp. Res. C 29:97–114
     [Google Scholar]
  48. 48.  Haghighi I, Sadraddini S, Belta C 2016. Robotic swarm control from spatio-temporal specifications. 2016 IEEE 55th Conference on Decision and Control5708–13 New York: IEEE
     [Google Scholar]
  49. 49.  Liu Z, Dai J, Wu B, Lin H 2017. Communication-aware motion planning for multi-agent systems from signal temporal logic specifications. 2017 American Control Conference2516–21 New York: IEEE
     [Google Scholar]
  50. 50.  Sahin YE, Nilsson P, Ozay N 2017. Provably-correct coordination of large collections of agents with counting temporal logic constraints. Proceedings of the 8th International Conference on Cyber-Physical Systems249–58 New York: ACM
     [Google Scholar]
  51. 51.  Liu Z, Wu B, Dai J, Lin H 2017. Distributed communication-aware motion planning for multi-agent systems from STL and SpaTeL specifications. 2017 IEEE 56th Annual Conference on Decision and Control4452–57 New York: IEEE
     [Google Scholar]
  52. 52.  Haghighi I, Jones A, Kong Z, Bartocci E, Gros R, Belta C 2015. SpaTeL: a novel spatial-temporal logic and its applications to networked systems. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control189–98 New York: ACM
     [Google Scholar]
  53. 53.  Shoukry Y, Nuzzo P, Balkan A, Saha I, Sangiovanni-Vincentelli AL et al. 2017. Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming. 2017 IEEE 56th Annual Conference on Decision and Control1132–37 New York: IEEE
     [Google Scholar]
  54. 54.  Shoukry Y, Nuzzo P, Saha I, Sangiovanni-Vincentelli AL, Seshia SA et al. 2016. Scalable lazy SMT-based motion planning. 2016 IEEE 55th Conference on Decision and Control6683–88 New York: IEEE
     [Google Scholar]
  55. 55.  Shoukry Y, Nuzzo P, Sangiovanni-Vincentelli AL, Seshia SA, Pappas GJ, Tabuada P 2017. SMC: satisfiability modulo convex optimization. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control19–28 New York: ACM
     [Google Scholar]
  56. 56.  Abbas H, Winn A, Fainekos G, Julius AA 2014. Functional gradient descent method for metric temporal logic specifications. 2014 American Control Conference2312–17 New York: IEEE
     [Google Scholar]
  57. 57.  Pant YV, Abbas H, Quaye RA, Mangharam R 2018. Fly-by-logic: control of multi-drone fleets with temporal logic objectives. 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems186–97 New York: IEEE
     [Google Scholar]
  58. 58.  Pant YV, Abbas H, Mangharam R 2017. Smooth operator: control using the smooth robustness of temporal logic. 2017 IEEE Conference on Control Technology and Applications1235–40 New York: IEEE
     [Google Scholar]
  59. 59.  Karaman S, Sanfelice RG, Frazzoli E 2008. Optimal control of mixed logical dynamical systems with linear temporal logic specifications. 2008 47th IEEE Conference on Decision and Control2117–22 New York: IEEE
     [Google Scholar]
  60. 60.  Raman V, Donzé A, Maasoumy M, Murray RM, Sangiovanni-Vincentelli A, Seshia SA 2014. Model predictive control with signal temporal logic specifications. 53rd IEEE Conference on Decision and Control81–87 New York: IEEE
     [Google Scholar]
  61. 61.  Sadraddini S, Belta C 2019. Formal synthesis of control strategies for positive monotone systems. IEEE Trans. Autom. Control 64:480–95
     [Google Scholar]
  62. 62.  Abbas H, Fainekos G, Sankaranarayanan S, Ivančić F, Gupta A 2013. Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12:95
     [Google Scholar]
  63. 63.  Abbas H, O'Kelly M, Mangharam R 2017. Relaxed decidability and the robust semantics of metric temporal logic. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control217–25 New York: ACM
     [Google Scholar]
  64. 64.  Vielma JP 2015. Mixed integer linear programming formulation techniques. SIAM Rev. 57:3–57
     [Google Scholar]
  65. 65.  Wolff EM, Murray RM 2016. Optimal control of nonlinear systems with temporal logic specifications. Robotics Research: The 16th International Symposium ISRR M Inaba, P Corke21–37 Cham, Switz.: Springer
     [Google Scholar]
  66. 66.  Mazo M, Davitian A, Tabuada P 2010. PESSOA: a tool for embedded controller synthesis. Computer Aided Verification: 22nd International Conference, CAV 2010 T Touili, B Cook, P Jackson566–69 Berlin: Springer
     [Google Scholar]
  67. 67.  Sadraddini S 2018. Formal methods for resilient control PhD Thesis, Boston Univ., Boston
  68. 68.  Wolff EM, Topcu U, Murray RM 2014. Optimization-based trajectory generation with linear temporal logic specifications. 2014 IEEE International Conference on Robotics and Automation5319–25 New York: IEEE
     [Google Scholar]
  69. 69.  Bemporad A, Borrelli F, Morari M 2000. Piecewise linear optimal controllers for hybrid systems. Proceedings of the 2000 American Control Conference 21190–94 New York: IEEE
     [Google Scholar]
  70. 70.  Löfberg J 2003. Minimax approaches to robust model predictive control PhD Thesis, Linköping Univ., Linköping, Swed.
  71. 71.  Farahani SS, Raman V, Murray RM 2015. Robust model predictive control for signal temporal logic synthesis. IFAC-PapersOnLine 48:323–28
     [Google Scholar]
  72. 72.  Sadraddini S, Belta C 2015. Robust temporal logic model predictive control. 2015 53rd Annual Allerton Conference on Communication, Control, and Computing772–79 New York: IEEE
     [Google Scholar]
  73. 73.  Raman V, Donzé A, Sadigh D, Murray RM, Seshia SA 2015. Reactive synthesis from signal temporal logic specifications. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control239–48 New York: ACM
     [Google Scholar]
  74. 74.  Sadigh D, Kapoor A 2015. Safe control under uncertainty. arXiv:1510.07313 [cs.SY]
  75. 75.  Mehr N, Sadigh D, Horowitz R, Sastry SS, Seshia SA 2017. Stochastic predictive freeway ramp metering from signal temporal logic specifications. 2017 American Control Conference4884–89 New York: IEEE
     [Google Scholar]
  76. 76.  Farahani SS, Majumdar R, Prabhu VS, Soudjani SEZ 2017. Shrinking horizon model predictive control with chance-constrained signal temporal logic specifications. 2017 American Control Conference1740–46 New York: IEEE
     [Google Scholar]
  77. 77.  Saha S, Julius AA 2016. An MILP approach for real-time optimal controller synthesis with metric temporal logic specifications. 2016 American Control Conference1105–10 New York: IEEE
     [Google Scholar]
  78. 78.  Lindemann L, Dimarogonas DV 2017. Robust motion planning employing signal temporal logic. 2017 American Control Conference2950–55 New York: IEEE
     [Google Scholar]
  79. 79.  Ghosh S, Sadigh D, Nuzzo P, Raman V, Donzé A et al. 2016. Diagnosis and repair for synthesis from signal temporal logic specifications. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control31–40 New York: ACM
     [Google Scholar]
  80. 80.  Blanchini F 1999. Set invariance in control—a survey. Automatica 35:1747–67
     [Google Scholar]
  81. 81.  Kerrigan EC, Kouramas KI, Mayne DQ, Raković SV 2005. Invariant approximations of the minimal robust positively invariant set. IEEE Trans. Autom. Control 50:406–10
     [Google Scholar]
  82. 82.  Kerrigan EC 2000. Robust constraint satisfaction: invariant sets and predictive control PhD Thesis, Univ. Cambridge, Cambridge, UK
  83. 83.  Sadraddini S, Rudan J, Belta C 2017. Formal synthesis of distributed optimal traffic control policies. Proceedings of the 8th International Conference on Cyber-Physical Systems15–24 New York: ACM
     [Google Scholar]
  84. 84.  Rungger M, Tabuada P 2017. Computing robust controlled invariant sets of linear systems. IEEE Trans. Autom. Control 62:3665–70
     [Google Scholar]
  85. 85.  Lindemann L, Verginis CK, Dimarogonas DV 2017. Prescribed performance control for signal temporal logic specifications. 2017 IEEE 56th Annual Conference on Decision and Control2997–3002 New York: IEEE
     [Google Scholar]
  86. 86.  Lindemann L, Dimarogonas DV 2018. Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3:96–101
     [Google Scholar]
  87. 87.  Jha S, Raj S, Jha SK, Shankar N 2018. Duality-based nested controller synthesis from STL specifications for stochastic linear systems. Formal Modeling and Analysis of Timed Systems: 16th International Conference, FORMATS 2018 D Jansen, P Prabhakar235–51 Cham, Switz.: Springer
     [Google Scholar]
  88. 88.  Xu Z, Julius A, Chow JH 2019. Energy storage controller synthesis for power systems with temporal logic specifications. IEEE Syst. J 13:748–59
     [Google Scholar]
  89. 89.  Sadraddini S, Belta C 2018. Formal guarantees in data-driven model identification and control synthesis. Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control147–56 New York: ACM
     [Google Scholar]
  90. 90.  Majumdar A, Ahmadi AA, Tedrake R 2013. Control design along trajectories with sums of squares programming. 2013 IEEE International Conference on Robotics and Automation4054–61 New York: IEEE
     [Google Scholar]
  91. 91.  Tedrake R, Manchester IR, Tobenkin M, Roberts JW 2010. LQR-trees: feedback motion planning via sums-of-squares verification. Int. J. Robot. Res. 29:1038–52
     [Google Scholar]
  92. 92.  Langson W, Chryssochoos I, Raković S, Mayne DQ 2004. Robust model predictive control using tubes. Automatica 40:125–33
     [Google Scholar]
  93. 93.  Mayne DQ, Seron MM, Raković S 2005. Robust model predictive control of constrained linear systems with bounded disturbances. Automatica 41:219–24
     [Google Scholar]
  94. 94.  Limon D, Alvarado I, Alamo T, Camacho EF 2010. Robust tube-based MPC for tracking of constrained linear systems with additive disturbances. J. Process Control 20:248–60
     [Google Scholar]
  95. 95.  Ghasemi MS, Afzalian AA 2017. Robust tube-based MPC of constrained piecewise affine systems with bounded additive disturbances. Nonlinear Anal. Hybrid Syst. 26:86–100
     [Google Scholar]
  96. 96.  Raković SV, Kerrigan EC, Mayne DQ, Kouramas KI 2007. Optimized robust control invariance for linear discrete-time systems: theoretical foundations. Automatica 43:831–41
     [Google Scholar]
  97. 97.  Raković SV, Baric M 2010. Parameterized robust control invariant sets for linear systems: theoretical advances and computational remarks. IEEE Trans. Autom. Control 55:1599–614
     [Google Scholar]
/content/journals/10.1146/annurev-control-053018-023717
Loading
Formal Methods for Control Synthesis: An Optimization Perspective
Annual Review of Control, Robotics, and Autonomous Systems 2, 115 (2019); https://doi.org/10.1146/annurev-control-053018-023717
/content/journals/10.1146/annurev-control-053018-023717
/content/journals/10.1146/annurev-control-053018-023717
Loading

Data & Media loading...

  • Article Type: Review Article

Most Cited Most Cited RSS feed

This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error