ref_verification.bib

@techreport{14:00-17:00ISO2626212018,
  type = {Standard},
  title = {Road Vehicles --- {{Functional}} Safety --- {{Part}} 1: {{Vocabulary}}},
  shorttitle = {{{ISO}} 26262-1},
  author = {{ISO}},
  year = {2018},
  number = {ISO 26262-1:2018},
  pages = {33},
  url = {https://www.iso.org/cms/render/live/en/sites/isoorg/contents/data/standard/06/83/68383.html},
  urldate = {2022-08-24},
  langid = {english}
}

@inproceedings{abateARCHCOMPFriendlyVerification2025,
  title = {The {{ARCH-COMP Friendly Verification Competition}} for~{{Continuous}} and~{{Hybrid Systems}}},
  booktitle = {{{TOOLympics Challenge}} 2023},
  author = {Abate, Alessandro and Althoff, Matthias and Bu, Lei and Ernst, Gidon and Frehse, Goran and Geretti, Luca and Johnson, Taylor T. and Menghi, Claudio and Mitsch, Stefan and Schupp, Stefan and Soudjani, Sadegh},
  editor = {Beyer, Dirk and Hartmanns, Arnd and Kordon, Fabrice},
  year = {2025},
  pages = {1--37},
  publisher = {Springer Nature Switzerland},
  address = {Cham},
  doi = {10.1007/978-3-031-67695-6_1},
  abstract = {The workshop on Applied Verification for Continuous and Hybrid Systems (ARCH) is an annual venue for researchers and practitioners working on automated analysis and verification of hybrid systems. ARCH-COMP is a friendly competition held with the ARCH event. The competition was established in 2017 and aims to explore, document, and push forward the state of the art in the field. It evaluates and compares methods and tools for automated hybrid systems analysis and verification on predefined benchmark problems. It is supported by an active community around several categories of problems, including linear and nonlinear systems, simulation-based and analytic methods, and models from many application domains, such as automotive systems or neural networks. This paper describes the format of the competition and its organization. It documents the experiences and decisions from the current and past editions of the competition and presents reflections and lessons learned.},
  isbn = {978-3-031-67695-6},
  langid = {english}
}

@phdthesis{ahmadiNonmonotonicLyapunovFunctions2008,
  type = {Thesis},
  title = {Non-Monotonic {{Lyapunov}} Functions for Stability of Nonlinear and Switched Systems : Theory and Computation},
  shorttitle = {Non-Monotonic {{Lyapunov}} Functions for Stability of Nonlinear and Switched Systems},
  author = {Ahmadi, Amir Ali},
  year = {2008},
  address = {Cambridge},
  url = {https://dspace.mit.edu/handle/1721.1/44206},
  urldate = {2022-08-15},
  abstract = {Lyapunov's direct method, which is based on the existence of a scalar function of the state that decreases monotonically along trajectories, still serves as the primary tool for establishing stability of nonlinear systems. Since the main challenge in stability analysis based on Lyapunov theory is always to nd a suitable Lyapunov function, weakening the requirements of the Lyapunov function is of great interest. In this thesis, we relax the monotonicity requirement of Lyapunov's theorem to enlarge the class of functions that can provide certicates of stability. Both the discrete time case and the continuous time case are covered. Throughout the thesis, special attention is given to techniques from convex optimization that allow for computationally tractable ways of searching for Lyapunov functions. Our theoretical contributions are therefore amenable to convex programming formulations. In the discrete time case, we propose two new sucient conditions for global asymptotic stability that allow the Lyapunov functions to increase locally, but guarantee an average decrease every few steps. Our first condition is nonconvex, but allows an intuitive interpretation. The second condition, which includes the first one as a special case, is convex and can be cast as a semidenite program. We show that when non-monotonic Lyapunov functions exist, one can construct a more complicated function that decreases monotonically. We demonstrate the strength of our methodology over standard Lyapunov theory through examples from three different classes of dynamical systems. First, we consider polynomial dynamics where we utilize techniques from sum-of-squares programming. Second, analysis of piecewise ane systems is performed. Here, connections to the method of piecewise quadratic Lyapunov functions are made.},
  copyright = {M.I.T. theses are protected by  copyright. They may be viewed from this source for any purpose, but  reproduction or distribution in any format is prohibited without written  permission. See provided URL for inquiries about permission.},
  langid = {english},
  school = {Massachusetts Institute of Technology},
  annotation = {Accepted: 2009-01-26T22:01:31Z}
}

@article{alanControlBarrierFunctions2023,
  title = {Control {{Barrier Functions}} and {{Input-to-State Safety With Application}} to {{Automated Vehicles}}},
  author = {Alan, Anil and Taylor, Andrew J. and He, Chaozhe R. and Ames, Aaron D. and Orosz, G{\'a}bor},
  year = {2023},
  month = nov,
  journal = {IEEE Transactions on Control Systems Technology},
  volume = {31},
  number = {6},
  pages = {2744--2759},
  issn = {1558-0865},
  doi = {10.1109/TCST.2023.3286090},
  url = {https://ieeexplore.ieee.org/abstract/document/10164803?casa_token=MwfI13XJZ8AAAAAA:6s_ljVbt7Y5Pb6BsH7gJmHLOPlLWYtZG3Zrl2WeFzx5gPMqafL-CUOM7FbTR3te38J0cHykp6w},
  urldate = {2023-12-21},
  abstract = {Balancing safety and performance is one of the predominant challenges in modern control system design. Moreover, it is crucial to robustly ensure safety without inducing unnecessary conservativeness that degrades performance. In this work, we present a constructive approach for safety-critical control synthesis via control barrier functions (CBFs). By filtering a hand-designed controller via a CBF, we are able to attain performant behavior while providing rigorous guarantees of safety. In the face of disturbances, robust safety and performance are simultaneously achieved through the notion of input-to-state safety (ISSf). We take a tutorial approach by developing the CBF-design methodology in parallel with an inverted pendulum example, making the challenges and sensitivities in the design process concrete. To establish the capability of the proposed approach, we consider the practical setting of safety-critical design via CBFs for a connected automated vehicle (CAV) in the form of a class-8 truck without a trailer. Through experimentation, we see the impact of unmodeled disturbances in the truck's actuation system on the safety guarantees provided by CBFs. We characterize these disturbances and using ISSf, produce a robust controller that achieves safety without conceding performance. We evaluate our design both in simulation, and for the first time on an automotive system, experimentally.}
}

@article{alanEnergyCriticalControlUsing2023,
  title = {Energy-{{Critical Control Using Control Barrier Functions}}},
  author = {Alan, Anil and Ivanco, Andrej and Orosz, G{\'a}bor},
  year = {2023},
  journal = {IEEE Control Systems Letters},
  pages = {1--1},
  issn = {2475-1456},
  doi = {10.1109/LCSYS.2023.3342771},
  url = {https://ieeexplore.ieee.org/abstract/document/10356903},
  urldate = {2023-12-30},
  abstract = {This study proposes an energy-critical control scheme for road vehicles. The framework is designed to ensure an energy-critical goal that is defined in the form of an upper bound on the energy consumption. In order to respond to the changing traffic environment, this bound is changed based on the preceding vehicle's energy consumption. Control barrier functions are used to obtain a condition on the control input such that the energy-critical goal is formally guaranteed. This condition is used in a quadratic program scheme as a constraint, and the resulting controller intervenes the driver input in a minimally-invasive fashion. The effect of the energy-critical controller is demonstrated in data-based simulations, where up to 25\% improvement in energy consumption is observed compared to an energy-inefficient driver, without drastically changing the car-following performance.}
}

@misc{allamaaRealtimeMPCControl2024,
  title = {Real-Time {{MPC}} with {{Control Barrier Functions}} for {{Autonomous Driving}} Using {{Safety Enhanced Collocation}}},
  author = {Allamaa, Jean Pierre and Patrinos, Panagiotis and Ohtsuka, Toshiyuki and Son, Tong Duy},
  year = {2024},
  month = jul,
  number = {arXiv:2401.06648},
  eprint = {2401.06648},
  primaryclass = {cs, eess, math},
  publisher = {arXiv},
  doi = {10.48550/arXiv.2401.06648},
  url = {http://arxiv.org/abs/2401.06648},
  urldate = {2024-08-29},
  abstract = {The autonomous driving industry is continuously dealing with safety-critical scenarios, and nonlinear model predictive control (NMPC) is a powerful control strategy for handling such situations. However, standard safety constraints are not scalable and require a long NMPC horizon. Moreover, the adoption of NMPC in the automotive industry is limited by the heavy computation of numerical optimization routines. To address those issues, this paper presents a real-time capable NMPC for automated driving in urban environments, using control barrier functions (CBFs). Furthermore, the designed NMPC is based on a novel collocation transcription approach, named RESAFE/COL, that allows to reduce the number of optimization variables while still guaranteeing the continuous time (nonlinear) inequality constraints satisfaction, through regional convex hull approximation. RESAFE/COL is proven to be 5 times faster than multiple shooting and more tractable for embedded hardware without a decrease in the performance, nor accuracy and safety of the numerical solution. We validate our NMPC-CBF with RESAFE/COL on digital twins of the vehicle and the urban environment and show the safe controller's ability to improve crash avoidance by 91{\textbackslash}\%. Supplementary visual material can be found at https://youtu.be/\_EnbfYwljp4.},
  archiveprefix = {arXiv}
}

@inproceedings{althoffAvoidingGeometricIntersection2012,
  title = {Avoiding Geometric Intersection Operations in Reachability Analysis of Hybrid Systems},
  booktitle = {Proceedings of the 15th {{ACM}} International Conference on {{Hybrid Systems}}: {{Computation}} and {{Control}}},
  author = {Althoff, Matthias and Krogh, Bruce H.},
  year = {2012},
  month = apr,
  pages = {45--54},
  publisher = {ACM},
  address = {Beijing China},
  doi = {10.1145/2185632.2185643},
  url = {https://dl.acm.org/doi/10.1145/2185632.2185643},
  urldate = {2025-01-04},
  isbn = {978-1-4503-1220-2},
  langid = {english}
}

@misc{althoffCORA2025Manual2025,
  title = {{{CORA}} 2025 {{Manual}}},
  author = {Althoff, Matthias and Kochdumper, Niklas and Wetzlinger, Mark and Ladner, Tobias},
  year = {2025},
  url = {https://tumcps.github.io/CORA/data/archive/manual/Cora2025Manual.pdf}
}

@article{althoffSetPropagationTechniques2021,
  title = {Set {{Propagation Techniques}} for {{Reachability Analysis}}},
  author = {Althoff, Matthias and Frehse, Goran and Girard, Antoine},
  year = {2021},
  journal = {Annual Review of Control, Robotics, and Autonomous Systems},
  volume = {4},
  number = {1},
  pages = {369--395},
  doi = {10.1146/annurev-control-071420-081941},
  url = {https://doi.org/10.1146/annurev-control-071420-081941},
  urldate = {2022-08-11},
  abstract = {Reachability analysis consists in computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. It is a fundamental problem motivated by many applications in formal verification, controller synthesis, and estimation, to name only a few. This article focuses on a class of methods for computing a guaranteed overapproximation of the reachable set of continuous and hybrid systems, relying predominantly on set propagation; starting from the set of initial states, these techniques iteratively propagate a sequence of sets according to the system dynamics. After a review of set representation and computation, the article presents the state of the art of set propagation techniques for reachability analysis of linear, nonlinear, and hybrid systems. It ends with a discussion of successful applications of reachability analysis to real-world problems.}
}

@article{alurAutomaticSymbolicVerification1996,
  title = {Automatic Symbolic Verification of Embedded Systems},
  author = {Alur, R. and Henzinger, T.A. and Ho, Pei-Hsin},
  year = {1996},
  month = mar,
  journal = {IEEE Transactions on Software Engineering},
  volume = {22},
  number = {3},
  pages = {181--201},
  issn = {1939-3520},
  doi = {10.1109/32.489079},
  abstract = {Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.}
}

@article{amesControlBarrierFunction2017,
  title = {Control {{Barrier Function Based Quadratic Programs}} for {{Safety Critical Systems}}},
  author = {Ames, Aaron D. and Xu, Xiangru and Grizzle, Jessy W. and Tabuada, Paulo},
  year = {2017},
  month = aug,
  journal = {IEEE Transactions on Automatic Control},
  volume = {62},
  number = {8},
  pages = {3861--3876},
  issn = {1558-2523},
  doi = {10.1109/TAC.2016.2638961},
  url = {https://ieeexplore.ieee.org/document/7782377},
  urldate = {2023-12-19},
  abstract = {Safety critical systems involve the tight coupling between potentially conflicting control objectives and safety constraints. As a means of creating a formal framework for controlling systems of this form, and with a view toward automotive applications, this paper develops a methodology that allows safety conditions-expressed as control barrier functions-to be unified with performance objectives-expressed as control Lyapunov functions-in the context of real-time optimization-based controllers. Safety conditions are specified in terms of forward invariance of a set, and are verified via two novel generalizations of barrier functions; in each case, the existence of a barrier function satisfying Lyapunov-like conditions implies forward invariance of the set, and the relationship between these two classes of barrier functions is characterized. In addition, each of these formulations yields a notion of control barrier function (CBF), providing inequality constraints in the control input that, when satisfied, again imply forward invariance of the set. Through these constructions, CBFs can naturally be unified with control Lyapunov functions (CLFs) in the context of a quadratic program (QP); this allows for the achievement of control objectives (represented by CLFs) subject to conditions on the admissible states of the system (represented by CBFs). The mediation of safety and performance through a QP is demonstrated on adaptive cruise control and lane keeping, two automotive control problems that present both safety and performance considerations coupled with actuator bounds.}
}

@inproceedings{amesControlBarrierFunctions2019a,
  title = {Control {{Barrier Functions}}: {{Theory}} and {{Applications}}},
  shorttitle = {Control {{Barrier Functions}}},
  booktitle = {2019 18th {{European Control Conference}} ({{ECC}})},
  author = {Ames, Aaron D. and Coogan, Samuel and Egerstedt, Magnus and Notomista, Gennaro and Sreenath, Koushil and Tabuada, Paulo},
  year = {2019},
  month = jun,
  pages = {3420--3431},
  doi = {10.23919/ECC.2019.8796030},
  url = {https://ieeexplore.ieee.org/abstract/document/8796030?casa_token=sAXPypQOIBEAAAAA:ki7Ctazwen6t9151g7hQk5Hpc4Nc43ma5SYKG6JWF1Z1vUX3vqtUV7YkvLH4Pzix8pPv-DtJ1A},
  urldate = {2023-12-16},
  abstract = {This paper provides an introduction and overview of recent work on control barrier functions and their use to verify and enforce safety properties in the context of (optimization based) safety-critical controllers. We survey the main technical results and discuss applications to several domains including robotic systems.}
}

@inproceedings{anevlavisComputingControlledInvariant2019,
  title = {Computing Controlled Invariant Sets in Two Moves},
  booktitle = {2019 {{IEEE}} 58th {{Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Anevlavis, Tzanis and Tabuada, Paulo},
  year = {2019},
  month = dec,
  pages = {6248--6254},
  issn = {2576-2370},
  doi = {10.1109/CDC40024.2019.9029610},
  abstract = {In this paper we revisit the problem of computing controlled invariant sets for controllable discrete-time linear systems. We propose a novel algorithm that does not rely on iterative computations. Instead, controlled invariant sets are computed in two moves: 1) we lift the problem to a higher dimensional space where a controlled invariant set is computed in closed-form; 2) we project the resulting set back to the original domain to obtain the desired controlled invariant set. One of the advantages of the proposed method is the ability to handle larger systems.}
}

@book{baierPrinciplesModelChecking2008,
  title = {Principles of {{Model Checking}}},
  author = {Baier, Christel and Katoen, Joost-Pieter},
  year = {2008},
  month = apr,
  publisher = {MIT Press},
  address = {Cambridge, MA, USA},
  url = {https://mitpress.mit.edu/books/principles-model-checking},
  abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
  isbn = {978-0-262-02649-9},
  langid = {english}
}

@article{beltaFormalMethodsControl2019,
  title = {Formal {{Methods}} for {{Control Synthesis}}: {{An Optimization Perspective}}},
  shorttitle = {Formal {{Methods}} for {{Control Synthesis}}},
  author = {Belta, Calin and Sadraddini, Sadra},
  year = {2019},
  journal = {Annual Review of Control, Robotics, and Autonomous Systems},
  volume = {2},
  number = {1},
  pages = {115--140},
  doi = {10.1146/annurev-control-053018-023717},
  url = {https://doi.org/10.1146/annurev-control-053018-023717},
  urldate = {2022-10-10},
  abstract = {In control theory, complicated dynamics such as systems of (nonlinear) differential equations are controlled mostly to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimizing a certain cost along the trajectories of a stable system. In formal verification (model checking), simple systems, such as finite-state transition graphs that model computer programs or digital circuits, are checked against rich specifications given as formulas of temporal logics. The formal synthesis problem, in which the goal is to synthesize or control a finite system from a temporal logic specification, has recently received increased interest. In this article, we review some recent results on the connection between optimal control and formal synthesis. Specifically, we focus on the following problem: Given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification. We first provide a short overview of automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification. We then provide a detailed overview of a class of methods that rely on mapping the specification and the dynamics to constraints of an optimization problem. We discuss advantages and limitations of these two types of approaches and suggest directions for future research.}
}

@book{beltaFormalMethodsDiscreteTime2017,
  title = {Formal {{Methods}} for {{Discrete-Time Dynamical Systems}}},
  author = {Belta, Calin and Yordanov, Boyan and Gol, Ebru Aydin},
  year = {2017},
  month = mar,
  series = {Studies in {{Systems}}, {{Decision}} and {{Control}}},
  number = {89},
  publisher = {Springer},
  address = {New York, NY},
  url = {https://doi.org/10.1007/978-3-319-50763-7},
  abstract = {This book bridges fundamental gaps between control theory and formal methods. Although it focuses on discrete-time linear and piecewise affine systems, it also provides general frameworks for abstraction, analysis, and control of more general models.The book is self-contained, and while some mathematical knowledge is necessary, readers are not expected to have a background in formal methods or control theory. It rigorously defines concepts from formal methods, such as transition systems, temporal logics, model checking and synthesis. It then links these to the infinite state dynamical systems through abstractions that are intuitive and only require basic convex-analysis and control-theory terminology, which is provided in the appendix. Several examples and illustrations help readers understand and visualize the concepts introduced throughout the book.},
  isbn = {978-3-319-50762-0},
  langid = {english}
}

@inproceedings{bemporadOptimizationBasedVerificationStability2000,
  title = {Optimization-{{Based Verification}} and {{Stability Characterization}} of {{Piecewise Affine}} and {{Hybrid Systems}}},
  booktitle = {Hybrid {{Systems}}: {{Computation}} and {{Control}}},
  author = {Bemporad, Alberto and Torrisi, Fabio Danilo and Morari, Manfred},
  editor = {Lynch, Nancy and Krogh, Bruce H.},
  year = {2000},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {45--58},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/3-540-46430-1_8},
  abstract = {In this paper, we formulate the problem of characterizing the stability of a piecewise affine (PWA) system as a verification problem. The basic idea is to take the whole IRnas the set of initial conditions, and check that all the trajectories go to the origin. More precisely, we test for semi-global stability by restricting the set of initial conditions to an (arbitrarily large) bounded set X(0), and label as ``asymptotically stable in T steps'' the trajectories that enter an invariant set around the origin within a finite time T, or as ``unstable in T steps'' the trajectories which enter a set Xinstof (very large) states. Subsets of X(0) leading to none of the two previous cases are labeled as ``non-classifiable in T steps''. The domain of asymptotical stability in T steps is a subset of the domain of attraction of an equilibrium point, and has the practical meaning of collecting the initial conditions from which the settling time to a specified set around the origin is smaller than T. In addition, it can be computed algorithmically in finite time. Such an algorithm requires the computation of reach sets, in a similar fashion as what has been proposed for verification of hybrid systems. In this paper we present a substantial extension of the verification algorithm presented in [6] for stability characterization of PWA systems, based on linear and mixed-integer linear programming. As a result, given a set of initial conditions we are able to determine its partition into subsets of trajectories which are asymptotically stable, or unstable, or non-classifiable in T steps.},
  isbn = {978-3-540-46430-3},
  langid = {english}
}

@inproceedings{bemporadVerificationHybridSystems1999,
  title = {Verification of {{Hybrid Systems}} via {{Mathematical Programming}}},
  booktitle = {Hybrid {{Systems}}: {{Computation}} and {{Control}}},
  author = {Bemporad, Alberto and Morari, Manfred},
  editor = {Vaandrager, Frits W. and {van Schuppen}, Jan H.},
  year = {1999},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {31--45},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/3-540-48983-5_7},
  abstract = {This paper proposes a novel approach to the verification of hybrid systems based on linear and mixed-integer linear programming. Models are described using the Mixed Logical Dynamical (MLD) formalism introduced in [5]. The proposed technique is demonstrated on a verification case study for an automotive suspension system.},
  isbn = {978-3-540-48983-2},
  langid = {english}
}

@article{birdHybridZonotopesNew2023,
  title = {Hybrid Zonotopes: {{A}} New Set Representation for Reachability Analysis of Mixed Logical Dynamical Systems},
  shorttitle = {Hybrid Zonotopes},
  author = {Bird, Trevor J. and Pangborn, Herschel C. and Jain, Neera and Koeln, Justin P.},
  year = {2023},
  month = aug,
  journal = {Automatica},
  volume = {154},
  pages = {111107},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2023.111107},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109823002674},
  urldate = {2024-06-26},
  abstract = {This article presents a new set representation named the hybrid zonotope that is equivalent to the union of 2N constrained zonotopes -- convex polytopes -- through the addition of N binary zonotope factors. The major contribution of this manuscript is a closed-form solution for exact forward reachable sets of discrete-time, linear hybrid systems modeled as mixed logical dynamical systems. The proposed approach captures the worst-case exponential growth in the number of convex sets required to represent the nonconvex reachable set while exhibiting only linear growth in the complexity of the hybrid zonotope set representation. Redundancy removal techniques are provided that leverage binary trees to store the combinations of binary factors of the hybrid zonotope that map to nonempty convex subsets. Numerical examples show the hybrid zonotope's ability to compactly represent nonconvex reachable sets with an exponential number of features. Furthermore, the hybrid zonotope is shown to be closed under linear mappings, Minkowski sums, generalized intersections, and halfspace intersections.}
}

@misc{blackCBFKITControlBarrier2024,
  title = {{{CBFKIT}}: {{A Control Barrier Function Toolbox}} for {{Robotics Applications}}},
  shorttitle = {{{CBFKIT}}},
  author = {Black, Mitchell and Fainekos, Georgios and Hoxha, Bardh and Okamoto, Hideki and Prokhorov, Danil},
  year = {2024},
  month = apr,
  number = {arXiv:2404.07158},
  eprint = {2404.07158},
  publisher = {arXiv},
  doi = {10.48550/arXiv.2404.07158},
  url = {http://arxiv.org/abs/2404.07158},
  urldate = {2024-10-20},
  abstract = {This paper introduces CBFKit, a Python/ROS toolbox for safe robotics planning and control under uncertainty. The toolbox provides a general framework for designing control barrier functions for mobility systems within both deterministic and stochastic environments. It can be connected to the ROS open-source robotics middleware, allowing for the setup of multi-robot applications, encoding of environments and maps, and integrations with predictive motion planning algorithms. Additionally, it offers multiple CBF variations and algorithms for robot control. The CBFKit is demonstrated on the Toyota Human Support Robot (HSR) in both simulation and in physical experiments.},
  archiveprefix = {arXiv}
}

@article{blanchiniSetInvarianceControl1999,
  title = {Set Invariance in Control},
  author = {Blanchini, F.},
  year = {1999},
  month = nov,
  journal = {Automatica},
  volume = {35},
  number = {11},
  pages = {1747--1767},
  issn = {0005-1098},
  doi = {10.1016/S0005-1098(99)00113-2},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109899001132},
  urldate = {2021-04-08},
  abstract = {The properties of positively invariant sets are involved in many different problems in control theory, such as constrained control, robustness analysis, synthesis and optimization. In this paper we provide an overview of the literature concerning positively invariant sets and their application to the analysis and synthesis of control systems.},
  langid = {english}
}

@inproceedings{bogomolovCaseStudyReachability2020,
  title = {Case {{Study}}: {{Reachability}} and {{Scalability}} in a {{Unified Combat-Command-and-Control Model}}},
  shorttitle = {Case {{Study}}},
  booktitle = {Reachability {{Problems}}},
  author = {Bogomolov, Sergiy and Forets, Marcelo and Potomkin, Kostiantyn},
  editor = {Schmitz, Sylvain and Potapov, Igor},
  year = {2020},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {52--66},
  publisher = {Springer International Publishing},
  address = {Cham},
  doi = {10.1007/978-3-030-61739-4_4},
  abstract = {Reachability analysis computes an envelope encompassing the reachable states of a hybrid automaton within a given time horizon. It is known to be a computationally intensive task. In this case study paper, we consider the application of reachability analysis on a mathematical model unifying two key warfighting functions: Combat, and Command-and-Control (C2). Reachability here has a meaning of whether, given a range of initial combat forces and a C2 network and various uncertainties, one side can survive combat with intact forces while the adversary is diminished to zero. These are questions which arise in military Operations Research (OR). This paper is the first to utilize the notions of a hybrid automaton and reachability analysis in the area of OR. We explore the applicability and scalability of Taylor-model based reachability techniques in this domain. Our experiments demonstrate the potential of reachability analysis in the context of OR.},
  isbn = {978-3-030-61739-4},
  langid = {english}
}

@article{braunCommentStabilizationGuaranteed2020,
  title = {Comment on ``{{Stabilization}} with Guaranteed Safety Using {{Control Lyapunov}}--{{Barrier Function}}''},
  author = {Braun, Philipp and Kellett, Christopher M.},
  year = {2020},
  month = dec,
  journal = {Automatica},
  volume = {122},
  pages = {109225},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2020.109225},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109820304234},
  urldate = {2023-12-21},
  abstract = {Recently, Romdlony and Jayawardhana (2016) proposed control Lyapunov--Barrier functions (CLBFs) for the stabilization of nonlinear control systems while avoiding a bounded set of unsafe states. We demonstrate that CLBFs used in Romdlony and Jayawardhana (2016, Prop. 3 and 5) cannot exist. Critically, this implies that the examples discussed in Romdlony and Jayawardhana (2016) do not satisfy the stated assumptions on CLBFs.}
}

@book{clarkeHandbookModelChecking2018,
  title = {Handbook of {{Model Checking}}},
  editor = {Clarke, Edmund M. and Henzinger, Thomas A. and Veith, Helmut and Bloem, Roderick},
  year = {2018},
  publisher = {Springer},
  address = {Cham},
  url = {https://doi.org/10.1007/978-3-319-10575-8},
  isbn = {978-3-319-10574-1},
  langid = {english}
}

@book{clarkeModelChecking2018,
  title = {Model {{Checking}}},
  author = {Clarke, Edmund M. and Jr and Grumberg, Orna and Kroening, Daniel and Peled, Doron and Veith, Helmut},
  editor = {Belta, Calin},
  year = {2018},
  month = dec,
  series = {Cyber {{Physical Systems Series}}},
  edition = {2},
  publisher = {MIT Press},
  address = {Cambridge, MA, USA},
  url = {https://mitpress.mit.edu/9780262038836/model-checking/},
  abstract = {An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems.},
  isbn = {978-0-262-03883-6},
  langid = {english}
}

@article{fanControllerSynthesisLinear2022,
  title = {Controller {{Synthesis}} for {{Linear System With Reach-Avoid Specifications}}},
  author = {Fan, Chuchu and Qin, Zengyi and Mathur, Umang and Ning, Qiang and Mitra, Sayan and Viswanathan, Mahesh},
  year = {2022},
  month = apr,
  journal = {IEEE Transactions on Automatic Control},
  volume = {67},
  number = {4},
  pages = {1713--1727},
  issn = {1558-2523},
  doi = {10.1109/TAC.2021.3069723},
  abstract = {We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Discrete abstraction-based controller synthesis techniques have been developed for linear and nonlinear systems with various types of specifications. However, these methods typically suffer from the state space explosion problem. Our solution decomposes the overall synthesis problem into two smaller, and more tractable problems: one synthesis problem for an open-loop controller, which can produce a reference trajectory, and a second for synthesizing a tracking controller, which can enforce the other trajectories to follow the reference trajectory. As a key building-block result, we show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be overapproximated by a sequence of ellipsoids, with shapes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Moreover, we are able to reduce the problem of synthesizing open-loop controllers to satisfiability problems over quantifier-free linear real arithmetic. The number of linear constraints in the satisfiability problem is linear to the number of hyperplanes as the surfaces of the polytopic obstacles and goal sets. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We implement this synthesis algorithm in a tool RealSyn ver 2.0 and use it on several benchmarks with up to 20 dimensions. Experiment results are very promising: RealSyn ver 2.0 can find controllers for most of the benchmarks in seconds.}
}

@inproceedings{fehnkerBenchmarksHybridSystems2004,
  title = {Benchmarks for {{Hybrid Systems Verification}}},
  booktitle = {Hybrid {{Systems}}: {{Computation}} and {{Control}}},
  author = {Fehnker, Ansgar and Ivan{\v c}i{\'c}, Franjo},
  editor = {Goos, Gerhard and Hartmanis, Juris and Van Leeuwen, Jan and Alur, Rajeev and Pappas, George J.},
  year = {2004},
  volume = {2993},
  pages = {326--341},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-24743-2_22},
  url = {http://link.springer.com/10.1007/978-3-540-24743-2_22},
  urldate = {2023-12-19},
  abstract = {There are numerous application examples for hybrid systems verification in recent literature. Most of them were introduced to illustrate a new approach to hybrid systems verification, and are therefore of a limited size. Others are case studies that serve to prove that an approach can be applied to real world problems. Verification of these typically requires a lot of domain experience to obtain a tractable, verifiable model. Verification of a case study yields a singular result that is hard to compare and time-consuming to reproduce.},
  isbn = {978-3-540-21259-1 978-3-540-24743-2},
  langid = {english}
}

@book{garocheFormalVerificationControl2019,
  title = {Formal {{Verification}} of {{Control System Software}}},
  author = {Garoche, Pierre-Lo{\"i}c},
  year = {2019},
  series = {Princeton {{Series}} in {{Applied Mathematics}}},
  publisher = {Princeton University Press},
  url = {https://press.princeton.edu/books/hardcover/9780691181301/formal-verification-of-control-system-software},
  urldate = {2022-12-22},
  abstract = {An essential introduction to the analysis and verification of control system software},
  isbn = {978-0-691-18130-1},
  langid = {english}
}

@book{GuideProjectManagement2021,
  title = {A {{Guide}} to the {{Project Management Body}} of {{Knowledge}} ({{PMBOK}}{\textregistered} {{Guide}})},
  year = {2021},
  edition = {7},
  publisher = {Project Management Institute},
  url = {https://www.pmi.org/pmbok-guide-standards/foundational/PMBOK}
}

@inproceedings{henzingerHyTechModelChecker1997,
  title = {{{HyTech}}: {{A}} Model Checker for Hybrid Systems},
  shorttitle = {{{HyTech}}},
  booktitle = {Computer {{Aided Verification}}},
  author = {Henzinger, Thomas A. and Ho, Pei-Hsin and {Wong-Toi}, Howard},
  editor = {Grumberg, Orna},
  year = {1997},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {460--463},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/3-540-63166-6_48},
  abstract = {A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.},
  isbn = {978-3-540-69195-2},
  langid = {english}
}

@misc{chanVerifyingSafetyAutonomous2017,
  title = {Verifying Safety of an Autonomous Spacecraft Rendezvous Mission},
  author = {Chan, Nicole and Mitra, Sayan},
  year = {2017},
  month = mar,
  number = {arXiv:1703.06930},
  eprint = {1703.06930},
  primaryclass = {cs},
  publisher = {arXiv},
  doi = {10.48550/arXiv.1703.06930},
  url = {http://arxiv.org/abs/1703.06930},
  urldate = {2025-01-04},
  abstract = {A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of constraints in each discrete mode. A switched LQR controller is designed accordingly to meet this collection of physical and geometric safety constraints, while maintaining liveness in navigating toward the target spacecraft. We extend this benchmark problem to check for passive safety, which is collision avoidance along a passive, propulsion-free trajectory that may be followed in the event of system failures. We show that existing hybrid verification tools like SpaceEx, C2E2, and our own implementation of a simulation-driven verification tool can robustly verify this system with respect to the requirements, and a variety of relevant initial conditions.},
  archiveprefix = {arXiv}
}

@techreport{iecFunctionalSafetyElectrical2010,
  type = {International {{Standard}}},
  title = {Functional Safety of Electrical/Electronic/Programmable Electronic Safety-Related Systems - {{Parts}} 1 to 7},
  author = {{IEC}},
  year = {2010},
  month = apr,
  number = {IEC 61508:2010 CMV},
  institution = {IEC},
  url = {https://webstore.iec.ch/publication/22273},
  urldate = {2022-08-26}
}

@inproceedings{jiangEnsuringSafetyVehicle2020,
  title = {Ensuring Safety for Vehicle Parking Tasks Using {{Hamilton-Jacobi}} Reachability Analysis},
  booktitle = {2020 59th {{IEEE Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Jiang, Frank J. and Gao, Yulong and Xie, Lihua and Johansson, Karl H.},
  year = {2020},
  month = dec,
  pages = {1416--1421},
  issn = {2576-2370},
  doi = {10.1109/CDC42340.2020.9304186},
  url = {https://ieeexplore.ieee.org/abstract/document/9304186?casa_token=oQJ0a128K6cAAAAA:NvYeDrlgwclQCnkicvFEqtvFEaR6BgayU_8KJihb7IjTNkH8Y7kQwHDBLSa9vVfnaEOp-sk8Uoo},
  urldate = {2024-06-26},
  abstract = {In this paper, we propose an approach for ensuring the safety of a vehicle throughout a parking task, even when the vehicle is being operated at varying levels of automation. We start by specifying a vehicle parking task using linear temporal logic formulae that can be model checked for feasibility. The model-checking is facilitated by the construction of a temporal logic tree via Hamilton-Jacobi reachability analysis. Once we know the parking task is feasible for our vehicle model, we utilize the constructed temporal logic tree to directly synthesize control sets. Our approach synthesizes control sets that are least-restrictive in the context of the specification, since they permit any control inputs that are guaranteed not to violate the specification. This least-restrictive characteristic allows for the application of our approach to vehicles under different modes of operation (e.g., human-in-the-loop shared autonomy or fully-automated schemes). Implementing in both simulation and on hardware, we demonstrate the approach's potential for ensuring the safety of vehicles throughout parking tasks, whether they are operated by humans or automated driving systems.}
}

@article{kordaComputingControlledInvariant2020,
  title = {Computing {{Controlled Invariant Sets}} from {{Data Using Convex Optimization}}},
  author = {Korda, Milan},
  year = {2020},
  month = jan,
  journal = {SIAM Journal on Control and Optimization},
  volume = {58},
  number = {5},
  pages = {2871--2899},
  publisher = {{Society for Industrial and Applied Mathematics}},
  issn = {0363-0129},
  doi = {10.1137/19M1305835},
  url = {https://epubs.siam.org/doi/abs/10.1137/19M1305835},
  urldate = {2021-04-08},
  abstract = {This work presents a data-driven method for approximation of the maximum positively invariant (MPI) set and the maximum controlled invariant (MCI) set for nonlinear dynamical systems. The method only requires knowledge of a finite collection of one-step transitions of the discrete-time dynamics, without the requirement of segments of trajectories or the control inputs that effected the transitions to be available. The approach uses a novel characterization of the MPI and MCI sets as the solution to an infinite-dimensional linear programming (LP) problem in the space of continuous functions, with the optimum being attained by a (Lipschitz) continuous function under mild assumptions. The infinite-dimensional LP is then approximated by restricting the decision variable to a finite-dimensional subspace and by imposing the nonnegativity constraint of this LP only on the available data samples. This leads to a single finite-dimensional LP that can be easily solved using off-the-shelf solvers. We analyze the convergence rate and sample complexity, proving probabilistic as well as hard guarantees on the volume error of the approximations. The approach is very general, requiring minimal underlying assumptions. In particular, the dynamics is not required to be polynomial or even continuous (forgoing some of the theoretical results). Detailed numerical examples up to state-space dimension 10 with code available online demonstrate the method.}
}

@article{kordaConvexComputationMaximum2014,
  title = {Convex {{Computation}} of the {{Maximum Controlled Invariant Set For Polynomial Control Systems}}},
  author = {Korda, Milan and Henrion, Didier and Jones, Colin N.},
  year = {2014},
  month = jan,
  journal = {SIAM Journal on Control and Optimization},
  volume = {52},
  number = {5},
  pages = {2944--2969},
  publisher = {{Society for Industrial and Applied Mathematics}},
  issn = {0363-0129},
  doi = {10.1137/130914565},
  url = {https://epubs.siam.org/doi/abs/10.1137/130914565},
  urldate = {2021-04-08},
  abstract = {We characterize the maximum controlled invariant (MCI) set for discrete- as well as continuous-time nonlinear dynamical systems as the solution of an infinite-dimensional linear programming problem. For systems with polynomial dynamics and compact semialgebraic state and control constraints, we describe a hierarchy of finite-dimensional linear matrix inequality (LMI) relaxations whose optimal values converge to the volume of the MCI set; dual to these LMI relaxations are sum-of-squares (SOS) problems providing a converging sequence of outer approximations to the MCI set. The approach is simple and readily applicable in the sense that the approximations are the outcome of a single semidefinite program with no additional input apart from the problem description. A number of numerical examples illustrate the approach.}
}

@article{kordaStabilityPerformanceVerification2022a,
  title = {Stability and {{Performance Verification}} of {{Dynamical Systems Controlled}} by {{Neural Networks}}: {{Algorithms}} and {{Complexity}}},
  shorttitle = {Stability and {{Performance Verification}} of {{Dynamical Systems Controlled}} by {{Neural Networks}}},
  author = {Korda, Milan},
  year = {2022},
  journal = {IEEE Control Systems Letters},
  volume = {6},
  pages = {3265--3270},
  issn = {2475-1456},
  doi = {10.1109/LCSYS.2022.3181806},
  url = {https://ieeexplore.ieee.org/document/9792308},
  urldate = {2023-12-08},
  abstract = {This letter makes several contributions on stability and performance verification of nonlinear dynamical systems controlled by neural networks. First, we show that the stability and performance of a polynomial dynamical system controlled by a neural network with semialgebraically representable activation functions (e.g., ReLU) can be certified by convex semidefinite programming. The result is based on the fact that the semialgebraic representation of the activation functions and polynomial dynamics allows one to search for a Lyapunov function using polynomial sum-of-squares methods. Second, we remark that even in the case of a linear system controlled by a neural network with ReLU activation functions, the problem of verifying asymptotic stability is undecidable. Finally, under additional assumptions, we establish a converse result on the existence of a polynomial Lyapunov function for this class of systems. Numerical results with code available online on examples of state-space dimension up to 50 and neural networks with several hundred neurons and up to 30 layers demonstrate the method.}
}

@misc{kousikEllipsotopesCombiningEllipsoids2022,
  title = {Ellipsotopes: {{Combining Ellipsoids}} and {{Zonotopes}} for {{Reachability Analysis}} and {{Fault Detection}}},
  shorttitle = {Ellipsotopes},
  author = {Kousik, Shreyas and Dai, Adam and Gao, Grace},
  year = {2022},
  month = jun,
  number = {arXiv:2108.01750},
  eprint = {2108.01750},
  primaryclass = {cs, eess},
  publisher = {arXiv},
  doi = {10.48550/arXiv.2108.01750},
  url = {http://arxiv.org/abs/2108.01750},
  urldate = {2024-06-26},
  abstract = {Ellipsoids are a common representation for reachability analysis, because they can be transformed efficiently under affine maps, and allow conservative approximation of Minkowski sums, which let one incorporate uncertainty and linearization error in a dynamical system by expanding the size of the reachable set. Zonotopes, a type of symmetric, convex polytope, are similarly frequently used due to efficient numerical implementation of affine maps and exact Minkowski sums. Both of these representations also enable efficient, convex collision detection for fault detection or formal verification tasks, wherein one checks if the reachable set of a system collides (i.e., intersects) with an unsafe set. However, both representations often result in conservative representations for reachable sets of arbitrary systems, and neither is closed under intersection. Recently, representations such as constrained zonotopes and constrained polynomial zonotopes have been shown to overcome some of these conservativeness challenges, and are closed under intersection. However, constrained zonotopes can not represent shapes with smooth boundaries such as ellipsoids, and constrained polynomial zonotopes can require solving a non-convex program for collision checking or fault detection. This paper introduces ellipsotopes, a set representation that is closed under affine maps, Minkowski sums, and intersections. Ellipsotopes combine the advantages of ellipsoids and zonotopes while ensuring convex collision checking. The utility of this representation is demonstrated on several examples.},
  archiveprefix = {arXiv}
}

@article{kvasnicaReachabilityAnalysisControl2015,
  title = {Reachability {{Analysis}} and {{Control Synthesis}} for {{Uncertain Linear Systems}} in {{MPT}}},
  author = {Kvasnica, Michal and Tak{\'a}cs, B{\'a}lint and Holaza, Juraj and Ingole, Deepak},
  year = {2015},
  month = jan,
  journal = {IFAC-PapersOnLine},
  series = {8th {{IFAC Symposium}} on {{Robust Control Design ROCOND}} 2015},
  volume = {48},
  number = {14},
  pages = {302--307},
  issn = {2405-8963},
  doi = {10.1016/j.ifacol.2015.09.474},
  url = {https://www.sciencedirect.com/science/article/pii/S2405896315015931},
  urldate = {2023-12-19},
  abstract = {Software tools play an important dissemination role by bringing cutting-edge theoretical algorithms into the hands of researchers and practitioners. This paper introduces a new robust analysis and control module of the Multi-Parametric toolbox, which is one of the most successful open-source tools in the field. We discuss how robust reachable and invariant sets can be computed using a convenient user interface. Such sets play an important role in many control-oriented tasks, such as in design of recursively feasible optimization-based control laws. Moreover, the new module also allows to synthesize robustly stabilizing linear controller and, more importantly, offers robust Model Predictive Control (MPC) synthesis features. The main aim of the paper is illustrate how complex tasks can be implemented using simple operators such that more sophisticated algorithms could be developed easily by the research community.}
}

@techreport{lagerbergBenchmarkHybridControl2007,
  title = {A {{Benchmark}} on {{Hybrid Control}} of an {{Automotive Powertrain}} with {{Backlash}}},
  author = {Lagerberg, Adam},
  year = {2007},
  number = {R005},
  address = {Goteborg, Sweden},
  institution = {Chalmers University of Technology},
  url = {https://www.researchgate.net/profile/Adam-Lagerberg/publication/251989348_A_Benchmark_on_Hybrid_Control_of_an_Automotive_Powertrain_with_Backlash/links/555ef93708ae86c06b5f685c/A-Benchmark-on-Hybrid-Control-of-an-Automotive-Powertrain-with-Backlash.pdf},
  abstract = {In automotive powertrains, the existence of backlash causes driveability problems, which to some extent are remedied by the engine control system. The control problem has a con- strained, minimum-time character, and a powertrain model including the backlash nonlinear- ity will be of a hybrid character. This motivates an investig ation of the usability of a hybrid control synthesis method for this problem. This document outlines a benchmark problem for this system, and a few simulation results are included to indicate how a solution may look. These simulations were produced with an explicit MPC controller.}
}

@article{legatGeometricControlAlgebraic2021,
  title = {Geometric Control of Algebraic Systems},
  author = {Legat, Beno{\^i}t and Jungers, Rapha{\"e}l M.},
  year = {2021},
  month = jan,
  journal = {arXiv:2101.06990 [math]},
  eprint = {2101.06990},
  primaryclass = {math},
  url = {http://arxiv.org/abs/2101.06990},
  urldate = {2021-04-08},
  abstract = {In this paper, we present a geometric approach for computing the controlled invariant set of a continuous-time control system. While the problem is well studied for in the ellipsoidal case, this family is quite conservative for constrained or switched linear systems. We reformulate the invariance of a set as an inequality for its support function that is valid for any convex set. This produces novel algebraic conditions for the invariance of sets with polynomial or piecewise quadratic support function. We compare it with the common algebraic approach for polynomial sublevel sets and show that it is significantly more conservative than our method.},
  archiveprefix = {arXiv}
}

@article{legatPiecewiseSemiEllipsoidalControl2021,
  title = {Piecewise {{Semi-Ellipsoidal Control Invariant Sets}}},
  author = {Legat, B. and Rakovi{\'c}, S. V. and Jungers, R. M.},
  year = {2021},
  month = jul,
  journal = {IEEE Control Systems Letters},
  volume = {5},
  number = {3},
  pages = {755--760},
  issn = {2475-1456},
  doi = {10.1109/LCSYS.2020.3005326},
  abstract = {Computing control invariant sets is paramount in many applications. The families of sets commonly used for computations are ellipsoids and polyhedra. However, searching for a control invariant set over the family of ellipsoids is conservative for systems more complex than unconstrained linear time invariant systems. Moreover, even if the control invariant set may be approximated arbitrarily closely by polyhedra, the complexity of the polyhedra may grow rapidly in certain directions. An attractive generalization of these two families are piecewise semi-ellipsoids. We provide in this letter a convex programming approach for computing control invariant sets of this family.}
}

@article{legatSumofSquaresMethodsControlled2020,
  title = {Sum-of-{{Squares}} Methods for Controlled Invariant Sets with Applications to Model-Predictive Control},
  author = {Legat, Beno{\^i}t and Tabuada, Paulo and Jungers, Rapha{\"e}l M.},
  year = {2020},
  month = may,
  journal = {Nonlinear Analysis: Hybrid Systems},
  volume = {36},
  pages = {100858},
  issn = {1751-570X},
  doi = {10.1016/j.nahs.2020.100858},
  url = {https://www.sciencedirect.com/science/article/pii/S1751570X20300054},
  urldate = {2021-04-08},
  abstract = {We develop a method for computing controlled invariant sets of discrete-time affine systems using Sum-of-Squares programming. We apply our method to the controller design problem for switching affine systems with polytopic safe sets but our work also improves the state of the art for the particular case of LTI systems. The task is reduced to a semidefinite programming problem by enforcing an invariance relation in the dual space of the geometric problem. The paper ends with an application to safety critical model predictive control.},
  langid = {english}
}

@phdthesis{leguernicReachabilityAnalysisHybrid2009,
  title = {Reachability {{Analysis}} of {{Hybrid Systems}} with {{Linear Continuous Dynamics}}},
  author = {Le Guernic, Colas},
  year = {2009},
  address = {Grenoble, France},
  url = {https://theses.hal.science/tel-00422569/},
  abstract = {This thesis is devoted to the problem of computing reachable sets of linear and hybrid systems. In the first part, after exposing existing approaches for reachability analysis of linear systems, we present the main contribution of the thesis: a new algorithmic scheme for linear time-invariant systems that definitely outperforms existing algorithms. As the exact implementation furnishes a representation of the reachable sets that is sometimes hard to manipulate, we propose an approximate version that is not subject to the wrapping effect, an uncontrolled growth of the approximation errors. We also discuss a variant of this algorithm specialized to support functions, a functional representation of convex sets. In the second part, we extend this work to hybrid systems. We first show how to deal with the constraints on the continuous dynamics imposed by the invariants. Then, we present algorithms for approximating the intersection of the continuous reachable sets with hyperplanar guards.},
  langid = {english},
  school = {Universit{\'e} Grenoble I -- Joseph-Fourier}
}

@article{maghenemSufficientConditionsForward2021,
  title = {Sufficient Conditions for Forward Invariance and Contractivity in Hybrid Inclusions Using Barrier Functions},
  author = {Maghenem, Mohamed and Sanfelice, Ricardo G.},
  year = {2021},
  month = feb,
  journal = {Automatica},
  volume = {124},
  pages = {109328},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2020.109328},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109820305288},
  urldate = {2023-12-19},
  abstract = {This paper studies set invariance and contractivity in hybrid systems modeled by hybrid inclusions using barrier functions. After introducing the notion of barrier function, we investigate sufficient conditions to guarantee different forward invariance and contractivity notions of a closed set for hybrid systems with nonuniqueness of solutions and solutions terminating prematurely. We consider forward (pre-)invariance of sets, which guarantees that the maximal solutions starting from the set stay in it, and (pre-)contractivity, which further requires that the solutions starting from the boundary of the set evolve immediately (continuously or discretely) towards its interior. Our conditions for forward invariance and contractivity are infinitesimal and in terms of the proposed barrier functions. Examples illustrate the results.}
}

@phdthesis{majumdarRobustOnlineMotion2013,
  type = {{{MSc}}. Thesis},
  title = {Robust {{Online Motion Planning}} with {{Reachable Sets}}},
  author = {Majumdar, Anirudha},
  year = {2013},
  month = jun,
  address = {Cambridge},
  url = {http://groups.csail.mit.edu/robotics-center/public_papers/Majumdar13f.pdf},
  school = {MIT}
}

@mastersthesis{michaloglouSystemsVerificationUsing2020,
  title = {Systems {{Verification}} Using {{Barrier Certificates}}},
  author = {Michaloglou, Alkmini},
  year = {2020},
  month = feb,
  address = {Thessaloniki, Grece},
  url = {http://ikee.lib.auth.gr/record/319548/files/GRI-2020-27465.pdf},
  langid = {english},
  school = {Aristotle University of Thessaloniki}
}

@book{mitraVerifyingCyberPhysicalSystems2021,
  title = {Verifying {{Cyber-Physical Systems}}: {{A Path}} to {{Safe Autonomy}}},
  shorttitle = {Verifying {{Cyber-Physical Systems}}},
  author = {Mitra, Sayan},
  editor = {Belta, Calin},
  year = {2021},
  month = feb,
  series = {Cyber {{Physical Systems Series}}},
  publisher = {MIT Press},
  address = {Cambridge, MA, USA},
  url = {https://sayanmitracode.github.io/cpsbooksite/about.html},
  abstract = {A graduate-level textbook that presents a unified mathematical framework for modeling and analyzing cyber-physical systems, with a strong focus on verification.},
  isbn = {978-0-262-04480-6},
  langid = {english}
}

@book{pageEssentialLogicComputer2019,
  title = {Essential {{Logic}} for {{Computer Science}}},
  author = {Page, Rex and Gamboa, Ruben},
  year = {2019},
  month = jan,
  publisher = {The MIT Press},
  address = {Cambridge, MA ; London, England},
  url = {https://mitpress.mit.edu/9780262039185/essential-logic-for-computer-science/},
  abstract = {An introduction to applying predicate logic to testing and verification of software and digital circuits that focuses on applications rather than theory. Computer scientists use logic for testing and verification of software and digital circuits, but many computer science students study logic only in the context of traditional mathematics, encountering the subject in a few lectures and a handful of problem sets in a discrete math course. This book offers a more substantive and rigorous approach to logic that focuses on applications in computer science. Topics covered include predicate logic, equation-based software, automated testing and theorem proving, and large-scale computation. Formalism is emphasized, and the book employs three formal notations: traditional algebraic formulas of propositional and predicate logic; digital circuit diagrams; and the widely used partially automated theorem prover, ACL2, which provides an accessible introduction to mechanized formalism. For readers who want to see formalization in action, the text presents examples using Proof Pad, a lightweight ACL2 environment. Readers will not become ALC2 experts, but will learn how mechanized logic can benefit software and hardware engineers. In addition, 180 exercises, some of them extremely challenging, offer opportunities for problem solving. There are no prerequisites beyond high school algebra. Programming experience is not required to understand the book's equation-based approach. The book can be used in undergraduate courses in logic for computer science and introduction to computer science and in math courses for computer science students.},
  isbn = {978-0-262-03918-5},
  langid = {english}
}

@article{prajnaBarrierCertificatesNonlinear2006,
  title = {Barrier Certificates for Nonlinear Model Validation},
  author = {Prajna, Stephen},
  year = {2006},
  month = jan,
  journal = {Automatica},
  volume = {42},
  number = {1},
  pages = {117--126},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2005.08.007},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109805002839},
  urldate = {2022-08-12},
  abstract = {Methods for model validation of continuous-time nonlinear systems with uncertain parameters are presented in this paper. The methods employ functions of state-parameter-time, termed barrier certificates, whose existence proves that a model and a feasible parameter set are inconsistent with some time-domain experimental data. A very large class of models can be treated within this framework; this includes differential-algebraic models, models with memoryless/dynamic uncertainties, and hybrid models. Construction of barrier certificates can be performed by convex optimization, utilizing recent results on the sum of squares decomposition of multivariate polynomials.},
  langid = {english}
}

@article{prajnaFrameworkWorstCaseStochastic2007,
  title = {A {{Framework}} for {{Worst-Case}} and {{Stochastic Safety Verification Using Barrier Certificates}}},
  author = {Prajna, Stephen and Jadbabaie, Ali and Pappas, George J.},
  year = {2007},
  month = aug,
  journal = {IEEE Transactions on Automatic Control},
  volume = {52},
  number = {8},
  pages = {1415--1428},
  issn = {1558-2523},
  doi = {10.1109/TAC.2007.902736},
  abstract = {This paper presents a methodology for safety verification of continuous and hybrid systems in the worst-case and stochastic settings. In the worst-case setting, a function of state termed barrier certificate is used to certify that all trajectories of the system starting from a given initial set do not enter an unsafe region. No explicit computation of reachable sets is required in the construction of barrier certificates, which makes it possible to handle nonlinearity, uncertainty, and constraints directly within this framework. In the stochastic setting, our method computes an upper bound on the probability that a trajectory of the system reaches the unsafe set, a bound whose validity is proven by the existence of a barrier certificate. For polynomial systems, barrier certificates can be constructed using convex optimization, and hence the method is computationally tractable. Some examples are provided to illustrate the use of the method.}
}

@phdthesis{prajnaOptimizationBasedMethodsNonlinear2005,
  title = {Optimization-{{Based Methods}} for {{Nonlinear}} and {{Hybrid Systems Verification}}},
  author = {Prajna, Stephen},
  year = {2005},
  address = {Pasadena, California},
  doi = {10.7907/S3BJ-4M47},
  url = {https://resolver.caltech.edu/CaltechETD:etd-05272005-144358},
  urldate = {2022-08-12},
  abstract = {Complex behaviors that can be exhibited by hybrid systems make the verification of such systems both important and challenging. Due to the infinite number of possibilities taken by the continuous state and the uncertainties in the system, exhaustive simulation is impossible, and also computing the set of reachable states is generally intractable. Nevertheless, the ever-increasing presence of hybrid systems in safety critical applications makes it evident that verification is an issue that has to be addressed. In this thesis, we develop a unified methodology for verifying temporal properties of continuous and hybrid systems. Our framework does not require explicit computation of reachable states. Instead, functions of state termed barrier certificates and density functions are used in conjunction with deductive inference to prove properties such as safety, reachability, eventuality, and their combinations. As a consequence, the proposed methods are directly applicable to systems with nonlinearity, uncertainty, and constraints. Moreover, it is possible to treat safety verification of stochastic systems in a similar fashion, by computing an upper-bound on the probability of reaching the unsafe states. We formulate verification using barrier certificates and density functions as convex programming problems. For systems with polynomial descriptions, sum of squares optimization can be used to construct polynomial barrier certificates and density functions in a computationally scalable manner. Some examples are presented to illustrate the use of the methods. At the end, the convexity of the problem formulation is also exploited to prove a converse theorem in safety verification using barrier certificates.},
  copyright = {other},
  langid = {english},
  school = {California Institute of Technology}
}

@inproceedings{prajnaSafetyVerificationHybrid2004,
  title = {Safety {{Verification}} of {{Hybrid Systems Using Barrier Certificates}}},
  booktitle = {Hybrid {{Systems}}: {{Computation}} and {{Control}}},
  author = {Prajna, Stephen and Jadbabaie, Ali},
  editor = {Alur, Rajeev and Pappas, George J.},
  year = {2004},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {477--492},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-24743-2_32},
  abstract = {This paper presents a novel methodology for safety verification of hybrid systems. For proving that all trajectories of a hybrid system do not enter an unsafe region, the proposed method uses a function of state termed a barrier certificate. The zero level set of a barrier certificate separates the unsafe region from all possible trajectories starting from a given set of initial conditions, hence providing an exact proof of system safety. No explicit computation of reachable sets is required in the construction of barrier certificates, which makes nonlinearity, uncertainty, and constraints can be handled directly within this framework. The method is also computationally tractable, since barrier certificates can be constructed using the sum of squares decomposition and semidefinite programming. Some examples are provided to illustrate the use of the method.},
  isbn = {978-3-540-24743-2},
  langid = {english}
}

@article{ratschanConverseTheoremsSafety2018,
  title = {Converse {{Theorems}} for {{Safety}} and {{Barrier Certificates}}},
  author = {Ratschan, Stefan},
  year = {2018},
  month = aug,
  journal = {IEEE Transactions on Automatic Control},
  volume = {63},
  number = {8},
  pages = {2628--2632},
  issn = {1558-2523},
  doi = {10.1109/TAC.2018.2792325},
  url = {https://ieeexplore.ieee.org/abstract/document/8253819},
  urldate = {2023-12-19},
  abstract = {An important tool for proving the safety of dynamical systems is the notion of a barrier certificate. In this paper, we prove that every robustly safe ordinary differential equation has a barrier certificate. Moreover, we show a construction of such a barrier certificate based on a set of states that is reachable in finite time.}
}

@article{romdlonyStabilizationGuaranteedSafety2016,
  title = {Stabilization with Guaranteed Safety Using {{Control Lyapunov}}--{{Barrier Function}}},
  author = {Romdlony, Muhammad Zakiyullah and Jayawardhana, Bayu},
  year = {2016},
  month = apr,
  journal = {Automatica},
  volume = {66},
  pages = {39--47},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2015.12.011},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109815005439},
  urldate = {2023-12-21},
  abstract = {We propose a novel nonlinear control method for solving the problem of stabilization with guaranteed safety for nonlinear systems. The design is based on the merging of the well-known Control Lyapunov Function (CLF) and the recent concept of Control Barrier Function (CBF). The proposed control method allows us to combine the design of a stabilizing feedback law based on CLF and the design of safety control based on CBF(s); both of which can be designed independently. Our proposed approach can also accommodate the case of multiple CBFs which correspond to multiple different sets of unsafe states. Lastly, the efficacy of the proposed approach is demonstrated in the simulation results on the stabilization of a nonlinear mechanical system and on the navigation of a mobile robot.}
}

@inproceedings{romdlonyUnitingControlLyapunov2014,
  title = {Uniting {{Control Lyapunov}} and {{Control Barrier Functions}}},
  booktitle = {53rd {{IEEE Conference}} on {{Decision}} and {{Control}}},
  author = {Romdlony, Muhammad Zakiyullah and Jayawardhana, Bayu},
  year = {2014},
  month = dec,
  pages = {2293--2298},
  issn = {0191-2216},
  doi = {10.1109/CDC.2014.7039737},
  url = {https://ieeexplore.ieee.org/document/7039737},
  urldate = {2023-12-21},
  abstract = {In this paper, we propose a nonlinear control design for solving the problem of stabilization with guaranteed safety. The design is based on the merging of a Control Lyapunov Function and a Control Barrier Function. The proposed control method allows us to combine the design of a stabilizer based on CLF and the design of safety control based on CBF. The efficacy of the proposed approach is shown in the simulation results.}
}

@article{runggerComputingRobustControlled2017,
  title = {Computing {{Robust Controlled Invariant Sets}} of {{Linear Systems}}},
  author = {Rungger, Matthias and Tabuada, Paulo},
  year = {2017},
  month = jul,
  journal = {IEEE Transactions on Automatic Control},
  volume = {62},
  number = {7},
  pages = {3665--3670},
  issn = {1558-2523},
  doi = {10.1109/TAC.2017.2672859},
  abstract = {We consider controllable linear discrete-time systems with bounded perturbations and present two methods to compute robust controlled invariant sets. The first method tolerates an arbitrarily small constraint violation to compute an arbitrarily precise outer approximation of the maximal robust controlled invariant set, while the second method provides an inner approximation. The outer approximation scheme is {$\delta$}-complete, given that the constraint sets are formulated as finite unions of polytopes.}
}

@inproceedings{shenSamplingQuotientRingSumofSquares2020,
  title = {Sampling {{Quotient-Ring Sum-of-Squares Programs}} for {{Scalable Verification}} of {{Nonlinear Systems}}},
  booktitle = {2020 59th {{IEEE Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Shen, Shen and Tedrake, Russ},
  year = {2020},
  month = dec,
  pages = {2535--2542},
  issn = {2576-2370},
  doi = {10.1109/CDC42340.2020.9304028},
  abstract = {This paper presents a novel method, combining new formulations and sampling, to improve the scalability of sum-of-squares (SOS) programming-based system verification. Region-of-attraction approximation problems are considered for polynomial, polynomial with generalized Lur'e uncertainty, and rational trigonometric multi-rigid-body systems. Our method starts by identifying that Lagrange multipliers, traditionally heavily used for S-procedures, are a major culprit of creating bloated SOS programs. In light of this, we exploit inherent system properties-continuity, convexity, and implicit algebraic structure-and reformulate the problems as quotient-ring SOS programs, thereby eliminating all the multipliers. These new programs are smaller, sparser, less constrained, yet less conservative. Their computation is further improved by leveraging a recent result on sampling algebraic varieties. Remarkably, solution correctness is guaranteed with just a finite (in practice, very small) number of samples. Altogether, the proposed method can verify systems well beyond the reach of existing SOS-based approaches (32 states); on smaller problems where a baseline is available, it computes tighter solution 2-3 orders of magnitude faster.}
}

@article{shoukrySMCSatisfiabilityModulo2018,
  title = {{{SMC}}: {{Satisfiability Modulo Convex Programming}}},
  shorttitle = {{{SMC}}},
  author = {Shoukry, Yasser and Nuzzo, Pierluigi and {Sangiovanni-Vincentelli}, Alberto L. and Seshia, Sanjit A. and Pappas, George J. and Tabuada, Paulo},
  year = {2018},
  month = sep,
  journal = {Proceedings of the IEEE},
  volume = {106},
  number = {9},
  pages = {1655--1679},
  issn = {1558-2256},
  doi = {10.1109/JPROC.2018.2849003},
  abstract = {The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.}
}

@misc{SimulinkDesignVerifier2022,
  title = {Simulink {{Design Verifier Getting Started}}},
  year = {2022},
  url = {https://www.mathworks.com/help/pdf_doc/sldv/sldv_gs.pdf},
  howpublished = {The Mathworks, Inc.}
}

@misc{SimulinkDesignVerifier2022a,
  title = {Simulink {{Design Verifier User}}'s {{Guide}}},
  year = {2022},
  url = {https://www.mathworks.com/help/pdf_doc/sldv/sldv.pdf},
  howpublished = {The Mathworks, Inc.}
}

@book{tabuadaVerificationControlHybrid,
  title = {Verification and {{Control}} of {{Hybrid Systems}}: {{A Symbolic Approach}}},
  author = {Tabuada, Paulo},
  year = {2009},
  publisher = {Springer},
  address = {New York, NY},
  url = {https://doi.org/10.1007/978-1-4419-0224-5},
  urldate = {2022-09-08},
  abstract = {Hybrid systems describe the interaction of software, modeled by finite-state systems such as finite-state machines, with the physical world, described by infinite-state systems such as differential equations. Verification and Control of Hybrid Systems provides a unique systematic exposition of several classes of hybrid systems, admitting symbolic models along with the relationships between them. The text outlines several key verification and control synthesis results for hybrid systems, guided by the concept of bisimulation, and illustrated by numerous examples. The book is divided into four parts: Part I presents basic concepts centered on a notion of system that is general enough to describe finite-state, infinite-state, and hybrid systems. Part II discusses the ways in which systems relate to other systems, such as behavioral inclusion/equivalence and simulation/bisimulation, using these relationships to study verification and control synthesis problems for finite-state systems. Part III draws inspiration from timed automata to present several classes of hybrid systems, with richer continuous dynamics, that can be related to finite-state symbolic systems. Once such relationships are established, verification and control synthesis problems for these hybrid systems can be immediately solved by resorting to the techniques described in Part II for finite-state systems. Part IV follows the same strategy by generalizing simulation/bisimulation relationships to approximate simulation/bisimulation relationships that can be used for a wider class of hybrid systems. This comprehensive treatment will appeal to researchers, engineers, computer scientists, and graduate students in the areas of formal methods, verification, model checking, and control and will undoubtedly inspire further study of the specialized literature.},
  isbn = {978-1-4419-0223-8}
}

@incollection{tedrakeChapterAcrobotsCartPoles2022,
  title = {Chapter 3: {{Acrobots}}, {{Cart-Poles}}, and {{Quadrotors}}},
  booktitle = {Underactuated {{Robotics}}: {{Algorithms}} for {{Walking}}, {{Running}}, {{Swimming}}, {{Flying}}, and {{Manipulation}}},
  author = {Tedrake, Russ},
  year = {2022},
  series = {Course {{Notes}} for {{MIT}} 6.832},
  url = {http://underactuated.mit.edu/acrobot.html}
}

@incollection{tedrakeChapterLyapunovAnalysis2022,
  title = {Chapter 9: {{Lyapunov}} Analysis},
  booktitle = {Underactuated {{Robotics}}: {{Algorithms}} for {{Walking}}, {{Running}}, {{Swimming}}, {{Flying}}, and {{Manipulation}}},
  author = {Tedrake, Russ},
  year = {2022},
  series = {Course {{Notes}} for {{MIT}} 6.832},
  url = {http://underactuated.mit.edu/lyapunov.html}
}

@incollection{tedrakeChapterSimplePendulum2022,
  title = {Chapter 2: {{The}} Simple Pendulum},
  booktitle = {Underactuated {{Robotics}}: {{Algorithms}} for {{Walking}}, {{Running}}, {{Swimming}}, {{Flying}}, and {{Manipulation}}},
  author = {Tedrake, Russ},
  year = {2022},
  series = {Course {{Notes}} for {{MIT}} 6.832},
  url = {http://underactuated.mit.edu/pend.html}
}

@article{tedrakeLQRtreesFeedbackMotion2010,
  title = {{{LQR-trees}}: {{Feedback Motion Planning}} via {{Sums-of-Squares Verification}}},
  shorttitle = {{{LQR-trees}}},
  author = {Tedrake, Russ and Manchester, Ian R. and Tobenkin, Mark and Roberts, John W.},
  year = {2010},
  month = jul,
  journal = {The International Journal of Robotics Research},
  volume = {29},
  number = {8},
  pages = {1038--1052},
  publisher = {SAGE Publications Ltd STM},
  issn = {0278-3649},
  doi = {10.1177/0278364910369189},
  url = {https://doi.org/10.1177/0278364910369189},
  urldate = {2022-08-12},
  abstract = {Advances in the direct computation of Lyapunov functions using convex optimization make it possible to efficiently evaluate regions of attraction for smooth non-linear systems. Here we present a feedback motion-planning algorithm which uses rigorously computed stability regions to build a sparse tree of LQR-stabilized trajectories. The region of attraction of this non-linear feedback policy ``probabilistically covers'' the entire controllable subset of state space, verifying that all initial conditions that are capable of reaching the goal will reach the goal. We numerically investigate the properties of this systematic non-linear feedback design algorithm on simple non-linear systems, prove the property of probabilistic coverage, and discuss extensions and implementation details of the basic algorithm.},
  langid = {english}
}

@article{tobenkinInvariantFunnelsTrajectories2011,
  title = {Invariant {{Funnels}} around {{Trajectories}} Using {{Sum-of-Squares Programming}}},
  author = {Tobenkin, Mark M. and Manchester, Ian R. and Tedrake, Russ},
  year = {2011},
  month = jan,
  journal = {IFAC Proceedings Volumes},
  series = {18th {{IFAC World Congress}}},
  volume = {44},
  number = {1},
  pages = {9218--9223},
  issn = {1474-6670},
  doi = {10.3182/20110828-6-IT-1002.03098},
  url = {https://www.sciencedirect.com/science/article/pii/S1474667016450925},
  urldate = {2022-08-15},
  abstract = {This paper presents numerical methods for computing regions of finite-time invariance (funnels) around solutions of polynomial differential equations. The methods are compared on stabilized trajectories of a six-state model of a satellite. First, we present a method which exactly certifies sufficient conditions for invariance despite relying on approximate trajectories from numerical integration. Our second method relaxes the constraints of the first by sampling in time. On the model system, this recovered almost identical funnels but was much faster to compute. In both cases, funnels are verified using Sum-of-Squares programming to search over time-varying quadratic Lyapunov functions. We examine both time-varying rescalings of quadratic forms computed from linearizations and searching directly over time-varying quadratic Lyapunov functions. On the model system the latter provided larger funnels at the cost of increased computation time.},
  langid = {english}
}

@inproceedings{wielandConstructiveSafetyUsing2007,
  title = {Constructive Safety Using Control Barrier Functions},
  booktitle = {{{IFAC Proceedings Volumes}}},
  author = {Wieland, Peter and Allg{\"o}wer, Frank},
  year = {2007},
  month = jan,
  series = {7th {{IFAC Symposium}} on {{Nonlinear Control Systems}}},
  volume = {40},
  pages = {462--467},
  doi = {10.3182/20070822-3-ZA-2920.00076},
  url = {https://www.sciencedirect.com/science/article/pii/S1474667016355690},
  urldate = {2022-08-12},
  abstract = {This paper presents a new safety feedback design for nonlinear systems based on barrier certificates and the idea of control Lyapunov functions. In contrast to existing methods, this approach ensures safety independently of abstract high-level tasks that might be unknown or change over time. Leaving as much freedom as possible to the safe system, the authors believe that the flexibility of this approach is very promising. The design is validated using an illustrative example.},
  langid = {english}
}

@inproceedings{wiltzConstructionControlBarrier2023,
  title = {Construction of {{Control Barrier Functions Using Predictions}} with {{Finite Horizon}}},
  booktitle = {2023 62nd {{IEEE Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Wiltz, Adrian and Tan, Xiao and Dimarogonas, Dimos V.},
  year = {2023},
  month = dec,
  pages = {2743--2749},
  issn = {2576-2370},
  doi = {10.1109/CDC49753.2023.10383564},
  url = {https://ieeexplore.ieee.org/abstract/document/10383564/citations#citations},
  urldate = {2025-01-03},
  abstract = {In this paper, we show that under mild controllability assumptions a time-invariant Control Barrier Function (CBF) can be constructed based on predictions with a finite horizon. As a starting point, we require only a known subset of a control-invariant set where the latter set does not need to be explicitly known. We show that, based on ideas similar to the Hamilton-Jacobi reachability analysis, the knowledge on the subset of a control-invariant set allows us to obtain a time-invariant CBF for the time-invariant dynamics under consideration. We also provide a thorough analysis of the properties of the constructed CBF, we characterize the impact of the prediction horizon, and comment on the practical implementation. In the end, we relate our construction approach to Model Predictive Control (MPC). With a relevant application example, we demonstrate how our method is applied.}
}

@misc{wongpiromsarnLectureModelChecking2020,
  type = {Lecture},
  title = {Lecture 4 {{Model Checking}} and {{Logic Synthesis}}},
  author = {Wongpiromsarn, Nok and Murray, Richard M. and Topcu, Ufuk},
  year = {2020},
  month = mar,
  address = {Belgrade (Serbia)},
  url = {http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model_checking-09Mar2020.pdf},
  langid = {english}
}

@article{wongpiromsarnSynthesisControlProtocols2013,
  title = {Synthesis of {{Control Protocols}} for {{Autonomous Systems}}},
  author = {Wongpiromsarn, Tichakorn and Topcu, Ufuk and Murray, Richard M.},
  year = {2013},
  month = jul,
  journal = {Unmanned Systems},
  volume = {01},
  number = {01},
  pages = {21--39},
  publisher = {World Scientific Publishing Co.},
  issn = {2301-3850},
  doi = {10.1142/S2301385013500027},
  url = {https://www.worldscientific.com/doi/abs/10.1142/S2301385013500027},
  urldate = {2023-01-04},
  abstract = {This article provides a review of control protocol synthesis techniques that incorporate methodologies from formal methods and control theory to provide correctness guarantee for different types of autonomous systems, including those with discrete and continuous state space. The correctness of the system is defined with respect to a given specification expressed as a formula in linear temporal logic to precisely describe the desired properties of the system. The formalism presented in this article admits nondeterminism, allowing uncertainties in the system to be captured. A particular emphasis is on alleviating some of the difficulties, e.g., heterogeneity in the underlying dynamics and computational complexity, that naturally arise in the construction of control protocols for autonomous systems.}
}

@book{xiaoSafeAutonomyControl2023,
  title = {Safe {{Autonomy}} with {{Control Barrier Functions}}: {{Theory}} and {{Applications}}},
  shorttitle = {Safe {{Autonomy}} with {{Control Barrier Functions}}},
  author = {Xiao, Wei and Cassandras, Christos G. and Belta, Calin},
  year = {11 kv{\v e}tna 2023},
  abstract = {This book presents the concept of Control Barrier Function (CBF), which captures the evolution of safety requirements during the execution of a system and can be used to enforce safety. Safety is formalized using an emerging state-of-the-art approach based on CBFs, and many illustrative examples from autonomous driving, traffic control, and robot control are provided. Safety is central to autonomous systems since they are intended to operate with minimal or no human supervision, and a single failure could result in catastrophic results. The authors discuss how safety can be guaranteed via both theoretical and application perspectives. This presented method is computationally efficient and can be easily implemented in real-time systems that require high-frequency reactive control. In addition, the CBF approach can easily deal with nonlinear models and complex constraints used in a wide spectrum of applications, including autonomous driving, robotics, and traffic control. With the proliferation of autonomous systems, such as self-driving cars, mobile robots, and unmanned air vehicles, safety plays a crucial role in ensuring their widespread adoption. This book considers the integration of safety guarantees into the operation of such systems including typical safety requirements that involve collision avoidance, technological system limitations, and bounds on real-time executions. Adaptive approaches for safety are also proposed for time-varying execution bounds and noisy dynamics.},
  isbn = {978-3-031-27575-3}
}

@article{xuConstrainedControlInput2018,
  title = {Constrained Control of Input--Output Linearizable Systems Using Control Sharing Barrier Functions},
  author = {Xu, Xiangru},
  year = {2018},
  month = jan,
  journal = {Automatica},
  volume = {87},
  pages = {195--201},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2017.10.005},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109817305046},
  urldate = {2024-12-18},
  abstract = {Control barrier functions (CBFs) have been used as an effective tool for designing a family of controls that ensures the forward invariance of a set. When multiple CBFs are present, it is important that the set of controls satisfying all the barrier conditions is non-empty. In this paper, we investigate such a control-sharing property for multiple CBFs and provide sufficient and necessary conditions for the property to hold. Based on that, we study the tracking control design problem of an input--output linearizable system with multiple time-varying output constraints, where the output constraints are encoded as CBFs and the barrier conditions are expressed as hard constraints in a quadratic program (QP) whose feasibility is guaranteed by the control-sharing property of the CBFs. With the controller generated from the QP, the output constraints are always satisfied and the tracking objective is achieved when it is not conflicting with the constraints. The effectiveness of our control design method is illustrated by two examples.}
}