Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> An autonomous robot offers a challenging and ideal field for the study of intelligent architectures. Autonomy within a rational be havior could be evaluated by the robot's effectiveness and robust ness in carrying out tasks in different and ill-known environments. It raises major requirements on the control architecture. Further more, a robot as a programmable machine brings up other archi tectural needs, such as the ease and quality of its specification and programming.This article describes an integrated architecture that allows a mobile robot to plan its tasks—taking into account temporal and domain constraints, to perform corresponding actions and to con trol their execution in real-time—while being reactive to possible events. The general architecture is composed of three levels: a de cision level, an execution level, and a functional level. The latter is composed of modules that embed the functions achieving sensor- data processing and effector control. The decision level is goal and event driven, a... <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> We describe the Simplex architecture, a real-time software technology which supports the safe, reliable introduction of control system upgrades while the system is running. We introduce its basic structure in control systems, discuss its fault-tolerance feature, and investigate the control issues when the technology is employed. Application of the Simplex architecture is demonstrated for a plasma-enhanced chemical vapor deposition (PECVD) system, a standard process in semiconductor manufacturing. We conclude the paper with a discussion of the potential impact that the Simplex architecture can make on future control applications. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Given a robot model and a class of admissible environments, this paper provides a framework for automatically and verifiably composing controllers that satisfy high level task specifications expressed in suitable temporal logics. The desired task specifications can express complex robot behaviors such as search and rescue, coverage, and collision avoidance. In addition, our framework explicitly captures sensor specifications that depend on the environment with which the robot is interacting, resulting in a novel paradigm for sensor-based temporal logic motion planning. As one robot is part of the environment of another robot, our sensor-based framework very naturally captures multi-robot specifications. Our computational approach is based on first creating discrete controllers satisfying so-called general reactivity formulas. If feasible, the discrete controller is then used in order to guide the sensor-based composition of continuous controllers resulting in a hybrid controller satisfying the high level specification, but only if the environment is admissible. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Hybrid systems describe the interaction of software, described by finite models such as finite-state machines, with the physical world, described by infinite models such as differential equations. This book addresses problems of verification and controller synthesis for hybrid systems. Although these problems are very difficult to solve for general hybrid systems, several authors have identified classes of hybrid systems that admit symbolic or finite models. The novelty of the book lies on the systematic presentation of these classes of hybrid systems along with the relationships between the hybrid systems and the corresponding symbolic models. To show how the existence of symbolic models can be used for verification and controller synthesis, the book also outlines several key results for the verification and controller design of finite systems. Several examples illustrate the different methods and techniques discussed in the book. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Formal verification efforts in the area of robotics are still comparatively scarce. In this paper we report on our experiences with one such effort, which was concerned with designing, implementing and certifying a safety function for autonomous vehicles and robots. We outline the algorithm which was specifically designed with safety through formal verification in mind, and present our verification methodology, which is based on formal proof and verification using the theorem prover Isabelle. The necessary normative measures that are covered are discussed. The algorithm and our methodology have been certified for use in applications up to SIL 3 of IEC61508-3 by a certification authority. Throughout, issues we recognised as being important for a successful application of formal methods in the domain at hand are highlighted. These pertain to the development process, the abstraction level at which specifications should be formulated, and the interplay between simulation and verification, among others. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Robot swarms provide a way for a number of simple robots to work together to carry out a task. While swarms have been found to be adaptable, fault-tolerant and widely applicable, designing individual robot algorithms so as to ensure effective and correct swarm behaviour is very difficult. In order to assess swarm effectiveness, either experiments with real robots or computational simulations of the swarm are usually carried out. However, neither of these involve a deep analysis of all possible behaviours. In this paper we will utilise automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether our swarms will indeed behave as required. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> This paper addresses the problem of navigating in a provably safe manner a mobile robot with a limited field-of-view placed in a unknown dynamic environment. In such a situation, absolute motion safety (in the sense that no collision will ever take place whatever happens in the environment) is impossible to guarantee in general. It is therefore settled for a weaker level of motion safety dubbed passive motion safety: it guarantees that, if a collision takes place, the robot will be at rest. ::: ::: The primary contribution of this paper is the concept of Braking Inevitable Collision States (ICS), i.e. a version of the ICS corresponding to passive motion safety. Braking ICS are defined as states such that, whatever the future braking trajectory followed by the robot, a collision occurs before it is at rest. Passive motion safety is obtained by avoiding Braking ICS at all times. ::: ::: It is shown that Braking ICS verify properties that allow the design of an efficient Braking ICS-Checking algorithm, i.e. an algorithm that determines whether a given state is a Braking ICS or not. ::: ::: To validate the Braking ICS concept and demonstrate its usefulness, the Braking ICS-Checking algorithm is integrated in a reactive navigation scheme called PassAvoid. It is formally established that PassAvoid is provably passively safe in the sense that it is guaranteed that the robot will always stay away from Braking ICS no matter what happens in the environment. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> I l l u S t r a t I o n b y a l I C I a k u b I S t a /a n D r I J b o r y S a S S o C I a t e S in This arTiCle we consider the question: How should autonomous systems be analyzed? in particular, we describe how the confluence of developments in two areas—autonomous systems architectures and formal verification for rational agents—can provide the basis for the formal verification of autonomous systems behaviors. We discuss an approach to this question that involves: 1. Modeling the behavior and describing the interface (input/output) to an agent in charge of making decisions within the system; 2. Model checking the agent within an unrestricted environment representing the “real world” and those parts of the systems external to the agent, in order to establish some property, j; 3. Utilizing theorems or analysis of the environment, in the form of logical statements (where necessary), to derive properties of the larger system; and 4. if the agent is refined, modify (1), but if environmental properties are clarified, modify (3). Autonomous systems are now being deployed in safety, mission, or business critical scenarios, which means a thorough analysis of the choices the core software might make becomes crucial. But, should the analysis and verification of autonomous software be treated any differently than traditional software used in critical situations? Or is there something new going on here? Autonomous systems are systems that decide for themselves what to do and when to do it. Such systems might seem futuristic, but they are closer than we might think. Modern household, business, and industrial systems increasingly incorporate autonomy. There are many examples, all varying in the degree of autonomy used, from almost pure human control to fully autonomous activities with minimal human interaction. Application areas are broad, ranging from healthcare monitoring to autonomous vehicles. But what are the reasons for this increase in autonomy? Typically, autonomy is used in systems that: 1. must be deployed in remote environments where direct human control is infeasible; 2. must be deployed in hostile environments where it is dangerous for humans to be nearby, and so difficult for humans to assess the possibilities; 3. involve activity that is too lengthy Verifying autonomous systems Doi:10.1145/2494558 <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty. <s> BIB011 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Human‐robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include healthcare and manufacturing, in which people need the assistance of machines to perform key tasks. It is essential for robots working in close proximity to people to be both safe and trustworthy. In this paper we examine formal verification of a high-level planner/scheduler for autonomous personal robotic assistants such as CareO-bot R . We describe how a model of Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some formal verification results and describe how these could be complemented by simulation-based testing and realworld end-user validation in order to increase the practical and perceived safety and trustworthiness of robotic assistants. <s> BIB012 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> This paper addresses the problem of safely navigating a mobile robot with limited sensing capability and limited information about stationary obstacles. We consider two sensing limitations: blind spots between sensors and limited sensing range. We identify a set of constraints on the sensors’ readings whose satisfaction at time t guarantees collision-freedom during the time interval \([t, t + \varDelta t]\). Here, \(\varDelta t\) is a parameter whose value is bounded by a function of the maximum velocity of the robot and the range of the sensors. The constraints are obtained under assumptions about minimum internal angle and minimum edge length of polyhedral obstacles. We apply these constraints in the switching logic of the Simplex architecture to obtain a controller that ensures collision-freedom. Experiments we have conducted are consistent with these claims. To the best of our knowledge, our study is the first to provide runtime assurance that an autonomous mobile robot with limited sensing can navigate without collisions with only limited information about obstacles. <s> BIB013 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Ensuring that autonomous systems work ethically is both complex and difficult. However, the idea of having an additional ‘governor’ that assesses options the system has, and prunes them to select the most ethical choices is well understood. Recent work has produced such a governor consisting of a ‘consequence engine’ that assesses the likely future outcomes of actions then applies a Safety/Ethical logic to select actions. Although this is appealing, it is impossible to be certain that the most ethical options are actually taken. In this paper we extend and apply a well-known agent verification approach to our consequence engine, allowing us to verify the correctness of its ethical decision-making. <s> BIB014 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Currently, the control software of swarm robotics systems is created by ad hoc development. This makes it hard to deploy these systems in real-world scenarios. In particular, it is difficult to maintain, analyse, or verify the systems. Formal methods can contribute to overcome these problems. However, they usually do not guarantee that the implementation matches the specification, because the system’s control code is typically generated manually. Also, there is cultural resistance to apply formal methods; they may be perceived as an additional step that does not add value to the final product. To address these problems, we propose supervisory control theory for the domain of swarm robotics. The advantages of supervisory control theory, and its associated tools, are a reduction in the amount of ad hoc development, the automatic generation of control code from modelled specifications, proofs of properties over generated control code, and the reusability of formally designed controllers between different robotic platforms. These advantages are demonstrated in four case studies using the e-puck and Kilobot robot platforms. Experiments with up to 600 physical robots are reported, which show that supervisory control theory can be used to formally develop state-of-the-art solutions to a range of problems in swarm robotics. <s> BIB015 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Abstract Autonomous systems such as unmanned vehicles are beginning to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan. <s> BIB016 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> The widespread adoption of autonomous systems depends on providing guarantees of safety and functional correctness, at both design time and runtime. Information about the extent to which functional requirements can be met in combination with non-functional requirements (NFRs) -- i.e. requirements that can be partially complied with -- , under dynamic and uncertain environments, provides opportunities to enhance the safety and functional correctness of systems at design time. We present a technique to formally define system attributes that can change or be changed to deal with dynamic and uncertain environments (denominated weakened specifications) as a partially ordered lattice, and to automatically explore the system under different specifications, using probabilistic model checking, to find the likelihood of satisfying a requirement. The resulting probabilities form boundaries of "optimal specifications", analogous to Pareto frontiers in multi-objective optimization, informing the designer about the system's capabilities, such as resilience or robustness, when changing its attributes to deal with dynamic and uncertain environments. We illustrate the proposed technique through a domestic robotic assistant example. <s> BIB017 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach. <s> BIB018 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> This article answers fundamental safety questions for ground robot navigation: under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective, as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot’s environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why the robots can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins. We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles; (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves; (iii) the stronger passive-friendly safety, in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well; and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. To account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem-proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions. <s> BIB019 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and further development of such robotic assistants is inhibited by the absence of assurances about their safety. In previous work, formal models of the robot behaviour and its environment were constructed by hand and model checkers were then used to check whether desirable formal temporal properties were satisfied for all possible system behaviours. In this paper we describe the details of the software CRutoN, that provides an automatic translation from sets of robot control rules into input for the model checker NuSMV. We compare our work with previous attempts to formally verify the robot control rules, discuss the potential applications of the approach, and consider future directions of research. <s> BIB020 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> Work in swarm robotics typically focuses on the bottom-up design of local rules for individual robots that create emergent swarm behaviors. In this paper, we take a top-down approach and consider the following problem: how can we specify a desired collective behavior and automatically synthesize decentralized controllers that can be distributed over robots to achieve the collective objective in a provably correct way? We propose a formal specification language for the high-level description of swarm behaviors on both swarm and individual levels. We present algorithms for automated synthesis of decentralized controllers and synchronization skeletons that describe how groups of robots must coordinate to satisfy the specification. We demonstrate our algorithms on a case study. <s> BIB021 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> The ability to navigate in diverse and previously unknown environments is a critical service of autonomous robots. The validation of the navigation software typically involves test campaigns in the field, which are costly and potentially risky for the robot itself or its environment. An alternative approach is to perform simulation-based testing, by immersing the software in virtual worlds. A question is then whether the bugs revealed in real worlds can also be found in simulation. The paper reports on an exploratory study of bugs in an academic software for outdoor robots navigation. The detailed analysis of the triggers and effects of these bugs shows that most of them can be revealed in low-fidelity simulation. It also provides insights into interesting navigation scenarios to test as well as into how to address the test oracle problem. <s> BIB022 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Modeling the Physical Environment <s> A major challenge towards large scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. To this end, we present a framework for building safe robots. Our approach for validating the end-to-end correctness of robotics system consists of two parts: (1) a high-level programming language for implementing and systematically testing the reactive robotics software via model checking; (2) a signal temporal logic (STL) based online monitoring system to ensure that the assumptions about the low-level controllers (discrete models) used during model checking hold at runtime. Combining model checking with runtime verification helps us bridge the gap between software verification (discrete) that makes assumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world. To demonstrate the efficacy of our approach, we build a safe adaptive surveillance system and present software-in-the-loop simulations of the application. <s> BIB023
As mentioned in Section 1, we consider an autonomous robot as a machine that implements AI techniques, has a physical presence, and interacts with the world. Thus, one of the most prominent challenges in verifying robotic systems is its interaction with an unstructured environment. This is further complicated by differing sensor accuracy or motor performance, or components that are degraded or damaged. Interactions between a robot and its physical environment can have a major influence on its behavior, because the robot may be reacting to environmental conditions not considered at design time. Indeed, the behavior of adaptive systems is directly driven by environmental interactions. While it is accepted that formally modeling a robotic system within its physical environment is important BIB010 BIB007 , it has had limited attention in the literature. We believe that this is due to the sheer complexity of this task: aside from the difficulty of modeling the real world, a robot only has partial knowledge of its surroundings. Sensing limitations caused by sensor blind-spots and interference between sensors add extra complexity to the modeling process BIB009  BIB013 . To address the challenge of combining discrete computations and a continuous environment, a robotic system is typically separated into several layers BIB001 BIB010 . At the bottom, the functional layer consists of control software for the robot's hardware. Then, the intermediate layer generally utilizes a middleware framework (such as ROS  or G en oM  ) that provides an interface to the hardware components. The upper layer contains the decision-making components of the robotic system, which capture its autonomous behavior. Some previous work has focused on a robot's decision making, ignoring its environment BIB008 BIB015 . Others assume that the environment is static and known, prior to the robot's deployment BIB020 BIB021 BIB012 , which is often neither possible nor feasible  . For example, the environment may contain both fixed and mobile objects whose future behavior is unknown BIB009 , or the robot's goal may be to map the environment, so the layout is unknown. Hybrid architectures often take a third approach: to abstract away from the environment and assume that a component has the ability to provide predicates that represent the continuous sensor data about the robot's environment BIB016 BIB014 BIB010 BIB006 BIB003 . While this encapsulates the high-level control, insulating it from the environment, the implicit assumption of a static, known environment can often remain. Using models of the environment that are static and assume prior knowledge may limit their effectiveness. However, Sotiropoulos et al. BIB022 examine the ability of low-fidelity environmental simulations to reproduce bugs that were found during field tests of the same robot. Of the 33 bugs that occured during the field test, only one could not be reproduced in the low-fidelity simulation. Perhaps similar results might be obtained with low-fidelity formal models of a robot's environment. Probabilistic models are a popular approach to capturing dynamic and uncertain environments. In BIB017 , a PRISM model captures the environment of a domestic assistant robot. Nonrobot actors in the environment are specified using probabilistic behaviors, to represent the uncertainty about their behavior. The robot model is also written in PRISM, so that it can be reasoned about within this probabilistic environment. This is a useful step that accepts the changing nature of the environment. However, for the model checker to explore outcomes based on a certain behavior, its probability must be encoded into the environment model. This still leaves the possibility of unforeseen situations having a detrimental effect on the robot's behavior. Similarly, Hoffmann et al. BIB018 formalize a pilotless aircraft and its physical environment using an extension of Probabilistic Finite-State Machines (PFSMs). They use PRISM to verify properties about their model, with the pilotless aircraft tasked with foraging for objects, which it must return to a drop-off location. Their approach involves running small-scale simulations of the pilotless aircraft in its environment to determine the probabilities and timing values for their formal model. In contrast, Costelha and Lima  divide their models into layers and try to obtain a model of the robot's environment that is as realistic as possible. Their work uses Petri Nets with the environment model using untimed direct transitions and other layers in the models using stochastic Petri Nets. Modeling the environment is particularly relevant for navigation, and tackling collision avoidance and safe robot navigation BIB009 BIB011 BIB013  often feature in the literature. Although several navigation algorithms exist, some cannot be used in safety-critical scenarios because they have not been verified BIB013 . The Simplex architecture BIB002 provides a gateway to using these unverified algorithms with the concept of advanced controllers (ACs). ACs are used alongside a verified baseline controller (BC) and a decision module, which chooses which controller is active. The decision module monitors the system, and if it determines that the AC will violate one of the safety properties, then the BC takes control. Other work employs reachability analysis to generate a maneuver automaton for collision avoidance of road vehicles  . Here, differential equations model the continuous behaviour of the system. Runtime fault monitoring is useful for catching irregular behaviors in running systems, but it does not ensure safety in all situations. Mitsch et al. BIB011 use differential dynamic logic (dL) BIB004 , designed for hybrid systems, to describe the discrete and continuous navigation behavior of a ground robot. Their approach uses hybrid programs for modeling a robot that follows the dynamic window algorithm and for modeling the behavior of moving objects in the environment. Using the hybrid theorem prover KeYmaera, Mitsch et al. verify that the robot will not collide with, and maintains a sufficient distance from, stationary and moving obstacles. In proving these safety properties, 85% of the proof steps were carried out automatically. In further work, Mitsch et al. BIB019 verify a safety property that makes less conservative driving assumptions, allowing for imperfect sensors, and add liveness proofs to guarantee progress. They extend their approach to add runtime monitors that can be automatically synthesized from their hybrid models. They note that all models deviate from reality, so their runtime monitors complement the offline proofs by checking for mismatches between the verified model and the real world. Formal and nonformal models of the real world are prone to the problem of the reality gap, where models produced are never close enough to the real world to ensure successful transfer of their results BIB010 BIB007 . This is especially problematic when real-world interactions can impact safety. Bridging the gap between discrete models of behavior and the continuous nature of the real world in a way that allows strong verification is often intractable BIB023 . Moreover, in a multirobot setting one robot can be part of another's environment BIB005 . There is also a tradeoff between ensuring that the system is safe and ensuring that it is not so restrictive that it is unusable in practice BIB007 .