CoChat
Sign Up
Cited by 17Formal Methods in VerificationSafety Systems Engineering in AutonomyLogic, programming, and type systems

The DOI matches its Crossref record; 11 of the 11 references it cites were found in a registry or an index.

Formal Methods for Autonomous Systems

Open access
Wongpiromsarn, Tichakorn, Ghasemi, Mahsa, Cubuktepe, Murat, Bakirtzis, Georgios, Carr, Steven, Karabag, Mustafa O., Neary, Cyrus, Gohari, Parham, Topcu, Ufuk·2023·Foundations and Trends® in Systems and Control
DOI 10.1561/2600000029
Open this paper in CoChat — free accountOpen PDF

Abstract

Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1561/2600000029

Cites

11 of 11 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Ensuring the safety of agentic systems with formal guarantees is complicated by the need to model a system's interactions in an arbitrarily complex environment that might not be formalizable.

    “Ensuring the safety of agentic systems with formal guarantees is further complicated by the need to model a system's interactions in an arbitrarily complex environment that might not be formalizable (Seshia et al., 2022;Wongpiromsarn et al., 2023;Dalrymple et al., 2024).”

    From Open Problems in Mechanistic Interpretability (2025) · cites this paper as Wongpiromsarn et al., 2023

    Section 1.3, “What Makes It Hard?” (page not specified), says uncertain, unstructured, changing environments make verification and synthesis more complex. The Introduction (page not specified) says formal guarantees depend on a well-defined model and notes the challenge of modeling open-world environments. Our copy does not establish that such environments may be impossible to formalize, or describe their complexity as arbitrary. (LLM, conf=0.83)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 277

  1. Abadi, 1994, An Old-Fashioned Recipe for Real Time, ACM Transactions on Programming Languages and Systems, 16, 1543, 10.1145/186025.186058 · DOI
  2. Agha, 2018, A survey of statistical model checking, ACM Transactions on Modeling and Computer Simulation (TOMACS), 28, 1, 10.1145/3158668 · DOI
  3. Ahmadi, 2018, Verification of Uncertain POMDPs Using Barrier Certificates, 115
  4. Ahmed, 2017, Sampling Based Approaches for Minimizing Regret in Uncertain Markov Decision Pro cesses (MDPs), J. Artif. Intell. Res, 59, 229, 10.1613/jair.5242 · DOI
  5. Akash, 2020, Human Trust-based Feedback Control: Dynamically Varying Automation Transparency to Optimize Human-Machine Interactions, IEEE Control Systems Magazine, 40, 98, 10.1109/MCS.2020.3019151 · DOI
  6. Almagor, 2016, Formally Reasoning About Quality, Journal of the ACM, 63, 24:1, 10.1145/2875421 · DOI
  7. Alur, 2008, Ranking Automata and Games for Prioritized Requirements, 10.1007/978-3-540-70545-1_23 · DOI
  8. Alur, 2004, Deterministic generators and games for LTL fragments, ACM Transactions on Computational Logic, 5, 1, 10.1145/963927.963928 · DOI
  9. Amato, 2010, Optimizing Fixed-Size Stochastic Controllers for POMDPs and Decentralized POMDPs, AAMAS, 21, 293
  10. Anderson, 2020, Surprise! 2020 Is Not the Year for Self-Driving Cars
  11. Arming, 2018, Parameter-Independent Strategies for pMDPs via POMDPs, 53
  12. Asarin, 1998, Controller synthesis for timed automata, 469
  13. Bacci, 2019, Model Checking Constrained Markov Reward Models with Uncertainties, 37
  14. Badings, 2022, Scenario-Based Verification of Uncertain Parametric MDPs, International Journal on Software Tools for Technology Transfer, 24, 803, 10.1007/s10009-022-00673-z · DOI
  15. Bai, 2014, Integrated perception and planning in the continuous space: A POMDP approach, The International Journal of Robotics Research, 33, 1288, 10.1177/0278364914528255 · DOI
  16. Baier, 2012, Probabilistic ω-auto-mata, Journal of the ACM, 59, 1:1, 10.1145/2108242.2108243 · DOI
  17. Baier, 2020, Parametric Markov Chains: PCTL Complexity and Fraction-Free Gaussian Elimination, Inf. Comput, 272, 104504, 10.1016/j.ic.2019.104504 · DOI
  18. Baier, 2008, Principles of Model Checking
  19. Bakirtzis, 2022, An Ontological Metamodel for Cyber-Physical System Safety, Security, and Resilience Co engineering, 10.1007/s10270-021-00892-z · DOI
  20. Bakirtzis, 2022, Dynamic Certification for Autonomous Systems, 10.48550/ARXIV.2203.10950 · DOI
  21. Bakker, 2001, Reinforcement Learning with Long Short-Term Memory, 1475
  22. 2018, Basic Theory of Driving: The Official Handbook
  23. Baum, 1987, Supervised Learning of Probability Distributions by Neural Networks, 52
  24. Benenson, 2006, Integrating perception and planning for autonomous navigation of urban vehicles, 98
  25. Bérard, 2015, Quantifying opacity, Mathematical Structures in Computer Science, 25, 361, 10.1017/S0960129513000637 · DOI
  26. Bertsekas, 2019, Reinforcement learning and optimal control
  27. Biere, 2009, Handbook of satisfiability
  28. Bloem, 2009, Better Quality in Synthesis through Quantitative Objectives, 140
  29. Bloem, 2015, Shield Synthesis: Runtime Enforcement for Reactive Systems, 10.1007/978-3-662-46681-0\_51 · DOI
  30. Boff, 1988, Engineering data compendium: Human perception and performance
  31. Borkar, 2014, Risk-Constrained Markov Decision Processes, IEEE Transactions on Automatic Control, 59, 25742579, 10.1109/TAC.2014.2309262 · DOI
  32. Bortolussi, 2018, Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models, 396
  33. Bouma, 1994, Towards a Pan-European Telecommunication Servcie Infrastructure, 393
  34. Bouton, 2020, Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes, 10061
  35. Boyd, 2004, Convex Optimization, 10.1017/CBO9780511804441 · DOI · Paper page
  36. Bozkurt, 2020, Control synthesis from linear temporal logic specifications using modelfree reinforcement learning, 10349
  37. Büchi, 1990, The collected works of J. Richard Büchi, 425, 10.1007/978-1-4613-8928-6_23 · DOI
  38. Burdick, 2007, Sensing, Navigation and Reasoning Technologies for the DARPA Urban Challenge, 10.21236/ADA475519 · DOI
  39. Burns, 2007, Sampling-Based Motion Planning with Sensing Uncertainty, 3313
  40. Calafiore, 2006, The Scenario Approach to Robust Control Design, IEEE Trans. Automat. Contr, 51, 742, 10.1109/TAC.2006.875041 · DOI
  41. Calinescu, 2016, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 540
  42. Camacho, 2019, LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning, 6065
  43. Campbell, 2010, Autonomous driving in urban environments: approaches, lessons and challenges, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 368, 4649, 10.1098/rsta.2010.0110 · DOI
  44. Campi, 2011, A Sampling-and-Discarding Approach to Chance-Constrained Optimization: Feasibility and Op-timality, Journal of Optimization Theory and Applications, 148, 257, 10.1007/s10957-010-9754-6 · DOI
  45. Campi, 2008, The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs, SIAM Journal on Optimization, 19, 1211, 10.1137/07069821X · DOI
  46. Campi, 2018, A General Scenario Theory for Nonconvex Optimization and Decision Making, IEEE Trans. Automat. Contr, 63, 4067, 10.1109/TAC.2018.2808446 · DOI
  47. Carr, 2020, Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints, 4121
  48. Carr, 2021, Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes, J. Artif. Intell. Res, 72, 819, 10.1613/jair.1.12963 · DOI
  49. Carr, 2019, Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks, 5532
  50. Cassandra, 1997, Incremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes, 54
  51. Castro, 2013, Incremental sampling-based algorithm for minimum-violation motion planning, 3217
  52. Censi, 2019, Liability, Ethics, and Culture-Aware Behavior Specification using Rulebooks, 8536, 10.1109/ICRA.2019.8794364 · DOI
  53. Cerrito, 1998, Using Linear Temporal Logic to Model and Solve Planning Problems, 141
  54. Chamie, 2018, Robust Action Selection in Partially Observable Markov Decision Processes with Model Uncertainty, 5586
  55. Chao, 2010, Autopilots for small unmanned aerial vehicles: a survey, International Journal of Control, Automation and Systems, 8, 36, 10.1007/s12555-010-0105-z · DOI
  56. Chatterjee, 2016, Optimal Cost Almost-sure Reachability in POMDPs, Artificial Intelligence, 234, 26, 10.1016/j.artint.2016.01.007 · DOI
  57. Chen, 2012, Supervisory control of multiple robots: Effects of imperfect automation and individual differences, Human Factors, 54, 157, 10.1177/0018720811435843 · DOI
  58. Chen, 2020, Trust-Aware Decision Making for Human-Robot Collaboration: Model Learning and Planning, ACM Transactions on Human-Robot Interaction (THRI), 9, 1, 10.1145/3359616 · DOI
  59. Chen, 2013, On the Complexity of Model Checking Interval-Valued Discrete Time Markov Chains, Information Processing Letters, 113, 210, 10.1016/j.ipl.2013.01.004 · DOI
  60. Chen, 2013, Optimality Conditions and a Smoothing Trust Region Newton Method for Non-Lipschitz Optimization, SIAM Journal on Optimization, 23, 1528, 10.1137/120871390 · DOI
  61. Cimatti, 2002, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, 359
  62. Cimatti, 2008, Diagnostic Information for Realizability, 10.1007/978-3-540-78163-9_9 · DOI
  63. Cimatti, 2007, Boolean Abstraction for Temporal Logic Satisfiability, 532
  64. Clarke, 1986, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), 8, 244, 10.1145/5397.5399 · DOI
  65. Conner, 2007, Valet parking without a valet, 572, 10.1109/IROS.2007.4399374 · DOI
  66. Cooke, 2009, Unmanned aerial vehicles
  67. Cubuktepe, 2020, IEEE Transactions on Automatic Control, Accepted
  68. Cubuktepe, 2017, Sequential Convex Programming for the Efficient Verification of Parametric MDPs, 133
  69. Cubuktepe, 2018, Synthesis in pMDPs: A Tale of 1001 Parameters, 160
  70. Cubuktepe, 2020, Scenario-Based Verification of Uncertain MDPs, 287
  71. Cubuktepe, 2020, Scenario-Based Verification of Uncertain MDPs, 287
  72. Cubuktepe, 2021, IEEE Transactions on Automatic Control, Under Revision
  73. Cubuktepe, 2021, Robust Finite-State Controllers for Uncertain POMDPs, 11792
  74. Daws, 2004, Symbolic and Parametric Model Checking of Discrete-Time Markov Chains, 280
  75. Degrave, 2022, Magnetic control of tokamak plasmas through deep reinforcement learning, Nature, 602, 414, 10.1038/s41586-021-04301-9 · DOI · Paper page
  76. Dehnert, 2015, PROPhESY: A PRObabilistic ParamEter SYnthesis Tool, 214
  77. Dehnert, 2017, A Storm is Coming: A Modern Probabilistic Model Checker, 592
  78. Dimitrova, 2018, Maximum Realizability for Linear Temporal Logic Specifications, 458475
  79. Ding, 2011, LTL control in uncertain environments with probabilistic satisfaction guarantees, IFAC Proceedings Volumes, 44, 3515, 10.3182/20110828-6-IT-1002.02287 · DOI
  80. Djeumou, 2021, Task-Guided Inverse Reinforcement Learning under Partial Information
  81. Donmez, 2010, Modeling Workload Impact in Multiple Unmanned Vehicle Supervisory Control, IEEE Trans. Syst. Man Cybern. Part A, 40, 1180, 10.1109/TSMCA.2010.2046731 · DOI
  82. Donzé, 2010, Formal Modeling and Analysis of Timed Systems, 92, 10.1007/978-3-642-15297-9_9 · DOI
  83. Dosovitskiy, 2017, CARLA: An Open Urban Driving Simulator, 1
  84. DuToit, 2008, Situational Reasoning for Road Driving in an Urban Environment
  85. Ehlers, 2014, Low-Effort Specification Debugging and Analysis, 117
  86. Emerson, 1990, Handbook of theoretical computer science (vol. B): formal models and semantics, 995
  87. Eysenbach, 2021, Robust predictable control, 34
  88. Faella, 2009, Admissible Strategies in Infinite Games over Graphs, 307, 10.1007/978-3-64203816-7\_27 · DOI
  89. Farokhi, 2017, Fisher information as a measure of privacy: Preserving privacy of households with smart meters using batteries, IEEE Transactions on Smart Grid, 9, 4726, 10.1109/TSG.2017.2667702 · DOI
  90. Faymonville, 2017, Encodings of Bounded Synthesis, 354
  91. Feng, 2018, Counterexamples for robotic planning explained in structured language, 7292
  92. Feng, 2016, Human-interpretable diagnostic information for robotic planning systems, 1673
  93. Feng, 2015, Controller synthesis for autonomous systems interacting with human operators, 70
  94. Feng, 2016, Synthesis of Human-in-the-Loop Control Protocols for Autonomous Systems, IEEE Trans Autom. Sci. Eng, 13, 450, 10.1109/TASE.2016.2530623 · DOI
  95. Filieri, 2016, Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time, IEEE Trans. Software Eng, 42, 75, 10.1109/TSE.2015.2421318 · DOI
  96. 2017, Final Theory of Driving: The Official Handbook
  97. Finkbeiner, 2013, Bounded synthesis, International Journal on Software Tools for Technology Transfer, 15, 10.1007/s10009-012-0228-z · DOI
  98. Forejt, 2011, Quantitative multi-objective verification for probabilistic systems, 112
  99. Franceschetti, 2014, Information and Control in Networks, 3, 10.1007/978-3-319-02150-8_1 · DOI
  100. Frey, 2017, Constrained Spacecraft Relative Motion Planning Exploiting Periodic Natural Motion Trajectories and Invariance, Journal of Guidance, Control, and Dynamics, 40, 3100, 10.2514/1.G002914 · DOI
  101. Fu, 2016, Optimal temporal logic planning in probabilistic semantic maps, 3690
  102. Fu, 2015, Integrating active sensing into reactive synthesis with temporal logic constraints under partial observations, 2408
  103. Fu, 2016, Synthesis of joint control and active sensing strategies under temporal logic constraints, IEEE Transactions on Automatic Control, 61, 3464, 10.1109/TAC.2016.2518639 · DOI
  104. Gabbay, 1995, Handbook of Logic in Artificial Intelligence and Logic Programming (Vol. 4): Epistemic and Temporal Reasoning, 10.1093/oso/9780198537915.001.0001 · DOI
  105. Galton, 1987, Temporal Logics and Their Applications
  106. Ghasemi, 2020, Task-oriented active perception and planning in environments with partially known semantics, 3484
  107. Ghasemi, 2019, Online Active Perception for Partially Observable Markov Decision Processes with Limited Budget, 6169
  108. Ghasemi, 2019, Perception-Aware Point-Based Value Iteration for Partially Observable Markov Decision Processes, 2371
  109. Girard, 2009, Hierarchical control system design using approximate simulation, Automatica, 45, 566, 10.1016/j.automatica.2008.09.016 · DOI
  110. Givan, 2000, Bounded-Parameter Markov Decision Processes, Artificial Intelligence, 122, 71, 10.1016/S0004-3702(00)00047-3 · DOI
  111. Gluck, 2002, Using SPIN model checking for flight software verification, 1-105
  112. Gohari, 2020, Privacy-preserving policy synthesis in Markov decision processes, 6266
  113. Goodfellow, 2016, Deep Learning. Adaptive computation and machine learning
  114. Goodfellow, 2015, Qualitatively characterizing neural network optimization problems
  115. Goodwin, 2004, Constrained Control and Estimation: An Optimisation Approach
  116. Gradel, 2002, Automata, logics, and infinite games: a guide to current research, 10.1007/3-540-36387-4 · DOI
  117. Gunter, 2002, Temporal Debugging for Concurrent Systems, 431, 10.1007/3-540-46002-0_30 · DOI
  118. Guo, 2013, Revising motion planning under linear temporal logic specifications in partially known workspaces, 5025
  119. Hahn, 2017, Multi-Objective Robust Strategy Synthesis for Interval Markov Decision Processes, 207
  120. Hahn, 2010, Probabilistic reachability for parametric Markov models, Software Tools for Technology Transfer, 13, 3, 10.1007/s10009-010-0146-x · DOI
  121. Hahn, 2014, iscasMc: A Web-Based Probabilistic Model Checker, 312
  122. Hahn, 2019, Omega-regular objectives in model-free reinforcement learning, 395
  123. Han, 2009, Counterexample generation in probabilistic model checking, IEEE Transactions on Software Engineering, 35, 241, 10.1109/TSE.2009.5 · DOI
  124. Harel, 2022, Creating a Foundation for Next-Generation Autonomous Systems, IEEE Design & Test, 39, 49, 10.1109/MDAT.2021.3069959 · DOI
  125. Hasanbeig, 2019, Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees, 5338, 10.1109/CDC40024.2019.9028919 · DOI
  126. Hasanbeig, 2019, Logically-Constrained Neural Fitted Q-Iteration, 2012
  127. Hausknecht, 2015, Deep Recurrent Q-Learning for Partially Observable MDPs, 29
  128. Havelund, 2001, Formal analysis of a space-craft controller using SPIN, IEEE Transactions on Software Engineering, 27, 749, 10.1109/32.940728 · DOI
  129. Hayes, 2017, Improving Robot Controller Transparency Through Autonomous Policy Explanation, 303
  130. Heess, 2015, Learning continuous control policies by stochastic value gradients, 2944
  131. Ho, 2018, Fast Bellman Updates for Robust MDPs
  132. Hobbs, 2020, A Taxonomy for Aerospace Collision Avoidance with Implications for Automation in Space Traffic Management, 0877
  133. Hoeffding, 1994, The collected works of Wassily Hoeffding, 409, 10.1007/978-1-4612-0865-5_26 · DOI
  134. Holzmann, 1994, The Theory and Practice of A Formal Method: NewCoRe, 35
  135. Holzmann, 2004, The Spin Model Checker
  136. Holzmann, 2014, Mars Code, Commun. ACM, 57, 64, 10.1145/2560217.2560218 · DOI
  137. Hosseini, 2014, A Coordinated MDP Approach to Multi-Agent Planning for Resource Allocation, with Applications to Healthcare
  138. Humphrey, 2013, Model Checking Human-Automation UAV Mission Plans, 10.2514/6.2013-5183 · DOI
  139. Humphrey, 2014, Formal specification and synthesis of mission plans for unmanned aerial vehicles
  140. Humphrey, 2016, Synthesis of Admissible Shields, 134, 10.1007/978-3-319-49052-6\_9 · DOI
  141. Huth, 2004, Logic in Computer Science: Modelling and Reasoning about Systems, 10.1017/CBO9780511810275 · DOI
  142. Icarte, 2018, Using reward machines for high-level task specification and decomposition in reinforcement learning, 2107
  143. Icarte, 2019, Learning reward machines for partially observable reinforcement learning, 15523
  144. Itoh, 2007, Partially Observable Markov Decision Processes with Imprecise Parameters, Artificial Intelligence, 171, 453, 10.1016/j.artint.2007.03.004 · DOI
  145. Jadbabaie, 2000, Nonlinear Receding Horizon Control: A Control Lyapunov Function Approach
  146. Jagadeesan, 1996, A formal approach to reactive systems software: a telecommunications application in ESTEREL, Formal Methods in System Design, 8, 123, 10.1007/BF00122418 · DOI
  147. Jansen, 2020, Safe Reinforcement Learning Using Probabilistic Shields
  148. Jiang, 2001, IEEE Transactions on Automatic Control, 128
  149. Jones, 2013, Distribution temporal logic: Combining correctness with quality of estimation, 4719
  150. Jothimurugan, 2021, Compositional reinforcement learning from logical specifications, 34
  151. Julian, 2019, Deep Neural Network Compression for Aircraft Collision Avoidance Systems, Journal of Guidance, Control, and Dynamics, 42, 598, 10.2514/1.G003724 · DOI
  152. Junges, 2020, PhD thesis
  153. Junges, 2019, Parameter Synthesis for Markov Models, CoRR, abs/1903.07993 · arXiv
  154. Junges, 2018, Finite-state controllers of POMDPs via parameter synthesis, 519
  155. Karabag, 2022, Planning Not to |Talk: Multiagent Systems that are Robust to Communication Loss
  156. Karabag, 2019, Least inferable policies for Markov decision processes, 1224
  157. Karabag, 2021, Deception in Supervisory Control
  158. Karaman, 2009, Sampling-based Motion Planning with Deterministic μ-Calculus Specifications, 10.1109/CDC.2009.5400278 · DOI
  159. Kearns, 1999, Approximate Planning in Large POMDPs via Reusable Trajectories, 1001
  160. Ketkar, 2017, Deep learning with Python, 97, 10.1007/978-1-4842-2766-4_7 · DOI
  161. Kim, 2015, On the minimal revision problem of specification automata, International Journal of Robotics Research, 34, 10.1177/0278364915587034 · DOI
  162. Kim, 2007, Mission Design and Trajectory Analysis for Inspection of a Host Spacecraft by a Microsatellite, 1
  163. Klein, 2007, Implementation and Application of Automata, 51, 10.1007/978-3-540-76336-9_7 · DOI
  164. Kloetzer, 2008, A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications, IEEE Transactions on Automatic Control, 53, 287, 10.1109/TAC.2007.914952 · DOI
  165. Kloetzer, 2008, Dealing with Nondeterminism in Symbolic Control, 287
  166. Könighofer, 2017, Shield synthesis, 10.1007/s10703-017-0276-9 · DOI
  167. Koul, 2019, Learning Finite State Representations of Recurrent Policy Networks
  168. Kozen, 1983, Results on the propositional μ-calculus, Theoretical Computer Science, 27, 333, 10.1016/0304-3975(82)90125-6 · DOI
  169. Kress-Gazit, 2007, Where’s Waldo? Sensor-Based Temporal Logic Motion Planning, 3116, 10.1109/ROBOT.2007.363946 · DOI
  170. Kress-Gazit, 2009, Temporal-logic-based reactive mission and motion planning, IEEE transactions on robotics, 25, 1370, 10.1109/TRO.2009.2030225 · DOI
  171. Kress-Gazit, 2011, Correct, Reactive, High-Level Robot Control, IEEE Robotics Automation Magazine, 18, 65, 10.1109/MRA.2011.942116 · DOI
  172. Kupferman, 2001, Model checking of safety properties, Formal Methods in System Design, 19, 291, 10.1023/A:1011254632723 · DOI · Paper page
  173. Kupferman, 2005, Safraless Decision Procedures, 531
  174. Kwiatkowska, 2011, PRISM 4.0: Verification of Probabilistic Real-Time Systems, 585
  175. Lahijanian, 2015, This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction
  176. Lahijanian, 2016, Specification revision for Markov decision processes with optimal trade-off, 7411
  177. Lahijanian, 2016, Iterative temporal planning in uncertain environments with partial satisfaction guarantees, IEEE Transactions on Robotics, 32, 583, 10.1109/TRO.2016.2544339 · DOI
  178. Lamport, 2002, Specifying systems: The TLA + language and tools for hardware and software engineers
  179. Lamport, 1983, Specifying concurrent program modules, ACM Transactions on Programming Languages and Systems, 5, 190222, 10.1145/69624.357207 · DOI
  180. Lamport, 1994, The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, 16, 872, 10.1145/177492.177726 · DOI
  181. Lanotte, 2007, Parametric Probabilistic Transition Systems for System Design and Analysis, Formal Aspects Comput, 19, 93, 10.1007/s00165-006-0015-2 · DOI
  182. Lecarpentier, 2019, Non-Stationary Markov Decision Processes, a Worst-Case Approach using Model-Based Reinforcement Learning, Extended Version
  183. Leike, 2017, AI Safety Gridworlds, CoRR, abs/1711.09883 · arXiv
  184. Leucker, 2009, A brief account of runtime verification, J. Log. Algebraic Methods Program, 78, 293, 10.1016/j.jlap.2008.08.004 · DOI
  185. Lignos, 2015, Provably correct reactive control from natural language, Autonomous Robots, 38, 89, 10.1007/s10514-014-9418-8 · DOI
  186. Lin, 1993, Analysis and synthesis of discrete event systems using temporal logic, Control Theory and Advanced Technologies, 9, 341
  187. Liu, 2018, Reinforcement Learning for Robot Navigation in Nondeterministic Environments, 615
  188. Livingston, 2012, Backtracking temporal logic synthesis for uncertain environments, 5163
  189. Llerena, 2018, Verifying the Long-run Behavior of Probabilistic System Models in the Presence of Uncertainty, 587
  190. Madani, 1999, On the Undecidability of Probabilistic Planning and Infinite-Horizon Partially Observable Markov Decision Problems, 541
  191. Manna, 1992, The Temporal Logic of Reactive and Concurrent Systems, 10.1007/978-1-4612-0931-7 · DOI
  192. Mao, 2018, Successive Con-vexification: A Superlinearly Convergent Algorithm for Non-convex Optimal Control Problems
  193. Mason, 2017, Assured Reinforcement Learning with Formally Verified Abstract Policies, 10.5220/0006156001050117 · DOI
  194. Mayne, 2000, Constrained model predictive control: Stability and optimality, Automatica, 36, 789, 10.1016/S0005-1098(99)00214-9 · DOI · Paper page
  195. Mazala, 2001, Infinite Games, 23, 10.1007/3-540-36387-4\_2 · DOI
  196. McMillan, 1993, Symbolic Model Checking, 10.1007/978-1-4615-3190-6 · DOI
  197. Mehdipour, 2019, Average-based Robustness for Continuous-Time Signal Temporal Logic, 5312, 10.1109/CDC40024.2019.9029989 · DOI
  198. Meuleau, 1999, Solving POMDPs by Searching the Space of Finite Policies, 417
  199. Michaud, 2015, Practical Stutter-Invariance Checks for ω-Regular Languages, 84
  200. Montana, 2017, Sampling-based reactive motion planning with temporal logic constraints and imperfect state information, 134

200 of 277 shown

Cited by

Sorted by citations

Metadata

Authors
Wongpiromsarn, T., Ghasemi, M., Cubuktepe, M., Bakirtzis, G., Carr, S., Karabag, M. O., Neary, C., Gohari, P., & Topcu, U.
Affiliations
  • Iowa State University (US)
  • Purdue University West Lafayette (US)
  • The University of Texas at Austin (US)
ORCID
Venue
Foundations and Trends® in Systems and Control
Publisher
Emerald
Published
2023-09-21
Volume
10
Issue
3-4
Pages
180-407
ISSN
  • 2325-6818 (ISSN-L)
  • 2325-6826
DOI
10.1561/2600000029
OpenAlex
W4386927538
Cited by
17
References
11
Citations by year
2026: 8 · 2025: 8 · 2024: 1
FWCI
3.10
Type
journal article
Language
en
Open access
Locations
  • Foundations and Trends® in Systems and Control (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
  • National Science Foundation (1652113, 2211141, 2141153, 1836900, 1646522)
  • National Aeronautics and Space Administration (80NSSC21M0071)
  • Nuclear Safety and Security Commission
  • Air Force Office of Scientific Research (#FA9550-19-1-0169, FA9550-, FA9550-19-1-0005)
  • Air Force Research Laboratory (FA9550-19-1-0169, FA9550)
Topics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Engineering › Safety, Risk, Reliability and Quality › Safety Systems Engineering in Autonomy
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
Keywords
formal methods, autonomous systems, reactive synthesis, closed systems, learning under uncertainty, monitoring, mitigation, reinforcement learning, privacy, explainability, safety-critical systems, certification

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review