When designing agents for operation in uncertain environments, designers need tools to automatically reason about what agents ought to do, how that conflicts with what is actually happening, and how a policy might be modified to remove the conflict. These obligations include ethical and social obligations, permissions and prohibitions, which constrain how the agent achieves its mission and executes its policy. We propose a new deontic logic, Expected Act Utilitarian deontic logic, for enabling this reasoning at design time: for specifying and verifying the agent's strategic obligations, then modifying its policy from a reference policy to meet those obligations. Unlike approaches that work at the reward level, working at the logical level increases the transparency of the trade-offs. We introduce two algorithms: one for model-checking whether an RL agent has the right strategic obligations, and one for modifying a reference decision policy to make it meet obligations expressed in our logic. We illustrate our algorithms on DAC-MDPs which accurately abstract neural decision policies, and on toy gridworld environments.

We present an algorithm for approximating the language of a temporal logic formula, that is, the set of all signals that satisfy the formula. Most tasks involving temporal logic require determining whether a signal satisfies the formula, or finding such satisfying signals: example tasks include monitoring, testing, control synthesis, formula inference, and example generation. In the majority of cases this is done via search heuristics, especially for logics not always amenable to exhaustive methods. Search heuristics take a variable time to run and might not converge to the desired signals. There is a wide variety of heuristics and, apart from falsification, no solid guidelines for choosing between them. We take a different approach: we directly approximate the entire language of the formula. With such an approximation, we might solve the above tasks faster and/or obtain guarantees on the solution. For example, generating satisfying signals reduces to random sampling in a union of polytopes. This paper focuses on the language approximation process. We do this approximation in the special case of discrete-time Signal Temporal Logic. We show the language in this case is a union of polytopes, and upper bound the number of polytopes. We then present an algorithm for approximating this language. We evaluate the algorithm empirically and observe that it is often able to compute a highly accurate representation of the language, and that for a fixed language, the algorithm requires fewer iterations as the length of the signal increases. These results suggest that working with the language is a viable way to solving many temporal logic tasks, and raise interesting theoretical questions for investigation.

This work gives a logical characterization of the (ethical and social) obligations of an agent trained with Reinforcement Learning (RL). An RL agent takes actions by following a utility-maximizing policy. We maintain that the choice of utility function embeds ethical and social values implicitly, and that it is necessary to make these values explicit. This work provides a basis for doing so. First, we propose a probabilistic deontic logic that is suited for formally specifying the obligations of a stochastic system, including its ethical obligations. We prove some useful validities about this logic, and how its semantics are compatible with those of Markov Decision Processes (MDPs). Second, we show that model checking allows us to prove that an agent has a given obligation to bring about some state of affairs - meaning that by acting optimally, it is seeking to reach that state of affairs. We develop a model checker for our logic against MDPs. Third, we observe that it is useful for a system designer to obtain a logical characterization of her system's obligations, which is potentially more interpretable and helpful in debugging than the expression of a utility function. Enumerating all the obligations of an agent is impractical, so we propose a Bayesian optimization routine that learns to generate a system's obligations that the system designer deems interesting. We implement the model checking and Bayesian optimization routines, and demonstrate their effectiveness with an initial pilot study. This work provides a rigorous method to characterize utility-maximizing agents in terms of the (ethical and social) obligations that they implicitly seek to satisfy.

Is it possible to determine whether a signal violates a formula in Signal Temporal Logic (STL), if the monitor only has access to a low-resolution version of the signal? We answer this question affirmatively by demonstrating that temporal logic has a multiresolution structure, which parallels the multiresolution structure of signals. A formula in discrete-time Signal Temporal Logic (STL) is equivalently defined via the set of signals that satisfy it, known as its language. If a wavelet decomposition x = y + d is performed on each signal x in the language, we end up with two signal sets Y and D, where Y contains the low-resolution approximation signals y, and D contains the detail signals d needed to reconstruct the x’s. This paper provides a complete computational characterization of both Y and D using a novel constraint set encoding of STL, s.t. x satisfies a formula if and only if its decomposition signals satisfy their respective encoding constraints. Then a conservative logical approximation of Y is also provided: namely, we show that Y is over approximated by the language of a formula − 1. By iterating the decomposition, we obtain a sequence of lower-resolution formulas − 1, − 2, − 3,... which thus constitute a multiresolution analysis of. This work lays the foundation for multiresolution monitoring in distributed systems. One potential application of these results is a multiresolution monitor that can detect specification violation early by simply observing a low-resolution version of the signal to be monitored. 1

We demonstrate the first recurrent neural network architecture for learning signal temporal logic (TL) formulas, and present the first systematic comparison of formula inference methods. Legacy systems embed much expert knowledge which is not explicitly formalized. There is great interest in learning formal specifications that characterize the ideal behavior of such systems—that is, formulas in TL that are satisfied by the system’s output signals. Such specifications can be used to better understand the system’s behavior and improve the design of its next iteration. Previous inference methods either assumed certain formula templates, or did a heuristic enumeration of all possible templates. This work proposes a neural network architecture that infers the formula structure via gradient descent, eliminating the need for imposing any specific templates. It combines the learning of formula structure and parameters in one optimization. Through systematic comparison, we demonstrate that this method achieves similar or better misclassification rates (MCRs) than enumerative and lattice methods. We also observe that different formulas can achieve similar MCR, empirically demonstrating the under-determinism of the problem of TL inference.

Urban Air Mobility, the scenario where hundreds of manned and Unmanned Aircraft Systems (UASs) carry out a wide variety of missions (e.g., moving humans and goods within the city), is gaining acceptance as a transportation solution of the future. One of the key requirements for this to happen is safely managing the air traffic in these urban airspaces. Due to the expected density of the airspace, this requires fast autonomous solutions that can be deployed online. We propose Learning-‘N-Flying (LNF), a multi-UAS Collision Avoidance (CA) framework. It is decentralized, works on the fly, and allows autonomous Unmanned Aircraft System (UAS)s managed by different operators to safely carry out complex missions, represented using Signal Temporal Logic, in a shared airspace. We initially formulate the problem of predictive collision avoidance for two UASs as a mixed-integer linear program, and show that it is intractable to solve online. Instead, we first develop Learning-to-Fly (L2F) by combining (1) learning-based decision-making and (2) decentralized convex optimization-based control. LNF extends L2F to cases where there are more than two UASs on a collision path. Through extensive simulations, we show that our method can run online (computation time in the order of milliseconds) and under certain assumptions has failure rates of less than 1% in the worst case, improving to near 0% in more relaxed operations. We show the applicability of our scheme to a wide variety of settings through multiple case studies.

In this article, we develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions, and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU) [23], is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems and illustrate it by model-checking obligations of a self-driving car controller from the literature.

We consider the pressing question of how to model, verify, and ensure that autonomous systems meet certain obligations (like the obligation to respect traffic laws), and refrain from impermissible behavior (like recklessly changing lanes). Temporal logics are heavily used in autonomous system design; however, as we illustrate here, temporal (alethic) logics alone are inappropriate for reasoning about obligations of autonomous systems. This paper proposes the use of Dominance Act Utilitarianism (DAU), a deontic logic of agency, to encode and reason about obligations of autonomous systems. We use DAU to analyze Intel's Responsibility-Sensitive Safety (RSS) proposal as a real-world case study. We demonstrate that DAU can express well-posed RSS rules, formally derive undesirable consequences of these rules, illustrate how DAU could help design systems that have specific obligations, and how to model-check DAU obligations.

In multi-agent systems, robots transmit their planned trajectories to each other or to a central controller, and each receiver plans its own actions by maximizing a measure of mission satisfaction. For missions expressed in temporal logic, the robustness function plays the role of satisfaction measure. Currently, a Piece-Wise Linear (PWL) or piece-wise constant reconstruction is used at the receiver. This allows an efficient robustness computation algorithm - a.k.a. monitoring - but is not adaptive to the signal class of interest, and does not leverage the compression properties of more general representations. When communication capacity is at a premium, this is a serious bottleneck. In this paper we first show that the robustness computation is significantly affected by how the continuous-time signal is reconstructed from the received samples, which can mean the difference between a successful control and a crash. We show that monitoring general spline-based reconstructions yields a smaller robustness error, and that it can be done with the same time complexity as monitoring the simpler PWL reconstructions. Thus robustness computation can now be adapted to the signal class of interest. We further show that the monitoring error is tightly upper-bounded by the L∞ signal reconstruction error. We present a (non-linear) L∞-based scheme which yields even lower monitoring error than the spline-based schemes (which have the advantage of being faster to compute), and illustrate all results on two case studies. As an application of these results, we show how time-frequency specifications can be efficiently monitored online.

Implantable medical devices are safety-critical systems whose incorrect operation can jeopardize a patient's health, and whose algorithms must meet tight platform constraints like memory consumption and runtime. In particular, we consider here the case of implantable cardioverter defibrillators, where peak detection algorithms and various others discrimination algorithms serve to distinguish fatal from non-fatal arrhythmias in a cardiac signal. Motivated by the need for powerful formal methods to reason about the performance of arrhythmia detection algorithms, we show how to specify all these algorithms using Quantitative Regular Expressions (QREs). QRE is a formal language to express complex numerical queries over data streams, with provable runtime and memory consumption guarantees. We show that QREs are more suitable than classical temporal logics to express in a concise and easy way a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today's arrhythmia detection devices. The proposed formalization also opens the way to formal analysis and rigorous testing of these detectors' correctness and performance, alleviating the regulatory burden on device developers when modifying their algorithms. We demonstrate the effectiveness of our approach by executing QRE-based monitors on real patient data on which they yield results on par with the results reported in the medical literature.

This paper surveys recent challenges and solutions in the design, implementation, and verification of embedded software for robotics. Emphasis is placed on mobile robots, like self-driving cars. In design, it addresses programming support for robotic systems, secure state estimation, and ROS-based monitor generation. In the implementation phase, it describes the synthesis of control software using finite precision arithmetic, real-time platforms and architectures for safety-critical robotics, efficient implementation of neural network based-controllers, and standards for computer vision applications. The issues in verification include verification of neural network-based robotic controllers, and falsification of closed-loop control systems. The paper also describes notable open-source robotic platforms. Along the way, we highlight important research problems for developing the next generation of high-performance, low-resource-usage, correct embedded software.

As methods and tools for cyber-physical systems (CPS) grow in capabilities and use, one-size-fits-all solutions start to show their limitations. In particular, tools and languages for programming an algorithm or modeling a CPS that are specific to the application domain are typically more usable, and yield better performance, than general-purpose languages and tools. In the domain of cardiac arrhythmia monitoring, a small, implantable medical device continuously monitors the patient's cardiac rhythm and delivers electrical therapy when needed. The algorithms executed by these devices are streaming algorithms, so they are best programmed in a streaming language that allows the programmer to reason about the incoming data stream as the basic object, rather than force her to think about lower-level details like state maintenance and minimization. Because these devices are resource-constrained, it is useful if the programming language allowed predictable performance in terms of processing runtime and energy consumption, or more general costs. StreamQRE is a declarative streaming programming language, with an efficient and portable implementation and strong theoretical guarantees. In particular, its evaluation algorithm guarantees constant cost (runtime, memory, energy) per data item and also calculates upper bounds on the per-item cost. Such an estimate of the cost allows early exploration of the algorithmic possibilities, while maintaining a handle on worst case performance, on the basis of which hardware can be designed and algorithms can be tuned.

Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and delta-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter delta used in delta-decidability when it is used to verify MTL properties. We present an application of this result in the form of an algorithm that generates new constraints to the delta-decision procedure from falsification runs, which can speed up the verification run. We then establish new conditions under which robust testing, based on the robust semantics of MTL, is in fact a quasi-semidecision procedure. These results allow us to delimit what is possible with fast, robustness-based methods, accelerate (near-)exhaustive verification, and further bridge the gap between verification and simulation.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient's body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

Autonomous vehicles promise significant benefits to society, from reduced accident rates to greater mobility for the elderly. The biggest challenge in the design of autonomous vehicles comes from the uncertainty of the environment in which they will operate. Their control algorithms must be able to cope with driving events that occur on widely ranging time scales. For example, relaxed rural driving can accommodate planning actions every few seconds, while imminent collision avoidance requires planning and actuation on the order of a few milliseconds. Thus 'real-time' performance will imply different things depending on the context.

Control software of autonomous robots has stringent real-time requirements that must be met to achieve the control objectives. One source of variability in the performance of a control system is the execution time and accuracy of the state estimator that provides the controller with state information. This estimator is typically perception-based (e.g., Computer Vision-based) and is computationally expensive. When the computational resources of the hardware platform become overloaded, the estimation delay can compromise control performance and even stability. In this paper, we define a framework for co-designing anytime estimation and control algorithms, in a manner that accounts for implementation issues like delays and inaccuracies. We construct an anytime perception-based estimator from standard off-the-shelf Computer Vision algorithms, and show how to obtain a trade-off curve for its delay vs estimate error behaviour. We use this anytime estimator in a controller that can use this trade-off curve at runtime to achieve its control objectives at a reduced energy cost. When the estimation delay is too large for correct operation, we provide an optimal manner in which the controller can use this curve to reduce estimation delay at the cost of higher inaccuracy, all the while guaranteeing basic objectives are met. We illustrate our approach on an autonomous hexrotor and demonstrate its advantage over a system that does not exploit co-design.

In model-based design of cyber-physical systems, such as switched mixed-signal circuits or software-controlled physical systems, it is common to develop a sequence of system models of different fidelity and complexity, each appropriate for a particular design or verification task. In such a sequence, one model is often derived from the other by a process of simplification or implementation. E.g. a Simulink model might be implemented on an embedded processor via automatic code generation. Three questions naturally present themselves: how do we quantify closeness between the two systems? How can we measure such closeness? If the original system satisfies some formal property, can we automatically infer what properties are then satisfied by the derived model? This paper addresses all three questions: we quantify the closeness between original and derived model via a distance measure between their outputs. We then propose two computational methods for approximating this closeness measure. Finally, we derive syntactical re-writing rules which, when applied to a Metric Temporal Logic specification satisfied by the original model, produce a formula satisfied by the derived model. We demonstrate the soundness of the theory with several experiments.

We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

This work addresses the problem of mosquito noise (MN) reduction in compressed video sequences. A compression-blind approach is adopted; the advantage of such an approach is that it is independent of the particular compressor used and of its particular settings. A recursive filtering scheme is presented. It is shown how the filtering parameter ϵ can be adaptively selected to maximize the denoising performance by minimizing the number of outlier pixels in the filter's support. Simulation results show that the proposed blind MN-denoising scheme outperforms existing MN-denoising methods.