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

Annual Review of Control, Robotics, and Autonomous Systems

Volume 1, 2018

Synthesis for Robots: Guarantees and Feedback for Robot Behavior

Abstract

Robot control for tasks such as moving around obstacles or grasping objects has advanced significantly in the last few decades. However, controlling robots to perform complex tasks is still accomplished largely by highly trained programmers in a manual, time-consuming, and error-prone process that is typically validated only through extensive testing. Formal methods are mathematical techniques for reasoning about systems, their requirements, and their guarantees. Formal synthesis for robotics refers to frameworks for specifying tasks in a mathematically precise language and automatically transforming these specifications into correct-by-construction robot controllers or into a proof that the task cannot be done. Synthesis allows users to reason about the task specification rather than its implementation, reduces implementation error, and provides behavioral guarantees for the resulting controller. This article reviews the current state of formal synthesis for robotics and surveys the landscape of abstractions, specifications, and synthesis algorithms that enable it.

Keyword(s): control, formal methods, high-level specifications, robotics, synthesis
Loading

Article metrics loading...

/content/journals/10.1146/annurev-control-060117-104838
2018-05-28
2024-04-16
Loading full text...

Full text loading...

/deliver/fulltext/control/1/1/annurev-control-060117-104838.html?itemId=/content/journals/10.1146/annurev-control-060117-104838&mimeType=html&fmt=ahah

Literature Cited

  1. 1.  Clarke EM, Wing JM 1996. Formal methods: state of the art and future directions. ACM Comput. Surv. 28:626–43
     [Google Scholar]
  2. 2.  Spenko M, Buerger S, Iagnemma K, eds. 2017. The DARPA Robotics Challenge finals. J. Field Robot 342, Spec. Issue New York: Wiley
     [Google Scholar]
  3. 3.  Loizou SSG, Kyriakopoulos KJ 2004. Automatic synthesis of multiagent motion tasks based on LTL specifications. 43rd IEEE Conference on Decision and Control153–58 New York: IEEE
     [Google Scholar]
  4. 4.  Kloetzer M, Belta C 2007. Temporal logic planning and control of robotic swarms by hierarchical abstractions. IEEE Trans. Robot. 23:320–30
     [Google Scholar]
  5. 5.  Karaman S, Frazzoli E 2008. Complex mission optimization for Multiple-UAVs using Linear Temporal Logic. 2008 American Control Conference2003–9 New York: IEEE
     [Google Scholar]
  6. 6.  Kress-Gazit H, Ayanian N, Pappas GJ, Kumar V 2008. Recycling controllers. 2008 IEEE International Conference on Automation Science and Engineering772–77 New York: IEEE
     [Google Scholar]
  7. 7.  Filippidis I, Dimarogonas DV, Kyriakopoulos KJ 2012. Decentralized multi-agent control from local LTL specifications. 2012 IEEE 51st Annual Conference on Decision and Control (CDC)6235–40 New York: IEEE
     [Google Scholar]
  8. 8.  Wongpiromsarn T, Ulusoy A, Belta C, Frazzoli E, Rus D 2013. Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications. 2013 IEEE International Conference on Robotics and Automation (ICRA)5011–18 New York: IEEE
     [Google Scholar]
  9. 9.  Raman V, Kress-Gazit H 2014. Synthesis for multi-robot controllers with interleaved motion. 2014 IEEE International Conference on Robotics and Automation (ICRA)4316–21 New York: IEEE
     [Google Scholar]
  10. 10.  Raman V 2014. Reactive switching protocols for multi-robot high-level tasks. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems336–41 New York: IEEE
     [Google Scholar]
  11. 11.  DeCastro JA, Alonso-Mora J, Raman V, Rus D, Kress-Gazit H 2018. Collision-free reactive mission and motion planning for multi-robot systems. Robotics Research 1 A Bicchi, W Burgard 459–76 Springer Proc. Adv. Robot . Vol. 2 Cham, Switz: Springer
     [Google Scholar]
  12. 12.  Wong KW, Kress-Gazit H 2015. Let's talk: autonomous conflict resolution for robots carrying out individual high-level tasks in a shared workspace. 2015 IEEE International Conference on Robotics and Automation (ICRA)339–45 New York: IEEE
     [Google Scholar]
  13. 13.  Tumova J, Dimarogonas DV 2016. Multi-agent planning under local LTL specifications and event-based synchronization. Automatica 70:239–48
     [Google Scholar]
  14. 14.  Saha I, Ramaithitima R, Kumar V, Pappas GJ, Seshia SA 2014. Automated composition of motion primitives for multi-robot systems from safe LTL specifications. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)1525–32 New York: IEEE
     [Google Scholar]
  15. 15.  Nedunuri S, Prabhu S, Moll M, Chaudhuri S, Kavraki LE 2014. SMT-based synthesis of integrated task and motion plans from plan outlines. 2014 IEEE International Conference on Robotics and Automation (ICRA)655–62 New York: IEEE
     [Google Scholar]
  16. 16.  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 Control (CDC)6683–88 New York: IEEE
     [Google Scholar]
  17. 17.  Raman V, Kress-Gazit H 2013. Explaining impossible high-level robot behaviors. IEEE Trans. Robot. 29:94–104
     [Google Scholar]
  18. 18.  Lignos C, Raman V, Finucane C, Marcus M, Kress-Gazit H 2014. Provably correct reactive control from natural language. Auton. Robots 38:89–105
     [Google Scholar]
  19. 19.  DeCastro JA, Ehlers R, Rungger M, Balkan A, Kress-Gazit H 2017. Automated generation of dynamics-based runtime certificates for high-level control. Discrete Event Dyn. Syst. Theory Appl. 27:371–405
     [Google Scholar]
  20. 20.  Dokhanchi A, Hoxha B, Fainekos G 2015. Metric interval temporal logic specification elicitation and debugging. 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)70–79 New York: IEEE
     [Google Scholar]
  21. 21.  Fainekos GE 2011. Revising temporal logic specifications for motion planning. 2011 IEEE International Conference on Robotics and Automation (ICRA)40–45 New York: IEEE
     [Google Scholar]
  22. 22.  Tumova J, Hall GC, Karaman S, Frazzoli E, Rus D 2013. Least-violating control strategy synthesis with safety rules. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control1–10 New York: ACM
     [Google Scholar]
  23. 23.  Guo M, Johansson KH, Dimarogonas DV 2013. Revising motion planning under linear temporal logic specifications in partially known workspaces. 2013 IEEE International Conference on Robotics and Automation (ICRA)5025–32 New York: IEEE
     [Google Scholar]
  24. 24.  Kim K, Fainekos G, Sankaranarayanan S 2015. On the minimal revision problem of specification automata. Int. J. Robot. Res. 34:1515–35
     [Google Scholar]
  25. 25.  Lahijanian M, Almagor S, Fried D, Kavraki LE, Vardi MY 2015. This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence3664–71 Menlo Park, CA: AAAI Press
     [Google Scholar]
  26. 26.  Lahijanian M, Kwiatkowska M 2016. Specification revision for Markov decision processes with optimal trade-off. 2016 IEEE 55th Conference on Decision and Control7411–18 New York: IEEE
     [Google Scholar]
  27. 27.  Li W, Dworkin L, Seshia SA 2011. Mining assumptions for synthesis. 2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE)43–50 New York: IEEE
     [Google Scholar]
  28. 28.  Alur R, Moarref S, Topcu U 2013. Counter-strategy guided refinement of GR(1) temporal logic specifications. 2013 Formal Methods in Computer-Aided Design (FMCAD)26–33 New York: IEEE
     [Google Scholar]
  29. 29.  DeCastro JA, Raman V, Kress-Gazit H 2015. Dynamics-driven adaptive abstraction for reactive high-level mission and motion planning. 2015 IEEE International Conference on Robotics and Automation (ICRA)369–76 New York: IEEE
     [Google Scholar]
  30. 30.  DeCastro JA, Kress-Gazit H 2016. Nonlinear controller synthesis and automatic workspace partitioning for reactive high-level behaviors. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control225–34 New York: ACM
     [Google Scholar]
  31. 31.  Johnson B, Kress-Gazit H 2015. Analyzing and revising synthesized controllers for robots with sensing and actuation errors. Int. J. Robot. Res. 34:816–32
     [Google Scholar]
  32. 32.  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]
  33. 33.  McDermott D, Ghallab M, Howe A, Knoblock C, Ram A et al. 1998. PDDL—the Planning Domain Definition Language Tech. Rep. CVC TR-98-003/DCS TR-1165, Cent. Comput. Vision Control, Yale Univ., New Haven, CT
  34. 34.  Bacchus F, Kabanza F 1996. Planning for temporally extended goals. Proceedings of the Thirteenth National Conference on Artificial Intelligence1215–22 Menlo Park, CA: AAAI Press
     [Google Scholar]
  35. 35.  Giacomo GD, Vardi MY 2000. Automata-theoretic approach to planning for temporally extended goals. ECP '99: Proceedings of the 5th European Conference on Planning226–38 Berlin: Springer
     [Google Scholar]
  36. 36.  Schoppers M 1987. Universal plans for reactive robots in unpredictable environments. Proceedings of the Tenth International Joint Conference on Artificial Intelligence (IJCAI-87) J McDermott 1039–46 Burlington, MA: Morgan Kaufmann
     [Google Scholar]
  37. 37.  Pryor L, Collins G 1996. Planning for contingencies: a decision-based approach. J. Artif. Intell. Res. 4:287–339
     [Google Scholar]
  38. 38.  Heger FW, Singh S 2010. Robust robotic assembly through contingencies, plan repair and re-planning. 2010 IEEE International Conference on Robotics and Automation (ICRA)3825–30 New York: IEEE
     [Google Scholar]
  39. 39.  Cimatti A, Pistore M, Roveri M, Traverso P 2003. Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147:35–84
     [Google Scholar]
  40. 40.  Cimatti A, Roveri M, Bertoli P 2004. Conformant planning via symbolic model checking and heuristic search. Artif. Intell. 159:127–206
     [Google Scholar]
  41. 41.  Ehlers R, Lafortune S, Tripakis S, Vardi MY 2017. Supervisory control and reactive synthesis: a comparative introduction. Discrete Event Dyn. Syst. Theory Appl. 27:209–60
     [Google Scholar]
  42. 42.  Clarke EM, Grumberg O, Peled DA 1999. Model Checking Cambridge, MA: MIT Press
  43. 43.  Rutten JJMM, Kwiatkowska M, Gethin N, Parker D 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems Providence, RI: Am. Math. Soc.
  44. 44.  Milner R. 1999. Communicating and Mobile Systems: The π Calculus Cambridge, UK: Cambridge Univ. Press
     [Google Scholar]
  45. 45.  Habets L, van Schuppen JH 2004. A control problem for affine dynamical systems on a full-dimensional polytope. Automatica 40:21–35
     [Google Scholar]
  46. 46.  Conner DC, Rizzi AA, Choset H 2003. Composition of local potential functions for global robot control and navigation. 2003 IEEE/RSJ International Conference on Intelligent Robots and Systems 43546–51 New York: IEEE
     [Google Scholar]
  47. 47.  Lindemann SR, LaValle SM 2005. Smoothly blending vector fields for global robot navigation. 44th IEEE Conference on Decision and Control207–14 New York: IEEE
     [Google Scholar]
  48. 48.  Rimon E, Koditschek DE 1992. Exact robot navigation using artificial potential functions. IEEE Trans. Robot. Autom. 8:501–18
     [Google Scholar]
  49. 49.  Ayanian N, Kumar V 2010. Decentralized feedback controllers for multiagent teams in environments with obstacles. IEEE Trans. Robot. 26:878–87
     [Google Scholar]
  50. 50.  Pola G, Girard A, Tabuada P 2008. Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44:2508–16
     [Google Scholar]
  51. 51.  Zamani M, Pola G, Mazo M, Tabuada P 2012. Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Autom. Control 57:1804–9
     [Google Scholar]
  52. 52.  Liu J, Ozay N 2016. Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22:1–15
     [Google Scholar]
  53. 53.  Mazo M, Davitian A, Tabuada P 2010. PESSOA: a tool for embedded controller synthesis. CAV 2010: Computer Aided Verification T Touli, B Cook, P Jackson 566–69 Berlin: Springer
     [Google Scholar]
  54. 54.  Mouelhi S, Girard A, Gössler G 2013. CoSyMA: a tool for controller synthesis using multi-scale abstractions. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control83–88 New York: ACM
     [Google Scholar]
  55. 55.  Rungger M, Zamani M 2016. SCOTS: a tool for the synthesis of symbolic controllers. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control99–104 New York: ACM
     [Google Scholar]
  56. 56.  Mitchell IM, Bayen AM, Tomlin CJ 2005. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50:947–57
     [Google Scholar]
  57. 57.  Ding J, Gillula J, Huang H, Vitus MP, Zhang W, Tomlin CJ 2011. Hybrid systems in robotics: toward reachability-based controller design. IEEE Robot. Autom. Mag. 18:33–43
     [Google Scholar]
  58. 58.  Chen M, Tomlin CJ 2015. Exact and efficient Hamilton-Jacobi reachability for decoupled systems. 2015 54th IEEE Conference on Decision and Control (CDC)1297–303 New York: IEEE
     [Google Scholar]
  59. 59.  Conner DC, Choset H, Rizzi AA 2006. Integrated planning and control for convex-bodied nonholonomic systems using local feedback control policies. Robotics: Science and Systems II GS Sukhatme, S Schaal, W Burgard, D Fox, chap. 8 Cambridge, MA: MIT Press
     [Google Scholar]
  60. 60.  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]
  61. 61.  Tobenkin MM, Manchester IR, Tedrake R 2011. Invariant funnels around trajectories using sum-of-squares programming. IFAC Proc. Vol. 44:9218–23
     [Google Scholar]
  62. 62.  Majumdar A, Tobenkin M, Tedrake R 2012. Algebraic verification for parameterized motion planning libraries. 2012 American Control Conference (ACC)250–57 New York: IEEE
     [Google Scholar]
  63. 63.  Majumdar A, Tedrake R 2017. Funnel libraries for real-time robust feedback motion planning. Int. J. Robot. Res. 36:947–82
     [Google Scholar]
  64. 64.  Tedrake R 2014. Drake: a planning, control, and analysis toolbox for nonlinear dynamical systems http://drake.mit.edu
  65. 65.  DeCastro JA, Kress-Gazit H 2015. Synthesis of nonlinear continuous controllers for verifiably correct high-level, reactive behaviors. Int. J. Robot. Res. 34:378–94
     [Google Scholar]
  66. 66.  Raman V, Piterman N, Finucane C, Kress-Gazit H 2015. Timing semantics for abstraction and execution of synthesized high-level robot control. IEEE Trans. Robot. 31:591–604
     [Google Scholar]
  67. 67.  Sucan IA, Moll M, Kavraki LE 2012. The open motion planning library. IEEE Robot. Autom. Mag. 19:72–82
     [Google Scholar]
  68. 68.  Pnueli A, Rosner R 1989. On the synthesis of a reactive module. POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages179–90 New York: ACM
     [Google Scholar]
  69. 69.  Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa'ar Y 2012. Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78:911–38
     [Google Scholar]
  70. 70.  Kupferman O, Vardi MY 2001. Model checking of safety properties. Formal Methods Syst. Des. 19:291–314
     [Google Scholar]
  71. 71.  Baier C, Katoen JP 2008. Principles of Model Checking Cambridge, MA: MIT Press
  72. 72.  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 Yovine 152–66 Berlin: Springer
     [Google Scholar]
  73. 73.  Raman V, Donzé A, Maasoumy M, Murray RM, Sangiovanni-Vincentelli AL, Seshia SA 2014. Model predictive control with signal temporal logic specifications. 2014 53rd IEEE Conference on Decision and Control (CDC)81–87 New York: IEEE
     [Google Scholar]
  74. 74.  Fainekos GE, Pappas GJ 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410:4262–91
     [Google Scholar]
  75. 75.  Fainekos G, Kress-Gazit H, Pappas G 2005. Temporal logic motion planning for mobile robots. Proceedings of the 2005 IEEE International Conference on Robotics and Automation2020–25 New York: IEEE
     [Google Scholar]
  76. 76.  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]
  77. 77.  Lahijanian M, Kloetzer M, Itani S, Belta C, Andersson SB 2009. Automatic deployment of autonomous cars in a robotic urban-like environment (RULE). 2009 IEEE International Conference on Robotics and Automation2055–60 New York: IEEE
     [Google Scholar]
  78. 78.  Fainekos GE, Girard A, Kress-Gazit H, Pappas GJ 2009. Temporal logic motion planning for dynamic mobile robots. Automatica 45:343–52
     [Google Scholar]
  79. 79.  Smith SL, 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]
  80. 80.  Wolff EM, Topcu U, Murray RM 2013. Efficient reactive controller synthesis for a fragment of linear temporal logic. 2013 IEEE International Conference on Robotics and Automation5033–40 New York: IEEE
     [Google Scholar]
  81. 81.  Maly MR, Lahijanian M, Kavraki LE, Kress-Gazit H, Vardi MY 2013. Iterative temporal motion planning for hybrid systems in partially unknown environments. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control353–62 New York: ACM
     [Google Scholar]
  82. 82.  Lahijanian M, Maly MR, Fried D, Kavraki LE, Kress-Gazit H, Vardi MY 2016. Iterative temporal planning in uncertain environments with partial satisfaction guarantees. IEEE Trans. Robot. 32:583–99
     [Google Scholar]
  83. 83.  Bhatia A, Kavraki LE, Vardi MY 2010. Sampling-based motion planning with temporal goals. 2010 IEEE International Conference on Robotics and Automation (ICRA)2689–96 New York: IEEE
     [Google Scholar]
  84. 84.  Bhatia A, Maly MR, Kavraki LE, Vardi MY 2011. Motion planning with complex goals. IEEE Robot. Autom. Mag. 18:55–64
     [Google Scholar]
  85. 85.  Vasile CI, Belta C 2013. Sampling-based temporal logic path planning. 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)4817–22 New York: IEEE
     [Google Scholar]
  86. 86.  McMahon J, Plaku E 2014. Sampling-based tree search with discrete abstractions for motion planning with dynamics and temporal logic. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)3726–33 New York: IEEE
     [Google Scholar]
  87. 87.  He K, Lahijanian M, Kavraki LE, Vardi MY 2015. Towards manipulation planning with temporal logic specifications. 2015 IEEE International Conference on Robotics and Automation (ICRA)346–52 New York: IEEE
     [Google Scholar]
  88. 88.  Lahijanian M, Wasniewski J, Andersson SB, Belta C 2010. Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. 2010 IEEE International Conference on Robotics and Automation (ICRA)3227–32 New York: IEEE
     [Google Scholar]
  89. 89.  Lahijanian M, Andersson S, Belta C 2011. Control of Markov decision processes from PCTL specifications. 2011 American Control Conference311–16 New York: IEEE
     [Google Scholar]
  90. 90.  Cizelj I, Ding XC, Lahijanian M, Pinto A, Belta C 2011. Probabilistically safe vehicle control in a hostile environment. IFAC-PapersOnline 18:11803–8
     [Google Scholar]
  91. 91.  Lahijanian M, Andersson SB, Belta C 2012. Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Trans. Robot. 28:396–409
     [Google Scholar]
  92. 92.  Lahijanian M, Andersson S, Belta C 2009. A probabilistic approach for control of a stochastic system from LTL specifications. Proceedings of the 48th IEEE Conference on Decision and Control (CDC) Held Jointly with the 2009 28th Chinese Control Conference2236–41 New York: IEEE
     [Google Scholar]
  93. 93.  Ding XC, Smith SL, Belta C, Rus D 2011. LTL control in uncertain environments with probabilistic satisfaction guarantees. IFAC-PapersOnline 18:3515–20
     [Google Scholar]
  94. 94.  Svorenova M, Cerna I, Belta C 2013. Optimal control of MDPs with temporal logic constraints. 2013 IEEE 52nd Annual Conference on Decision and Control (CDC)3938–43 New York: IEEE
     [Google Scholar]
  95. 95.  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]
  96. 96.  Fu J, Topcu U 2016. Synthesis of shared autonomy policies with temporal logic specifications. IEEE Trans. Autom. Sci. Eng. 13:7–17
     [Google Scholar]
  97. 97.  Wang J, Ding XXC, Lahijanian M, Paschalidis IIC, Belta CCA et al. 2012. Temporal logic motion control using actor-critic methods. 2012 IEEE International Conference on Robotics and Automation (ICRA)4687–92 New York: IEEE
     [Google Scholar]
  98. 98.  Fu J, Topcu U 2014. Probably approximately correct MDP learning and control with temporal logic constraints. Robotics: Science and Systems X D Fox, LE Kavraki, H Kurniawati, chap. 39 N.p.: Robot. Sci. Syst. Found.
     [Google Scholar]
  99. 99.  Brázdil T, Chatterjee K, Chmelík M, Forejt V, Křetínský J et al. 2014. Verification of Markov decision processes using learning algorithms. Automated Technology for Verification and Analysis F Cassez, JF Raskin 98–114 Berlin: Springer
     [Google Scholar]
  100. 100.  Sadigh D, Kim ES, Coogan S, Sastry S, Seshia SA 2014. A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. IEEE 53rd Annual Conference on Decision and Control (CDC)1091–96 New York: IEEE
     [Google Scholar]
  101. 101.  Wang J, Ding XXC, Lahijanian M, Paschalidis IIC, Belta CC 2015. Temporal logic motion control using actor-critic methods. Int. J. Robot. Res. 34:1329–44
     [Google Scholar]
  102. 102.  Wolff EM, Topcu U, Murray RM 2012. Robust control of uncertain Markov decision processes with temporal logic specifications. 2012 IEEE 51st Annual Conference on Decision and Control (CDC)3372–79 New York: IEEE
     [Google Scholar]
  103. 103.  Lahijanian M, Andersson SB, Belta C 2015. Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60:2031–45
     [Google Scholar]
  104. 104.  Luna R, Lahijanian M, Moll M, Kavraki L 2015. Asymptotically optimal stochastic motion planning with temporal goals. Algorithmic Foundations of Robotics XI335–52 Berlin: Springer
     [Google Scholar]
  105. 105.  de Alfaro L 1997. Formal verification of probabilistic systems PhD Thesis, Dep. Comput. Sci., Stanford Univ. Stanford, CA:
  106. 106.  Kress-Gazit H, Fainekos GE, Pappas GJ 2009. Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25:1370–81
     [Google Scholar]
  107. 107.  Kress-Gazit H, Wongpiromsarn T, Topcu U 2011. Correct, reactive, high-level robot control. IEEE Robot. Autom. Mag. 18:65–74
     [Google Scholar]
  108. 108.  Wongpiromsarn T, Topcu U, Murray RM 2012. Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57:2817–30
     [Google Scholar]
  109. 109.  Kozen D 1983. Results on the propositional μ-calculus. Theor. Comput. Sci. 27:333–54
     [Google Scholar]
  110. 110.  Ehlers R 2011. Generalized Rabin(1) synthesis with applications to robust system synthesis. NFM 2011: NASA Formal Methods M Bobaru, K Havelund, GJ Holzmann, R Joshi 101–15 Berlin: Springer
     [Google Scholar]
  111. 111.  Ehlers R, Raman V 2016. Slugs: extensible GR(1) synthesis. CAV 2016: Computer Aided Verification S Chaudhuri, A Farzan 333–39 Berlin: Springer
     [Google Scholar]
  112. 112.  Pnueli A, Sa'ar Y, Zuck LD 2010. JTLV: a framework for developing verification algorithms. CAV 2010: Computer Aided Verification T Touili, B Cook, P Jackson 171–74 Berlin: Springer
     [Google Scholar]
  113. 113.  Finucane C, Jing G, Kress-Gazit H 2010. LTLMoP: experimenting with language, temporal logic and robot control. 2010 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)1988–93 New York: IEEE
     [Google Scholar]
  114. 114.  Filippidis I, Dathathri S, Livingston SC, Ozay N, Murray RM 2016. Control design for hybrid systems with TuLiP: the Temporal Logic Planning toolbox. 2016 IEEE Conference on Control Applications (CCA)1030–41 New York: IEEE
     [Google Scholar]
  115. 115.  Karaman S, Sanfelice RG, Frazzoli E 2008. Optimal control of mixed logical dynamical systems with linear temporal logic specifications. 47th IEEE Conference on Decision and Control (CDC)2117–22 New York: IEEE
     [Google Scholar]
  116. 116.  Kwon Y, Agha G 2008. LTLC: linear temporal logic for control. HSCC '08: Proceedings of the 11th International Workshop on Hybrid Systems: Computation and Control316–29 Berlin: Springer
     [Google Scholar]
  117. 117.  Wolff EM, Topcu U, Murray RM 2014. Optimization-based trajectory generation with linear temporal logic specifications. 2014 IEEE International Conference on Robotics and Automation (ICRA)5319–25 New York: IEEE
     [Google Scholar]
  118. 118.  Lindemann L, Dimarogonas DV 2017. Robust motion planning employing signal temporal logic. 2017 American Control Conference (ACC)2950–55 New York: IEEE
     [Google Scholar]
  119. 119.  Gol EA, Lazar M 2013. Temporal logic model predictive control for discrete-time systems. HSCC'13: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control343–52 New York: ACM
     [Google Scholar]
  120. 120.  Raman V, Donzé A, Sadigh D, Murray RM, Seshia SA 2015. Reactive synthesis from signal temporal logic specifications. HSCC '15: Proceedings of the 18th International Conference on Hybrid Systems Computation and Control239–48 New York: ACM
     [Google Scholar]
  121. 121.  Sadigh D, Kapoor A 2016. Safe control under uncertainty with probabilistic signal temporal logic. Robotics: Science and Systems XII D Hu, N Amato, S Berman, S Jacobs, chap. 17 N.p.: Robot. Sci. Syst. Found.
     [Google Scholar]
  122. 122.  Jha S, Raman V 2016. Automated synthesis of safe autonomous vehicle control under perception uncertainty. NFM 2016: NASA Formal Methods S Rayadurgam, O Tkachuk 117–32 Cham, Switz.: Springer
     [Google Scholar]
/content/journals/10.1146/annurev-control-060117-104838
Loading
Synthesis for Robots: Guarantees and Feedback for Robot Behavior
Annual Review of Control, Robotics, and Autonomous Systems 1, 211 (2018); https://doi.org/10.1146/annurev-control-060117-104838
/content/journals/10.1146/annurev-control-060117-104838
/content/journals/10.1146/annurev-control-060117-104838
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