{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T18:55:05Z","timestamp":1774983305190,"version":"3.50.1"},"reference-count":289,"publisher":"Emerald","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,21]]},"abstract":"<jats:p>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.<\/jats:p>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1561\/2600000029","type":"journal-article","created":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T09:43:59Z","timestamp":1695289439000},"page":"180-407","source":"Crossref","is-referenced-by-count":4,"title":["Formal Methods for Autonomous Systems"],"prefix":"10.1561","volume":"10","author":[{"given":"Tichakorn","family":"Wongpiromsarn","sequence":"first","affiliation":[{"name":"Iowa State University,","place":["USA"]}]},{"given":"Mahsa","family":"Ghasemi","sequence":"additional","affiliation":[{"name":"Purdue University,","place":["USA"]}]},{"given":"Murat","family":"Cubuktepe","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Georgios","family":"Bakirtzis","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Steven","family":"Carr","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Mustafa O.","family":"Karabag","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Cyrus","family":"Neary","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Parham","family":"Gohari","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin,","place":["USA"]}]}],"member":"140","published-online":{"date-parts":[[2023,9,21]]},"reference":[{"issue":"5","key":"2026033114013287400_ref001","doi-asserted-by":"crossref","first-page":"1543","DOI":"10.1145\/186025.186058","article-title":"An Old-Fashioned Recipe for Real Time","volume":"16","author":"Abadi","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"2026033114013287400_ref002","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158668","article-title":"A survey of statistical model checking","volume":"28","author":"Agha","year":"2018","journal-title":"ACM Transactions on Modeling and Computer Simulation (TOMACS)"},{"key":"2026033114013287400_ref003","first-page":"115","volume-title":"Verification of Uncertain POMDPs Using Barrier Certificates","author":"Ahmadi","year":"2018"},{"key":"2026033114013287400_ref004","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1613\/jair.5242","article-title":"Sampling Based Approaches for Minimizing Regret in Uncertain Markov Decision Pro cesses (MDPs)","volume":"59","author":"Ahmed","year":"2017","journal-title":"J. Artif. Intell. Res"},{"issue":"6","key":"2026033114013287400_ref005","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1109\/MCS.2020.3019151","article-title":"Human Trust-based Feedback Control: Dynamically Varying Automation Transparency to Optimize Human-Machine Interactions","volume":"40","author":"Akash","year":"2020","journal-title":"IEEE Control Systems Magazine"},{"issue":"3","key":"2026033114013287400_ref006","doi-asserted-by":"crossref","first-page":"24:1","DOI":"10.1145\/2875421","article-title":"Formally Reasoning About Quality","volume":"63","author":"Almagor","year":"2016","journal-title":"Journal of the ACM"},{"key":"2026033114013287400_ref007","doi-asserted-by":"crossref","DOI":"10.1609\/aaai.v32i1.11797","volume-title":"Safe Reinforcement Learning via Shielding","author":"Alshiekh","year":"2018"},{"key":"2026033114013287400_ref008","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-70545-1_23","volume-title":"Ranking Automata and Games for Prioritized Requirements","author":"Alur","year":"2008"},{"issue":"1","key":"2026033114013287400_ref009","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/963927.963928","article-title":"Deterministic generators and games for LTL fragments","volume":"5","author":"Alur","year":"2004","journal-title":"ACM Transactions on Computational Logic"},{"issue":"3","key":"2026033114013287400_ref010","first-page":"293","article-title":"Optimizing Fixed-Size Stochastic Controllers for POMDPs and Decentralized POMDPs","volume":"21","author":"Amato","year":"2010","journal-title":"AAMAS"},{"key":"2026033114013287400_ref011","volume-title":"Surprise! 2020 Is Not the Year for Self-Driving Cars","author":"Anderson","year":"2020"},{"key":"2026033114013287400_ref012","first-page":"53","volume-title":"Parameter-Independent Strategies for pMDPs via POMDPs","author":"Arming","year":"2018"},{"key":"2026033114013287400_ref013","first-page":"469","volume-title":"Controller synthesis for timed automata","author":"Asarin","year":"1998"},{"key":"2026033114013287400_ref014","first-page":"37","volume-title":"Model Checking Constrained Markov Reward Models with Uncertainties","author":"Bacci","year":"2019"},{"issue":"5","key":"2026033114013287400_ref015","doi-asserted-by":"crossref","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","article-title":"Scenario-Based Verification of Uncertain Parametric MDPs","volume":"24","author":"Badings","year":"2022","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"9","key":"2026033114013287400_ref016","doi-asserted-by":"crossref","first-page":"1288","DOI":"10.1177\/0278364914528255","article-title":"Integrated perception and planning in the continuous space: A POMDP approach","volume":"33","author":"Bai","year":"2014","journal-title":"The International Journal of Robotics Research"},{"issue":"1","key":"2026033114013287400_ref017","doi-asserted-by":"crossref","first-page":"1:1","DOI":"10.1145\/2108242.2108243","article-title":"Probabilistic \u03c9-auto-mata","volume":"59","author":"Baier","year":"2012","journal-title":"Journal of the ACM"},{"key":"2026033114013287400_ref018","doi-asserted-by":"crossref","first-page":"104504","DOI":"10.1016\/j.ic.2019.104504","article-title":"Parametric Markov Chains: PCTL Complexity and Fraction-Free Gaussian Elimination","volume":"272","author":"Baier","year":"2020","journal-title":"Inf. Comput"},{"key":"2026033114013287400_ref019","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"2026033114013287400_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-021-00892-z","article-title":"An Ontological Metamodel for Cyber-Physical System Safety, Security, and Resilience Co engineering","volume-title":"Software & Systems Modeling","author":"Bakirtzis","year":"2022"},{"key":"2026033114013287400_ref021","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2203.10950","volume-title":"Dynamic Certification for Autonomous Systems","author":"Bakirtzis","year":"2022"},{"key":"2026033114013287400_ref022","first-page":"1475","volume-title":"Reinforcement Learning with Long Short-Term Memory","author":"Bakker","year":"2001"},{"key":"2026033114013287400_ref023","volume-title":"Basic Theory of Driving: The Official Handbook","year":"2018","edition":"10th"},{"key":"2026033114013287400_ref024","volume-title":"Algorithms in Real Algebraic Geometry","author":"Basu","year":"2010"},{"key":"2026033114013287400_ref025","first-page":"52","volume-title":"Supervised Learning of Probability Distributions by Neural Networks","author":"Baum","year":"1987"},{"key":"2026033114013287400_ref026","first-page":"98","volume-title":"Integrating perception and planning for autonomous navigation of urban vehicles","author":"Benenson","year":"2006"},{"issue":"2","key":"2026033114013287400_ref027","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129513000637","article-title":"Quantifying opacity","volume":"25","author":"B\u00e9rard","year":"2015","journal-title":"Mathematical Structures in Computer Science"},{"key":"2026033114013287400_ref028","volume-title":"Reinforcement learning and optimal control","author":"Bertsekas","year":"2019"},{"key":"2026033114013287400_ref029","volume-title":"Handbook of satisfiability","author":"Biere","year":"2009"},{"key":"2026033114013287400_ref030","first-page":"140","volume-title":"Better Quality in Synthesis through Quantitative Objectives","author":"Bloem","year":"2009"},{"key":"2026033114013287400_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0\\_51","volume-title":"Shield Synthesis: Runtime Enforcement for Reactive Systems","author":"Bloem","year":"2015"},{"key":"2026033114013287400_ref032","volume-title":"Engineering data compendium: Human perception and performance","author":"Boff","year":"1988"},{"issue":"9","key":"2026033114013287400_ref033","doi-asserted-by":"crossref","first-page":"25742579","DOI":"10.1109\/TAC.2014.2309262","article-title":"Risk-Constrained Markov Decision Processes","volume":"59","author":"Borkar","year":"2014","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026033114013287400_ref034","first-page":"396","volume-title":"Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models","author":"Bortolussi","year":"2018"},{"key":"2026033114013287400_ref035","first-page":"393","volume-title":"Towards a Pan-European Telecommunication Servcie Infrastructure","author":"Bouma","year":"1994"},{"key":"2026033114013287400_ref036","first-page":"10061","volume-title":"Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes","author":"Bouton","year":"2020"},{"key":"2026033114013287400_ref037","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"Boyd","year":"2004"},{"key":"2026033114013287400_ref038","first-page":"10349","volume-title":"Control synthesis from linear temporal logic specifications using modelfree reinforcement learning","author":"Bozkurt","year":"2020"},{"key":"2026033114013287400_ref039","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-1-4613-8928-6_23","volume-title":"The collected works of J. Richard B\u00fcchi","author":"B\u00fcchi","year":"1990"},{"key":"2026033114013287400_ref040","doi-asserted-by":"crossref","DOI":"10.21236\/ADA475519","article-title":"Sensing, Navigation and Reasoning Technologies for the DARPA Urban Challenge","volume-title":"Tech. rep","author":"Burdick","year":"2007"},{"key":"2026033114013287400_ref041","first-page":"3313","volume-title":"Sampling-Based Motion Planning with Sensing Uncertainty","author":"Burns","year":"2007"},{"issue":"5","key":"2026033114013287400_ref042","doi-asserted-by":"crossref","first-page":"742","DOI":"10.1109\/TAC.2006.875041","article-title":"The Scenario Approach to Robust Control Design","volume":"51","author":"Calafiore","year":"2006","journal-title":"IEEE Trans. Automat. Contr"},{"key":"2026033114013287400_ref043","first-page":"540","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Calinescu","year":"2016"},{"key":"2026033114013287400_ref044","first-page":"6065","volume-title":"LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning","author":"Camacho","year":"2019"},{"issue":"1928","key":"2026033114013287400_ref045","doi-asserted-by":"crossref","first-page":"4649","DOI":"10.1098\/rsta.2010.0110","article-title":"Autonomous driving in urban environments: approaches, lessons and challenges","volume":"368","author":"Campbell","year":"2010","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"issue":"2","key":"2026033114013287400_ref046","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10957-010-9754-6","article-title":"A Sampling-and-Discarding Approach to Chance-Constrained Optimization: Feasibility and Op-timality","volume":"148","author":"Campi","year":"2011","journal-title":"Journal of Optimization Theory and Applications"},{"issue":"3","key":"2026033114013287400_ref047","doi-asserted-by":"crossref","first-page":"1211","DOI":"10.1137\/07069821X","article-title":"The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs","volume":"19","author":"Campi","year":"2008","journal-title":"SIAM Journal on Optimization"},{"issue":"12","key":"2026033114013287400_ref048","doi-asserted-by":"crossref","first-page":"4067","DOI":"10.1109\/TAC.2018.2808446","article-title":"A General Scenario Theory for Nonconvex Optimization and Decision Making","volume":"63","author":"Campi","year":"2018","journal-title":"IEEE Trans. Automat. Contr"},{"key":"2026033114013287400_ref049","first-page":"4121","volume-title":"Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints","author":"Carr","year":"2020"},{"key":"2026033114013287400_ref050","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1613\/jair.1.12963","article-title":"Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes","volume":"72","author":"Carr","year":"2021","journal-title":"J. Artif. Intell. Res"},{"key":"2026033114013287400_ref051","first-page":"5532","volume-title":"Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks","author":"Carr","year":"2019"},{"key":"2026033114013287400_ref052","first-page":"54","volume-title":"Incremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes","author":"Cassandra","year":"1997"},{"key":"2026033114013287400_ref053","first-page":"3217","volume-title":"Incremental sampling-based algorithm for minimum-violation motion planning","author":"Castro","year":"2013"},{"key":"2026033114013287400_ref054","doi-asserted-by":"publisher","first-page":"8536","DOI":"10.1109\/ICRA.2019.8794364","volume-title":"Liability, Ethics, and Culture-Aware Behavior Specification using Rulebooks","author":"Censi","year":"2019"},{"key":"2026033114013287400_ref055","first-page":"141","volume-title":"Using Linear Temporal Logic to Model and Solve Planning Problems","author":"Cerrito","year":"1998"},{"key":"2026033114013287400_ref056","first-page":"5586","volume-title":"Robust Action Selection in Partially Observable Markov Decision Processes with Model Uncertainty","author":"Chamie","year":"2018"},{"issue":"1","key":"2026033114013287400_ref057","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/s12555-010-0105-z","article-title":"Autopilots for small unmanned aerial vehicles: a survey","volume":"8","author":"Chao","year":"2010","journal-title":"International Journal of Control, Automation and Systems"},{"key":"2026033114013287400_ref058","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.artint.2016.01.007","article-title":"Optimal Cost Almost-sure Reachability in POMDPs","volume":"234","author":"Chatterjee","year":"2016","journal-title":"Artificial Intelligence"},{"issue":"2","key":"2026033114013287400_ref059","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1177\/0018720811435843","article-title":"Supervisory control of multiple robots: Effects of imperfect automation and individual differences","volume":"54","author":"Chen","year":"2012","journal-title":"Human Factors"},{"issue":"2","key":"2026033114013287400_ref060","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3359616","article-title":"Trust-Aware Decision Making for Human-Robot Collaboration: Model Learning and Planning","volume":"9","author":"Chen","year":"2020","journal-title":"ACM Transactions on Human-Robot Interaction (THRI)"},{"issue":"7","key":"2026033114013287400_ref061","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/j.ipl.2013.01.004","article-title":"On the Complexity of Model Checking Interval-Valued Discrete Time Markov Chains","volume":"113","author":"Chen","year":"2013","journal-title":"Information Processing Letters"},{"issue":"3","key":"2026033114013287400_ref062","doi-asserted-by":"crossref","first-page":"1528","DOI":"10.1137\/120871390","article-title":"Optimality Conditions and a Smoothing Trust Region Newton Method for Non-Lipschitz Optimization","volume":"23","author":"Chen","year":"2013","journal-title":"SIAM Journal on Optimization"},{"key":"2026033114013287400_ref063","first-page":"359","volume-title":"NuSMV 2: An OpenSource Tool for Symbolic Model Checking","author":"Cimatti","year":"2002"},{"key":"2026033114013287400_ref064","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Diagnostic Information for Realizability","author":"Cimatti","year":"2008"},{"key":"2026033114013287400_ref065","first-page":"532","volume-title":"Boolean Abstraction for Temporal Logic Satisfiability","author":"Cimatti","year":"2007"},{"issue":"2","key":"2026033114013287400_ref066","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"2026033114013287400_ref067","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/IROS.2007.4399374","volume-title":"Valet parking without a valet","author":"Conner","year":"2007"},{"key":"2026033114013287400_ref068","article-title":"Unmanned aerial vehicles","volume-title":"Handbook of Aviation Human Factors","author":"Cooke","year":"2009"},{"key":"2026033114013287400_ref069","volume-title":"IEEE Transactions on Automatic Control, Accepted","author":"Cubuktepe","year":"2020"},{"key":"2026033114013287400_ref070","first-page":"133","volume-title":"Sequential Convex Programming for the Efficient Verification of Parametric MDPs","author":"Cubuktepe","year":"2017"},{"key":"2026033114013287400_ref071","first-page":"160","volume-title":"Synthesis in pMDPs: A Tale of 1001 Parameters","author":"Cubuktepe","year":"2018"},{"key":"2026033114013287400_ref072","first-page":"287","volume-title":"Scenario-Based Verification of Uncertain MDPs","author":"Cubuktepe","year":"2020"},{"key":"2026033114013287400_ref073","first-page":"287","volume-title":"Scenario-Based Verification of Uncertain MDPs","author":"Cubuktepe","year":"2020"},{"key":"2026033114013287400_ref074","volume-title":"IEEE Transactions on Automatic Control, Under Revision","author":"Cubuktepe","year":"2021"},{"key":"2026033114013287400_ref075","first-page":"11792","volume-title":"Robust Finite-State Controllers for Uncertain POMDPs","author":"Cubuktepe","year":"2021"},{"key":"2026033114013287400_ref076","first-page":"280","volume-title":"Symbolic and Parametric Model Checking of Discrete-Time Markov Chains","author":"Daws","year":"2004"},{"issue":"7897","key":"2026033114013287400_ref077","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1038\/s41586-021-04301-9","article-title":"Magnetic control of tokamak plasmas through deep reinforcement learning","volume":"602","author":"Degrave","year":"2022","journal-title":"Nature"},{"key":"2026033114013287400_ref078","first-page":"214","volume-title":"PROPhESY: A PRObabilistic ParamEter SYnthesis Tool","author":"Dehnert","year":"2015"},{"key":"2026033114013287400_ref079","first-page":"592","volume-title":"A Storm is Coming: A Modern Probabilistic Model Checker","author":"Dehnert","year":"2017"},{"key":"2026033114013287400_ref080","first-page":"458475","volume-title":"Maximum Realizability for Linear Temporal Logic Specifications","author":"Dimitrova","year":"2018"},{"issue":"1","key":"2026033114013287400_ref081","doi-asserted-by":"crossref","first-page":"3515","DOI":"10.3182\/20110828-6-IT-1002.02287","article-title":"LTL control in uncertain environments with probabilistic satisfaction guarantees","volume":"44","author":"Ding","year":"2011","journal-title":"IFAC Proceedings Volumes"},{"key":"2026033114013287400_ref082","volume-title":"Task-Guided Inverse Reinforcement Learning under Partial Information","author":"Djeumou","year":"2021"},{"issue":"6","key":"2026033114013287400_ref083","doi-asserted-by":"publisher","first-page":"1180","DOI":"10.1109\/TSMCA.2010.2046731","article-title":"Modeling Workload Impact in Multiple Unmanned Vehicle Supervisory Control","volume":"40","author":"Donmez","year":"2010","journal-title":"IEEE Trans. Syst. Man Cybern. Part A"},{"key":"2026033114013287400_ref084","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"Donz\u00e9","year":"2010"},{"key":"2026033114013287400_ref085","first-page":"1","volume-title":"CARLA: An Open Urban Driving Simulator","author":"Dosovitskiy","year":"2017"},{"key":"2026033114013287400_ref086","volume-title":"Situational Reasoning for Road Driving in an Urban Environment","author":"DuToit","year":"2008"},{"key":"2026033114013287400_ref087","first-page":"117","volume-title":"Low-Effort Specification Debugging and Analysis","author":"Ehlers","year":"2014"},{"key":"2026033114013287400_ref088","first-page":"995","volume-title":"Handbook of theoretical computer science (vol. B): formal models and semantics","author":"Emerson","year":"1990"},{"key":"2026033114013287400_ref089","first-page":"34","article-title":"Robust predictable control","volume-title":"Advances in Neural Information Processing Systems","author":"Eysenbach","year":"2021"},{"key":"2026033114013287400_ref090","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-64203816-7\\_27","volume-title":"Admissible Strategies in Infinite Games over Graphs","author":"Faella","year":"2009"},{"issue":"5","key":"2026033114013287400_ref091","doi-asserted-by":"crossref","first-page":"4726","DOI":"10.1109\/TSG.2017.2667702","article-title":"Fisher information as a measure of privacy: Preserving privacy of households with smart meters using batteries","volume":"9","author":"Farokhi","year":"2017","journal-title":"IEEE Transactions on Smart Grid"},{"key":"2026033114013287400_ref092","first-page":"354","volume-title":"Encodings of Bounded Synthesis","author":"Faymonville","year":"2017"},{"key":"2026033114013287400_ref093","first-page":"7292","volume-title":"Counterexamples for robotic planning explained in structured language","author":"Feng","year":"2018"},{"key":"2026033114013287400_ref094","first-page":"1673","volume-title":"Human-interpretable diagnostic information for robotic planning systems","author":"Feng","year":"2016"},{"key":"2026033114013287400_ref095","first-page":"70","volume-title":"Controller synthesis for autonomous systems interacting with human operators","author":"Feng","year":"2015"},{"issue":"2","key":"2026033114013287400_ref096","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/TASE.2016.2530623","article-title":"Synthesis of Human-in-the-Loop Control Protocols for Autonomous Systems","volume":"13","author":"Feng","year":"2016","journal-title":"IEEE Trans Autom. Sci. Eng"},{"issue":"1","key":"2026033114013287400_ref097","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","article-title":"Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time","volume":"42","author":"Filieri","year":"2016","journal-title":"IEEE Trans. Software Eng"},{"key":"2026033114013287400_ref098","volume-title":"Final Theory of Driving: The Official Handbook","year":"2017","edition":"9th"},{"issue":"5-6","key":"2026033114013287400_ref099","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-012-0228-z","article-title":"Bounded synthesis","volume":"15","author":"Finkbeiner","year":"2013","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2026033114013287400_ref100","first-page":"112","volume-title":"Quantitative multi-objective verification for probabilistic systems","author":"Forejt","year":"2011"},{"key":"2026033114013287400_ref101","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-02150-8_1","volume-title":"Information and Control in Networks","author":"Franceschetti","year":"2014"},{"issue":"12","key":"2026033114013287400_ref102","doi-asserted-by":"crossref","first-page":"3100","DOI":"10.2514\/1.G002914","article-title":"Constrained Spacecraft Relative Motion Planning Exploiting Periodic Natural Motion Trajectories and Invariance","volume":"40","author":"Frey","year":"2017","journal-title":"Journal of Guidance, Control, and Dynamics"},{"key":"2026033114013287400_ref103","first-page":"3690","volume-title":"Optimal temporal logic planning in probabilistic semantic maps","author":"Fu","year":"2016"},{"key":"2026033114013287400_ref104","first-page":"2408","volume-title":"Integrating active sensing into reactive synthesis with temporal logic constraints under partial observations","author":"Fu","year":"2015"},{"issue":"11","key":"2026033114013287400_ref105","doi-asserted-by":"crossref","first-page":"3464","DOI":"10.1109\/TAC.2016.2518639","article-title":"Synthesis of joint control and active sensing strategies under temporal logic constraints","volume":"61","author":"Fu","year":"2016","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026033114013287400_ref106","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537915.001.0001","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming (Vol. 4): Epistemic and Temporal Reasoning","author":"Gabbay","year":"1995"},{"key":"2026033114013287400_ref107","volume-title":"Temporal Logics and Their Applications","author":"Galton","year":"1987"},{"key":"2026033114013287400_ref108","first-page":"3484","volume-title":"Task-oriented active perception and planning in environments with partially known semantics","author":"Ghasemi","year":"2020"},{"key":"2026033114013287400_ref109","first-page":"6169","volume-title":"Online Active Perception for Partially Observable Markov Decision Processes with Limited Budget","author":"Ghasemi","year":"2019"},{"key":"2026033114013287400_ref110","first-page":"2371","volume-title":"Perception-Aware Point-Based Value Iteration for Partially Observable Markov Decision Processes","author":"Ghasemi","year":"2019"},{"issue":"2","key":"2026033114013287400_ref111","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1016\/j.automatica.2008.09.016","article-title":"Hierarchical control system design using approximate simulation","volume":"45","author":"Girard","year":"2009","journal-title":"Automatica"},{"issue":"1-2","key":"2026033114013287400_ref112","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","article-title":"Bounded-Parameter Markov Decision Processes","volume":"122","author":"Givan","year":"2000","journal-title":"Artificial Intelligence"},{"key":"2026033114013287400_ref113","first-page":"1-105","volume-title":"Using SPIN model checking for flight software verification","author":"Gluck","year":"2002"},{"key":"2026033114013287400_ref114","first-page":"6266","volume-title":"Privacy-preserving policy synthesis in Markov decision processes","author":"Gohari","year":"2020"},{"key":"2026033114013287400_ref115","volume-title":"Deep Learning. Adaptive computation and machine learning","author":"Goodfellow","year":"2016"},{"key":"2026033114013287400_ref116","volume-title":"Qualitatively characterizing neural network optimization problems","author":"Goodfellow","year":"2015"},{"key":"2026033114013287400_ref117","volume-title":"Constrained Control and Estimation: An Optimisation Approach","author":"Goodwin","year":"2004"},{"key":"2026033114013287400_ref118","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata, logics, and infinite games: a guide to current research","author":"Gradel","year":"2002"},{"key":"2026033114013287400_ref119","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-46002-0_30","volume-title":"Temporal Debugging for Concurrent Systems","author":"Gunter","year":"2002"},{"key":"2026033114013287400_ref120","first-page":"5025","volume-title":"Revising motion planning under linear temporal logic specifications in partially known workspaces","author":"Guo","year":"2013"},{"key":"2026033114013287400_ref121","first-page":"207","volume-title":"Multi-Objective Robust Strategy Synthesis for Interval Markov Decision Processes","author":"Hahn","year":"2017"},{"issue":"1","key":"2026033114013287400_ref122","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","article-title":"Probabilistic reachability for parametric Markov models","volume":"13","author":"Hahn","year":"2010","journal-title":"Software Tools for Technology Transfer"},{"key":"2026033114013287400_ref123","first-page":"312","volume-title":"iscasMc: A Web-Based Probabilistic Model Checker","author":"Hahn","year":"2014"},{"key":"2026033114013287400_ref124","first-page":"395","volume-title":"Omega-regular objectives in model-free reinforcement learning","author":"Hahn","year":"2019"},{"issue":"2","key":"2026033114013287400_ref125","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/TSE.2009.5","article-title":"Counterexample generation in probabilistic model checking","volume":"35","author":"Han","year":"2009","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"2026033114013287400_ref126","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1109\/MDAT.2021.3069959","article-title":"Creating a Foundation for Next-Generation Autonomous Systems","volume":"39","author":"Harel","year":"2022","journal-title":"IEEE Design & Test"},{"key":"2026033114013287400_ref127","doi-asserted-by":"publisher","first-page":"5338","DOI":"10.1109\/CDC40024.2019.9028919","volume-title":"Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees","author":"Hasanbeig","year":"2019"},{"key":"2026033114013287400_ref128","first-page":"2012","volume-title":"Logically-Constrained Neural Fitted Q-Iteration","author":"Hasanbeig","year":"2019"},{"key":"2026033114013287400_ref129","first-page":"29","volume-title":"Deep Recurrent Q-Learning for Partially Observable MDPs","author":"Hausknecht","year":"2015"},{"issue":"8","key":"2026033114013287400_ref130","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","article-title":"Formal analysis of a space-craft controller using SPIN","volume":"27","author":"Havelund","year":"2001","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2026033114013287400_ref131","first-page":"303","volume-title":"Improving Robot Controller Transparency Through Autonomous Policy Explanation","author":"Hayes","year":"2017"},{"key":"2026033114013287400_ref132","first-page":"1512.04455","article-title":"Memory-based control with recurrent neural networks","volume-title":"CoRR","author":"Heess","year":"2015"},{"key":"2026033114013287400_ref133","first-page":"2944","volume-title":"Learning continuous control policies by stochastic value gradients","author":"Heess","year":"2015"},{"key":"2026033114013287400_ref134","volume-title":"Fast Bellman Updates for Robust MDPs","author":"Ho","year":"2018"},{"key":"2026033114013287400_ref135","first-page":"0877","volume-title":"A Taxonomy for Aerospace Collision Avoidance with Implications for Automation in Space Traffic Management","author":"Hobbs","year":"2020"},{"issue":"8","key":"2026033114013287400_ref136","doi-asserted-by":"crossref","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","article-title":"Long short-term memory","volume":"9","author":"Hochreiter","year":"1997","journal-title":"Neural Computation"},{"key":"2026033114013287400_ref137","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/978-1-4612-0865-5_26","volume-title":"The collected works of Wassily Hoeffding","author":"Hoeffding","year":"1994"},{"key":"2026033114013287400_ref138","first-page":"35","volume-title":"The Theory and Practice of A Formal Method: NewCoRe","author":"Holzmann","year":"1994"},{"key":"2026033114013287400_ref139","volume-title":"The Spin Model Checker","author":"Holzmann","year":"2004"},{"issue":"2","key":"2026033114013287400_ref140","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","article-title":"Mars Code","volume":"57","author":"Holzmann","year":"2014","journal-title":"Commun. ACM"},{"key":"2026033114013287400_ref141","article-title":"A Coordinated MDP Approach to Multi-Agent Planning for Resource Allocation, with Applications to Healthcare","volume-title":"arXiv preprint","author":"Hosseini","year":"2014"},{"key":"2026033114013287400_ref142","doi-asserted-by":"crossref","DOI":"10.2514\/6.2013-5183","volume-title":"Model Checking Human-Automation UAV Mission Plans","author":"Humphrey","year":"2013"},{"key":"2026033114013287400_ref143","volume-title":"Formal specification and synthesis of mission plans for unmanned aerial vehicles","author":"Humphrey","year":"2014"},{"key":"2026033114013287400_ref144","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-49052-6\\_9","volume-title":"Synthesis of Admissible Shields","author":"Humphrey","year":"2016"},{"key":"2026033114013287400_ref145","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"Huth","year":"2004","edition":"2nd"},{"key":"2026033114013287400_ref146","first-page":"2107","volume-title":"Using reward machines for high-level task specification and decomposition in reinforcement learning","author":"Icarte","year":"2018"},{"key":"2026033114013287400_ref147","first-page":"15523","volume-title":"Learning reward machines for partially observable reinforcement learning","author":"Icarte","year":"2019"},{"issue":"8","key":"2026033114013287400_ref148","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1016\/j.artint.2007.03.004","article-title":"Partially Observable Markov Decision Processes with Imprecise Parameters","volume":"171","author":"Itoh","year":"2007","journal-title":"Artificial Intelligence"},{"key":"2026033114013287400_ref149","volume-title":"Nonlinear Receding Horizon Control: A Control Lyapunov Function Approach","author":"Jadbabaie","year":"2000"},{"issue":"2","key":"2026033114013287400_ref150","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF00122418","article-title":"A formal approach to reactive systems software: a telecommunications application in ESTEREL","volume":"8","author":"Jagadeesan","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"2026033114013287400_ref151","volume-title":"Safe Reinforcement Learning Using Probabilistic Shields","author":"Jansen","year":"2020"},{"key":"2026033114013287400_ref152","first-page":"128","volume-title":"IEEE Transactions on Automatic Control","author":"Jiang","year":"2001"},{"key":"2026033114013287400_ref153","first-page":"4719","volume-title":"Distribution temporal logic: Combining correctness with quality of estimation","author":"Jones","year":"2013"},{"key":"2026033114013287400_ref154","first-page":"34","article-title":"Compositional reinforcement learning from logical specifications","volume-title":"Advances in Neural Information Processing Systems","author":"Jothimurugan","year":"2021"},{"issue":"3","key":"2026033114013287400_ref155","doi-asserted-by":"crossref","first-page":"598","DOI":"10.2514\/1.G003724","article-title":"Deep Neural Network Compression for Aircraft Collision Avoidance Systems","volume":"42","author":"Julian","year":"2019","journal-title":"Journal of Guidance, Control, and Dynamics"},{"key":"2026033114013287400_ref156","volume-title":"PhD thesis","author":"Junges","year":"2020"},{"key":"2026033114013287400_ref157","article-title":"Parameter Synthesis for Markov Models","volume":"abs\/1903.07993","author":"Junges","year":"2019","journal-title":"CoRR"},{"key":"2026033114013287400_ref158","first-page":"519","volume-title":"Finite-state controllers of POMDPs via parameter synthesis","author":"Junges","year":"2018"},{"key":"2026033114013287400_ref159","volume-title":"Planning Not to |Talk: Multiagent Systems that are Robust to Communication Loss","author":"Karabag","year":"2022"},{"key":"2026033114013287400_ref160","first-page":"1224","volume-title":"Least inferable policies for Markov decision processes","author":"Karabag","year":"2019"},{"key":"2026033114013287400_ref161","article-title":"Deception in Supervisory Control","volume-title":"IEEE Transactions on Automatic Control","author":"Karabag","year":"2021"},{"key":"2026033114013287400_ref162","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.2009.5400278","volume-title":"Sampling-based Motion Planning with Deterministic \u03bc-Calculus Specifications","author":"Karaman","year":"2009"},{"key":"2026033114013287400_ref163","first-page":"1001","volume-title":"Approximate Planning in Large POMDPs via Reusable Trajectories","author":"Kearns","year":"1999"},{"key":"2026033114013287400_ref164","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-1-4842-2766-4_7","volume-title":"Deep learning with Python","author":"Ketkar","year":"2017"},{"issue":"12","key":"2026033114013287400_ref165","doi-asserted-by":"crossref","DOI":"10.1177\/0278364915587034","article-title":"On the minimal revision problem of specification automata","volume":"34","author":"Kim","year":"2015","journal-title":"International Journal of Robotics Research"},{"key":"2026033114013287400_ref166","first-page":"1","volume-title":"Mission Design and Trajectory Analysis for Inspection of a Host Spacecraft by a Microsatellite","author":"Kim","year":"2007"},{"key":"2026033114013287400_ref167","volume-title":"Adam: A Method for Stochastic Optimization","author":"Kingma","year":"2015"},{"key":"2026033114013287400_ref168","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-540-76336-9_7","volume-title":"Implementation and Application of Automata","author":"Klein","year":"2007"},{"issue":"1","key":"2026033114013287400_ref169","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1109\/TAC.2007.914952","article-title":"A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications","volume":"53","author":"Kloetzer","year":"2008","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026033114013287400_ref170","first-page":"287","volume-title":"Dealing with Nondeterminism in Symbolic Control","author":"Kloetzer","year":"2008"},{"key":"2026033114013287400_ref171","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0276-9","article-title":"Shield synthesis","volume-title":"Formal Methods Syst. Des","author":"K\u00f6nighofer","year":"2017"},{"key":"2026033114013287400_ref172","volume-title":"Learning Finite State Representations of Recurrent Policy Networks","author":"Koul","year":"2019"},{"issue":"3","key":"2026033114013287400_ref173","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"2026033114013287400_ref174","doi-asserted-by":"publisher","first-page":"3116","DOI":"10.1109\/ROBOT.2007.363946","volume-title":"Where\u2019s Waldo? Sensor-Based Temporal Logic Motion Planning","author":"Kress-Gazit","year":"2007"},{"issue":"6","key":"2026033114013287400_ref175","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","article-title":"Temporal-logic-based reactive mission and motion planning","volume":"25","author":"Kress-Gazit","year":"2009","journal-title":"IEEE transactions on robotics"},{"issue":"3","key":"2026033114013287400_ref176","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1109\/MRA.2011.942116","article-title":"Correct, Reactive, High-Level Robot Control","volume":"18","author":"Kress-Gazit","year":"2011","journal-title":"IEEE Robotics Automation Magazine"},{"issue":"3","key":"2026033114013287400_ref177","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","article-title":"Model checking of safety properties","volume":"19","author":"Kupferman","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"2026033114013287400_ref178","first-page":"531","volume-title":"Safraless Decision Procedures","author":"Kupferman","year":"2005"},{"key":"2026033114013287400_ref179","first-page":"585","volume-title":"PRISM 4.0: Verification of Probabilistic Real-Time Systems","author":"Kwiatkowska","year":"2011"},{"key":"2026033114013287400_ref180","volume-title":"This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction","author":"Lahijanian","year":"2015"},{"key":"2026033114013287400_ref181","first-page":"7411","volume-title":"Specification revision for Markov decision processes with optimal trade-off","author":"Lahijanian","year":"2016"},{"issue":"3","key":"2026033114013287400_ref182","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1109\/TRO.2016.2544339","article-title":"Iterative temporal planning in uncertain environments with partial satisfaction guarantees","volume":"32","author":"Lahijanian","year":"2016","journal-title":"IEEE Transactions on Robotics"},{"key":"2026033114013287400_ref183","volume-title":"Specifying systems: The TLA + language and tools for hardware and software engineers","author":"Lamport","year":"2002"},{"issue":"2","key":"2026033114013287400_ref184","doi-asserted-by":"crossref","first-page":"190222","DOI":"10.1145\/69624.357207","article-title":"Specifying concurrent program modules","volume":"5","author":"Lamport","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"2026033114013287400_ref185","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The Temporal Logic of Actions","volume":"16","author":"Lamport","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"2026033114013287400_ref186","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","article-title":"Parametric Probabilistic Transition Systems for System Design and Analysis","volume":"19","author":"Lanotte","year":"2007","journal-title":"Formal Aspects Comput"},{"key":"2026033114013287400_ref187","article-title":"Non-Stationary Markov Decision Processes, a Worst-Case Approach using Model-Based Reinforcement Learning, Extended Version","volume-title":"arXiv preprint","author":"Lecarpentier","year":"2019"},{"key":"2026033114013287400_ref188","article-title":"AI Safety Gridworlds","volume":"abs\/1711.09883","author":"Leike","year":"2017","journal-title":"CoRR"},{"issue":"5","key":"2026033114013287400_ref189","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","article-title":"A brief account of runtime verification","volume":"78","author":"Leucker","year":"2009","journal-title":"J. Log. Algebraic Methods Program"},{"issue":"1","key":"2026033114013287400_ref190","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10514-014-9418-8","article-title":"Provably correct reactive control from natural language","volume":"38","author":"Lignos","year":"2015","journal-title":"Autonomous Robots"},{"issue":"1","key":"2026033114013287400_ref191","first-page":"341","article-title":"Analysis and synthesis of discrete event systems using temporal logic","volume":"9","author":"Lin","year":"1993","journal-title":"Control Theory and Advanced Technologies"},{"key":"2026033114013287400_ref192","first-page":"615","volume-title":"Reinforcement Learning for Robot Navigation in Nondeterministic Environments","author":"Liu","year":"2018"},{"key":"2026033114013287400_ref193","first-page":"5163","volume-title":"Backtracking temporal logic synthesis for uncertain environments","author":"Livingston","year":"2012"},{"key":"2026033114013287400_ref194","first-page":"587","volume-title":"Verifying the Long-run Behavior of Probabilistic System Models in the Presence of Uncertainty","author":"Llerena","year":"2018"},{"key":"2026033114013287400_ref195","first-page":"541","volume-title":"On the Undecidability of Probabilistic Planning and Infinite-Horizon Partially Observable Markov Decision Problems","author":"Madani","year":"1999"},{"key":"2026033114013287400_ref196","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"key":"2026033114013287400_ref197","article-title":"Successive Con-vexification: A Superlinearly Convergent Algorithm for Non-convex Optimal Control Problems","volume-title":"arXiv preprint","author":"Mao","year":"2018"},{"key":"2026033114013287400_ref198","doi-asserted-by":"crossref","DOI":"10.5220\/0006156001050117","volume-title":"Assured Reinforcement Learning with Formally Verified Abstract Policies","author":"Mason","year":"2017"},{"key":"2026033114013287400_ref199","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1016\/S0005-1098(99)00214-9","article-title":"Constrained model predictive control: Stability and optimality","volume":"36","author":"Mayne","year":"2000","journal-title":"Automatica"},{"key":"2026033114013287400_ref200","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4\\_2","volume-title":"Infinite Games","author":"Mazala","year":"2001"},{"issue":"4","key":"2026033114013287400_ref201","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF02478259","article-title":"A logical calculus of the ideas immanent in nervous activity","volume":"5","author":"McCulloch","year":"1943","journal-title":"The bulletin of mathematical biophysics"},{"key":"2026033114013287400_ref202","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"2026033114013287400_ref203","doi-asserted-by":"publisher","first-page":"5312","DOI":"10.1109\/CDC40024.2019.9029989","volume-title":"Average-based Robustness for Continuous-Time Signal Temporal Logic","author":"Mehdipour","year":"2019"},{"key":"2026033114013287400_ref204","first-page":"417","volume-title":"Solving POMDPs by Searching the Space of Finite Policies","author":"Meuleau","year":"1999"},{"key":"2026033114013287400_ref205","first-page":"84","volume-title":"Practical Stutter-Invariance Checks for \u03c9-Regular Languages","author":"Michaud","year":"2015"},{"key":"2026033114013287400_ref206","article-title":"Privacy in deep learning: A survey","volume-title":"arXiv preprint","author":"Mireshghallah","year":"2020"},{"key":"2026033114013287400_ref207","first-page":"134","volume-title":"Sampling-based reactive motion planning with temporal logic constraints and imperfect state information","author":"Montana","year":"2017"},{"issue":"1","key":"2026033114013287400_ref208","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.csl.2014.09.005","article-title":"A survey on the application of recurrent neural networks to statistical language modeling","volume":"30","author":"Mulder","year":"2015","journal-title":"Computer Speech & Language"},{"key":"2026033114013287400_ref209","volume-title":"Software-Enabled Control: Information Technology for Dynamical Systems","author":"Murray","year":"2003"},{"issue":"2","key":"2026033114013287400_ref210","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1137\/S0363012902402116","article-title":"Stabilizability of stochastic linear systems with finite feedback data rates","volume":"43","author":"Nair","year":"2004","journal-title":"SIAM Journal on Control and Optimization"},{"key":"2026033114013287400_ref211","doi-asserted-by":"crossref","DOI":"10.1609\/icaps.v32i1.19849","volume-title":"Verifiable and Compositional Reinforcement Learning Systems","author":"Neary","year":"2022"},{"key":"2026033114013287400_ref212","first-page":"934","volume-title":"Reward Machines for Cooperative Multi-Agent Reinforcement Learning","author":"Neary","year":"2021"},{"key":"2026033114013287400_ref213","doi-asserted-by":"publisher","DOI":"10.1145\/2699417","article-title":"How Amazon web services uses formal methods","volume-title":"Communications of the ACM","author":"Newcombe","year":"2015"},{"issue":"5","key":"2026033114013287400_ref214","doi-asserted-by":"crossref","first-page":"780","DOI":"10.1287\/opre.1050.0216","article-title":"Robust Control of Markov Decision Processes with Uncertain Transition Matrices","volume":"53","author":"Nilim","year":"2005","journal-title":"Operations Research"},{"issue":"3","key":"2026033114013287400_ref215","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","article-title":"Verification and Control of Partially Observable Probabilistic Systems","volume":"53","author":"Norman","year":"2017","journal-title":"Real-Time Systems"},{"issue":"3","key":"2026033114013287400_ref216","doi-asserted-by":"crossref","first-page":"1042","DOI":"10.1007\/s10957-016-0892-3","article-title":"Conic Optimization via Operator Splitting and Homogeneous Self-Dual Embedding","volume":"169","author":"O\u2019Donoghue","year":"2016","journal-title":"Journal of Optimization Theory and Applications"},{"issue":"2","key":"2026033114013287400_ref217","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1177\/0278364917692864","article-title":"Decentralized Control of Multi-Robot Partially Observable Markov Decision Processes Using Belief Space Macro-Actions","volume":"36","author":"Omidshafiei","year":"2017","journal-title":"The International Journal of Robotics Research"},{"key":"2026033114013287400_ref218","first-page":"106","volume-title":"Robust Partially Observable Markov Decision Process","author":"Osogami","year":"2015"},{"issue":"1","key":"2026033114013287400_ref219","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/TIV.2016.2578706","article-title":"A Survey of Motion Planning and Control Techniques for Self-Driving Urban Vehicles","volume":"1","author":"Paden","year":"2016","journal-title":"IEEE Transactions on Intelligent Vehicles"},{"key":"2026033114013287400_ref220","volume-title":"How to Construct Deep Recurrent Neural Networks","author":"Pascanu","year":"2014"},{"issue":"5","key":"2026033114013287400_ref221","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","article-title":"Stutter-invariant temporal properties are expressible without the next-time operator","volume":"63","author":"Peled","year":"1997","journal-title":"Inf. Process. Lett"},{"key":"2026033114013287400_ref222","doi-asserted-by":"crossref","DOI":"10.1109\/CDC40024.2019.9030068","volume-title":"Towards Assume-Guarantee Profiles for Autonomous Vehicles","author":"Phan-Minh","year":"2019"},{"key":"2026033114013287400_ref223","first-page":"1025","volume-title":"Point-based value iteration: An anytime algorithm for POMDPs","author":"Pineau","year":"2003"},{"key":"2026033114013287400_ref224","first-page":"364","volume-title":"Verification, Model Checking and Abstract Interpretation","author":"Piterman","year":"2006"},{"key":"2026033114013287400_ref225","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","article-title":"Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends","volume-title":"Current Trends in Concurrency. Overviews and Tutorials","author":"Pnueli","year":"1986"},{"key":"2026033114013287400_ref226","first-page":"179","volume-title":"On the synthesis of a reactive module","author":"Pnueli","year":"1989"},{"key":"2026033114013287400_ref227","first-page":"46","volume-title":"The Temporal Logic of Programs","author":"Pnueli","year":"1977"},{"key":"2026033114013287400_ref228","first-page":"823","volume-title":"Bounded Finite State Controllers","author":"Poupart","year":"2003"},{"key":"2026033114013287400_ref229","doi-asserted-by":"crossref","DOI":"10.1002\/9781119815068","volume-title":"Reinforcement Learning and Stochastic Optimization: A unified framework for sequential decisions","author":"Powell","year":"2022"},{"key":"2026033114013287400_ref230","doi-asserted-by":"crossref","first-page":"527","DOI":"10.21236\/ADA583813","volume-title":"Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties","author":"Puggelli","year":"2013"},{"key":"2026033114013287400_ref231","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman","year":"2014"},{"key":"2026033114013287400_ref232","first-page":"50","volume-title":"Parameter Synthesis for Markov Models: Faster than Ever","author":"Quatmann","year":"2016"},{"key":"2026033114013287400_ref233","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114","article-title":"Finite automata and their decision problems","volume-title":"IBM J. Res. Dev","author":"Rabin","year":"1959"},{"key":"2026033114013287400_ref234","first-page":"3","volume-title":"Solving F3 MDPs: Collaborative Multiagent Markov Decision Processes with Factored Transitions, Rewards and Stochastic Policies","author":"Radoszycki","year":"2015"},{"key":"2026033114013287400_ref235","first-page":"757","volume-title":"Towards minimal explanations of unsynthesizability for high-level robot behaviors","author":"Raman","year":"2013"},{"key":"2026033114013287400_ref236","first-page":"5056","volume-title":"Notions of security and opacity in discrete event systems","author":"Saboori","year":"2007"},{"key":"2026033114013287400_ref237","first-page":"44","volume-title":"Multi-Objective Approaches to Markov Decision Processes with Uncertain Transition Parameters","author":"Scheftelowitsch","year":"2017"},{"key":"2026033114013287400_ref238","first-page":"474","volume-title":"Bounded Synthesis","author":"Schewe","year":"2007"},{"key":"2026033114013287400_ref239","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/ICRE.1998.667803","volume-title":"Validating requirements for fault tolerant systems using model checking","author":"Schneider","year":"1998"},{"issue":"7-8","key":"2026033114013287400_ref240","doi-asserted-by":"crossref","first-page":"908939","DOI":"10.1016\/j.scico.2010.11.004","article-title":"Towards a notion of unsatisfiable and unrealizable cores for LTL","volume":"77","author":"Schuppan","year":"2012","journal-title":"Science of Computer Programming"},{"key":"2026033114013287400_ref241","first-page":"394","volume-title":"Model-Checking Markov Chains in the Presence of Uncertainties","author":"Sen","year":"2006"},{"issue":"2","key":"2026033114013287400_ref242","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1109\/70.282546","article-title":"A temporal framework for assembly sequence representation and analysis","volume":"10","author":"Seow","year":"1994","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"2026033114013287400_ref243","doi-asserted-by":"crossref","unstructured":"Shah, S., D.Dey, C.Lovett, and A.Kapoor. (2017). \u201cAirSim: High-Fidelity Visual and Physical Simulation for Autonomous Vehicles\u201d. In: Field and Service Robotics. eprint: arXiv:1705.05065. url: https:\/\/arxiv.org\/abs\/1705.05065.","DOI":"10.1007\/978-3-319-67361-5_40"},{"key":"2026033114013287400_ref244","article-title":"On a Formal Model of Safe and Scalable Self-driving Cars","volume":"abs\/1708.06374","author":"Shalev-Shwartz","year":"2017","journal-title":"ArXiv"},{"key":"2026033114013287400_ref245","doi-asserted-by":"crossref","first-page":"132306","DOI":"10.1016\/j.physd.2019.132306","article-title":"Fundamentals of recurrent neural network (RNN) and long short-term memory (LSTM) network","volume":"404","author":"Sherstinsky","year":"2020","journal-title":"Physica D: Nonlinear Phenomena"},{"issue":"4","key":"2026033114013287400_ref246","doi-asserted-by":"crossref","first-page":"1068","DOI":"10.1109\/LCSYS.2019.2920826","article-title":"Active Perception and Control From Temporal Logic Specifications","volume":"3","author":"da Silva","year":"2019","journal-title":"IEEE Control Systems Letters"},{"issue":"6419","key":"2026033114013287400_ref247","doi-asserted-by":"crossref","first-page":"1140","DOI":"10.1126\/science.aar6404","article-title":"A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play","volume":"362","author":"Silver","year":"2018","journal-title":"Science"},{"key":"2026033114013287400_ref248","first-page":"479","volume-title":"Are Parametric Markov Chains Monotonic","author":"Spel","year":"2019"},{"key":"2026033114013287400_ref249","doi-asserted-by":"publisher","first-page":"19911996","DOI":"10.1109\/CDC.2018.8619113","volume-title":"Control of MultiAgent Systems with Finite Time Control Barrier Certificates and Temporal Logic","author":"Srinivasan","year":"2018"},{"key":"2026033114013287400_ref250","article-title":"Multi-Model Markov Decision Processes","volume-title":"Optimization Online","author":"Steimle","year":"2018"},{"key":"2026033114013287400_ref251","first-page":"4761","volume-title":"Privacy and autonomous systems","author":"Such","year":"2017"},{"key":"2026033114013287400_ref252","first-page":"4113","volume-title":"Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization","author":"Suilen","year":"2020"},{"key":"2026033114013287400_ref253","volume-title":"Reinforcement Learning: An Introduction","author":"Sutton","year":"2018"},{"key":"2026033114013287400_ref254","first-page":"10:1","volume-title":"Robust Linear Temporal Logic","author":"Tabuada","year":"2016"},{"issue":"12","key":"2026033114013287400_ref255","doi-asserted-by":"crossref","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","article-title":"Linear Time Logic control of linear systems","volume":"51","author":"Tabuada","year":"2006","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026033114013287400_ref256","article-title":"Transfer-entropy-regularized markov decision processes","volume-title":"IEEE Transactions on Automatic Control","author":"Tanaka","year":"2021"},{"key":"2026033114013287400_ref257","first-page":"4740","volume-title":"Predictive Off-Policy Policy Evaluation for Nonstationary Decision Problems, with Applications to Digital Marketing","author":"Thomas","year":"2017"},{"issue":"7","key":"2026033114013287400_ref258","doi-asserted-by":"crossref","DOI":"10.1007\/s00236-016-0280-3","article-title":"Safraless LTL synthesis considering maximal realizability","volume":"54","author":"Tomita","year":"2017","journal-title":"Acta Informatica"},{"issue":"2","key":"2026033114013287400_ref259","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10626-017-0264-7","article-title":"Current-state opacity enforcement in discrete event systems under incomparable observations","volume":"28","author":"Tong","year":"2018","journal-title":"Discrete Event Dynamic Systems"},{"key":"2026033114013287400_ref260","first-page":"73","article-title":"Reward Machines:: Exploiting Reward Function Structure in Reinforcement Learning","volume-title":"Journal of Artificial Intelligence Research","author":"Toro Icarte","year":"2022"},{"key":"2026033114013287400_ref261","doi-asserted-by":"crossref","DOI":"10.1145\/2461328.2461330","volume-title":"Least-violating control strategy synthesis with safety rules","author":"Tumova","year":"2013"},{"key":"2026033114013287400_ref262","first-page":"4817","volume-title":"Sampling-based temporal logic path planning","author":"Vasile","year":"2013"},{"issue":"4","key":"2026033114013287400_ref263","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/2382559.2382563","article-title":"On the Computational Complexity of Stochastic Controller Optimization in POMDPs","volume":"4","author":"Vlassis","year":"2012","journal-title":"ACM Trans. on Computation Theory"},{"key":"2026033114013287400_ref264","doi-asserted-by":"crossref","DOI":"10.1609\/aaai.v31i1.11032","volume-title":"Accelerated Vector Pruning for Optimal POMDP Solvers","author":"Walraven","year":"2017"},{"key":"2026033114013287400_ref265","first-page":"9908","volume-title":"Learning efficient multi-agent communication: An information bottleneck approach","author":"Wang","year":"2020"},{"key":"2026033114013287400_ref266","doi-asserted-by":"publisher","first-page":"3055","DOI":"10.24963\/ijcai.2017\/426","volume-title":"Learning from Demonstrations with High-Level Side Information","author":"Wen","year":"2017"},{"key":"2026033114013287400_ref267","first-page":"697","volume-title":"Solving deep memory POMDPs with recurrent policy gradients","author":"Wierstra","year":"2007"},{"issue":"1","key":"2026033114013287400_ref268","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1287\/moor.1120.0566","article-title":"Robust Markov Decision Processes","volume":"38","author":"Wiesemann","year":"2013","journal-title":"Mathematics of Operations Research"},{"key":"2026033114013287400_ref269","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.tcs.2014.06.020","article-title":"Minimal counterexamples for linear-time probabilistic verification","volume":"549","author":"Wimmer","year":"2014","journal-title":"Theoretical Computer Science"},{"key":"2026033114013287400_ref270","first-page":"39","volume-title":"High-level counterexamples for probabilistic automata","author":"Wimmer","year":"2013"},{"key":"2026033114013287400_ref271","first-page":"14:1","volume-title":"On the Complexity of Reachability in Parametric Markov Decision Processes","author":"Winkler","year":"2019"},{"key":"2026033114013287400_ref272","first-page":"3372","volume-title":"Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications","author":"Wolff","year":"2012"},{"key":"2026033114013287400_ref273","first-page":"1168","volume-title":"Synthesis of provably correct controllers for autonomous vehicles in urban environments","author":"Wongpiromsarn","year":"2011"},{"key":"2026033114013287400_ref274","volume-title":"Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle","author":"Wongpiromsarn","year":"2010"},{"key":"2026033114013287400_ref275","unstructured":"Wongpiromsarn, T.\n           (2020). \u201cThe Journey of Autonomous Vehicles\u201d. URL: https:\/\/tichakorn.dev\/post\/av-journey\/."},{"key":"2026033114013287400_ref276","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-642-00602-9_28","volume-title":"Hybrid Systems: Computation and Control","author":"Wongpiromsarn","year":"2009"},{"key":"2026033114013287400_ref277","volume-title":"Distributed Mission and Contingency Management for the DARPA Urban Challenge","author":"Wongpiromsarn","year":"2008"},{"key":"2026033114013287400_ref278","volume-title":"Minimum-Violation Planning for Autonomous Systems: Theoretical and Practical Considerations","author":"Wongpiromsarn","year":"2021"},{"key":"2026033114013287400_ref279","first-page":"104","volume-title":"Automatic Synthesis of Robust Embedded Control Software","author":"Wongpiromsarn","year":"2010"},{"key":"2026033114013287400_ref280","first-page":"101","volume-title":"Receding horizon control for temporal logic specifications","author":"Wongpiromsarn","year":"2010"},{"issue":"11","key":"2026033114013287400_ref281","doi-asserted-by":"crossref","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","article-title":"Receding Horizon Temporal Logic Planning","volume":"57","author":"Wongpiromsarn","year":"2012","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"1","key":"2026033114013287400_ref282","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S2301385013500027","article-title":"Synthesis of Control Protocols for Autonomous Systems","volume":"1","author":"Wongpiromsarn","year":"2013","journal-title":"Unmanned Systems"},{"key":"2026033114013287400_ref283","first-page":"313","volume-title":"TuLiP: A Software Toolbox for Receding Horizon Temporal Logic Planning","author":"Wongpiromsarn","year":"2011"},{"issue":"8-9","key":"2026033114013287400_ref284","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","article-title":"Reachability Analysis of Uncertain Systems using Bounded-Parameter Markov Decision Processes","volume":"172","author":"Wu","year":"2008","journal-title":"Artificial Intelligence"},{"key":"2026033114013287400_ref285","first-page":"590598","volume-title":"Joint inference of reward machines and policies for reinforcement learning","author":"Xu","year":"2020"},{"key":"2026033114013287400_ref286","article-title":"On the Privacy Risks of Deploying Recurrent Neural Networks in Machine Learning","volume-title":"arXiv preprint","author":"Yang","year":"2021"},{"key":"2026033114013287400_ref287","first-page":"54","volume-title":"Model Checking TLA+ Specifications","author":"Yu","year":"1999"},{"issue":"1","key":"2026033114013287400_ref288","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10107-015-0893-2","article-title":"Recent Advances in Trust Region Algorithms","volume":"151","author":"Yuan","year":"2015","journal-title":"Mathematical Programming"},{"key":"2026033114013287400_ref289","first-page":"540","volume-title":"Hypothesis testing game for cyber deception","author":"Zhang","year":"2018"}],"container-title":["Foundations and Trends\u00ae in Systems and Control"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftsys\/article-pdf\/10\/3-4\/180\/11161204\/2600000029en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftsys\/article-pdf\/10\/3-4\/180\/11161204\/2600000029en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T18:02:17Z","timestamp":1774980137000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftsys\/article\/10\/3-4\/180\/1332872\/Formal-Methods-for-Autonomous-Systems"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,21]]},"references-count":289,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2023,9,21]]}},"URL":"https:\/\/doi.org\/10.1561\/2600000029","relation":{},"ISSN":["2325-6818","2325-6826"],"issn-type":[{"value":"2325-6818","type":"print"},{"value":"2325-6826","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,21]]}}}