Designing robot controllers that correctly react to changes in the environment is a time-consuming and error-prone process. An alternative is to use “correct-by-construction” synthesis approaches to automatically generate controller designs from high-level specifications. In particular, Generalized Reactivity(l) or GR(1) specifications are well-suited to express specifications for robots that must act in dynamic environments, and approaches to generate controller designs from GR(1) specifications are highly computationally efficient. Toward that end, this paper presents Salty, a domain-specific language for GR(1) specifications. While tools exist to synthesize system designs from GR(1) specifications, Salty makes such specifications easier to write and debug by supporting features such as richer input and output types, user-defined macros, common specification patterns, and specification optimization and sanity checking. Salty interfaces with the separately developed synthesis tool Slugs to produce a system or controller design, and Salty translates this design to a software implementation in a variety of languages. We demonstrate Salty on an application involving coordination of multiple unmanned air vehicles (UAVs) and provide a workflow for connecting synthesized UAV controllers to freely available UAV planning and simulation software suites UxAS and AMASE.

Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given the temporal logic specification that is to be obeyed by the learning system, we propose to synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification. We discuss which requirements a shield must meet to preserve the convergence guarantees of the learner. Finally, we demonstrate the versatility of our approach on several challenging reinforcement learning scenarios.

Classification techniques are useful for processing complex signals into labels with semantic value. For example, they can be used to interpret brain signals generated by humans corresponding to a finite set of commands for a physical device. The classifier, however, may interpret the signal as a command that is different from the intended one. This error in classification leads to poor performance in tasks where the class labels are used to learn some information or to control a physical device. We propose a computationally efficient algorithm to identify which class labels may be misclassified out of a sequence of class labels, when these labels are used in a given learning or control task. The algorithm is based on inference methods using Markov random fields. We apply the algorithm to goal-learning and tracking using brain-computer interfacing (BCI), in which signals from the brain are commonly processed using classification techniques. We demonstrate that the proposed algorithm reduces the time taken to identify the goal state in control experiments.

Shield synthesis is an approach to enforce safety properties at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to hand back control to the system as soon as possible. In the first part of this paper, we consider shield synthesis for reactive hardware systems. First, we define a general framework for solving the shield synthesis problem. Second, we discuss two concrete shield synthesis methods that automatically construct shields from a set of safety properties: (1) k-stabilizing shields, which guarantee recovery in a finite time. (2) Admissible shields, which attempt to work with the system to recover as soon as possible. Next, we discuss an extension of k-stabilizing and admissible shields, where erroneous output values of the reactive system are corrected while liveness properties of the system are preserved. Finally, we give experimental results for both synthesis methods. In the second part of the paper, we consider shielding a human operator instead of shielding a reactive system: the outputs to be corrected are not initiated by a system but by a human operator who works with an autonomous system. The challenge here lies in giving simple and intuitive explanations to the human for any interferences of the shield. We present results involving mission planning for unmanned aerial vehicles.