Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL$\,{\to}\,$DPA$\,{\to}\,$COCOA), where the first step ignores natural colors and requires involved constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid such constructions and obtain a direct translation from LTL to COCOA. In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new path from LTL to DPA and exploits the definition of natural colors. It relies on standard operations on weak alternating automata, the Miyano-Hayashi breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

Abstract In many applications for which reactive synthesis is attractive, computed implementations need to have understandable behavior. While some existing synthesis approaches compute finite-state machines with a structure that supports their understandability, such approaches do not scale to specifications that can only be realized with a large number of states. Furthermore, asking the engineer to understand the internal structure of the implementation is unnecessary when only the behavior of the implementation is to be understood. In this paper, we present an approach to computing understandable safety invariants that every implementation satisfying a generalized reactivity(1) specification needs to fulfill. Together with the safety part of the specification, the invariants completely define which transitions between input and output proposition valuations any correct implementation can take. We apply the approach in two case studies and demonstrate that the computed invariants highlight the strategic decisions that implementations for the given specification need to make, which not only helps the system designer with understanding what the specification entails, but also supports specification debugging.

Abstract Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure – the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-Büchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.

Inferring correct and meaningful specifications of complex (black-box) systems is an important problem in practice, which arises naturally in debugging, reverse engineering, formal verification, and explainable AI, to name just a few examples.Usually, one here assumes that both positive and negative examples of system traces are given-an assumption that is often unrealistic in practice because negative examples (i.e., examples that the system cannot exhibit) are typically hard to obtain.To overcome this serious practical limitation, we develop a novel technique that is able to infer specifications in the form of universal very-weak automata from positive examples only.This type of automata captures exactly the class of properties in the intersection of Linear Temporal Logic (LTL) and the universal fragment of Computation Tree Logic (ACTL), and features an easy-to-interpret graphical representation.Our proposed algorithm reduces the problem of learning a universal very-weak automaton to the enumeration of elements in the Pareto front of a specifically-designed monotonous function and uses classical automaton minimization to obtain a concise, finite-state representation of the learned property.In a case study with specifications from the Advanced Microcontroller Bus Architecture, we demonstrate that our approach is able to infer meaningful, concise, and easy-to-interpret specifications from positive examples only.

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.

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.

Whether robot controllers are manually designed or synthesized from high-level task specifications, assumptions about the environment need to be made, which can involve adversarial events or cooperative robots. In either case, if these assumptions are violated at runtime, the robot will fail to fulfill its task and will likely do something unexpected. In this paper, we focus on controllers synthesized from linear temporal logic. We tackle the problem of making these controllers robust against environment assumption violations that are common in robot execution. Our solution is a three-layer system: first, we propose an offline approach that accounts for transient violations such that the robot can still complete its task after temporary anomalies; the second layer is an online approach that automatically relaxes the environment assumptions to better capture environment behaviors and that allows the robot to react accordingly; and, finally, we automatically modify the actual environment behaviors, when possible, through negotiation with one of the environment robots operating in the workspace, such that our assumptions are met by the other robot and both robots accomplish their tasks.

The Exists-Forall (EF) synthesis problem deals with finding parameters such that for all input assignments a correctness specification is met. Many standard problems from computer-aided design and verification can be formulated as an instance of EF synthesis when a function template with holes - parameters to be synthesized - is provided. In this paper, we generalize the idea of EF synthesis in the context of Boolean logic by allowing existential quantification over the domain of Boolean functions (rather than Boolean variables) and present a bounded synthesis approach guided by counterexamples to generate them using techniques from Boolean learning. As an application, we present circuit rectification as an EF synthesis problem and apply the presented approach to incrementally synthesize patches for digital circuits with multiple seeded faults.

We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is an important goal in the design of distributed systems, because systems that are composed from identical components are easier to build and maintain. We show that for the class of rotation-symmetric architectures, i.e., multi-process architectures where all processes have access to all system inputs, but see different rotations of the inputs, the symmetric synthesis problem is EXPTIME-complete in the number of processes. In architectures where the processes do not have access to all input variables, the symmetric synthesis problem becomes undecidable, even in cases where the standard distributed synthesis problem is decidable.

Lack of complete run-time information about the environment behavior significantly increases the computational complexity and limits the applicability of practical reactive synthesis methods, e.g., synthesis from generalized reactivity( 1) specifications. We tackle this difficulty by splitting incomplete-information controller synthesis into estimator construction and complete-information synthesis steps. The estimator, which executes in parallel to the controller, establishes approximations of the unobserved variables that are salient for the synthesis step. It essentially provides an abstraction from the belief space of the controller, whose exponential growth often plagues incomplete-information synthesis, by keeping track of only the properties of relevance for the specification engineer and the scenario under consideration.

By performing synthesis from formal high-level mission specifications, we can obtain robot controllers that are guaranteed to operate correctly under the specified environment conditions. Such conditions must be stated in the specification whenever there is no way in which the robot's task can be fulfilled without them holding, and they relate the possible behaviors of the environment with the behavior of the robot. Contemporary synthesis algorithms however frequently construct implementations that try to trivially satisfy their specifications by actively working towards the violation of the assumptions, which is undesirable behavior.

We consider a problem on the synthesis of optimal reactive controllers with an a priori unknown performance criterion while satisfying a given temporal logic specification through the interaction with an uncontrolled environment. We decouple the problem into two sub-problems. First, we extract a (maximally) permissive strategy for the system, which encodes multiple (possibly all) ways in which the system can react to the adversarial environment and satisfy the specifications. Then, we quantify the a priori unknown performance criterion as a (still unknown) reward function, and compute - by using the so-called maximin-Q learning algorithm - an optimal strategy for the system within the operating envelope allowed by the permissive strategy. We establish both correctness (with respect to the temporal logic specifications) and optimality (with respect to the a priori unknown performance criterion) of this two-step technique for a fragment of temporal logic specifications. For specifications beyond this fragment, correctness can still be preserved, but the learned strategy may be sub-optimal. We present an algorithm to the overall problem, and demonstrate its use and computational requirements on a set of robot motion planning examples.

We consider the synthesis of reactive systems that are robust against intermittent violations of their environment assumptions. Such assumptions are needed to allow many systems that work in a larger context to fulfill their tasks. Yet, due to glitches in hardware or exceptional operating conditions, these assumptions do not always hold in the field. Manually constructed systems often exhibit error-resilience and can continue to work correctly in such cases. With the development cycles of reactive systems becoming shorter, and thus reactive synthesis becoming an increasingly suitable alternative to the manual design of such systems, automatically synthesized systems are also expected to feature such resilience.

A recent method to obtain correct robot controllers is to automatically synthesize them from high-level robot missions that are specified in temporal logic. In this context, we aim for controllers that are optimal, i.e., do not let the robot take unnecessarily costly paths to reach its goals. Previous work on obtaining optimal synthesized robot controllers either ignored interactions with the environment, or assumed a cooperative environment. In this paper, we solve the problem of obtaining optimal robot controllers for adversarial environments. Our main observation is that the quality of a path to a goal has two dimensions: (1) the number of phases in which the robot waits for the environment to perform some actions and (2) the cost of the robot's actions to reach the goal. Our synthesis algorithm can take any prioritization over the possible cost combinations into account, and computes the optimal strategy in a symbolic manner, despite the fact that the action costs can be non-integer. We show the scalability of the new algorithm by example of a delivery problem.

We present constraint matrix diagrams (CMDs), a novel data structure for the fully symbolic reach ability analysis of timed automata. CMDs combine matrix-based and diagram-based state space representations generalizing the concepts of difference bound matrices (DBMs), clock difference diagrams (CDDs), and clock restriction diagrams (CRDs). The key idea is to represent convex parts of the state space as (partial) DBMs which are, in turn, organized in a CDD/CRD-like ordered and reduced diagram. The location information is incorporated as a special Boolean constraint in the matrices. We describe all CMD operations needed for the construction of the transition relation and the reach ability fixed point computation. Based on a prototype implementation, we compare our technique with the timed model checkers RED and Uppaal, and furthermore investigate the impact of two different reduced forms on the time and space consumption.

This paper presents results from extensive simulation studies on the iterated prisoner’s dilemma. Two models were implemented: a nongroup model in order to study fundamental principles of cooperation and a model to imitate ethnocentrism. Some extensions of Axelrod’s elementary model implemented individual reputation. We furthermore introduced group reputation to provide a more realistic scenario. In an environment with group reputation the behavior of one agent will affect the reputation of the whole group and vice-versa. While kind agents (e.g. those with a cooperative behavior) lose reputation when being in a group, in which defective strategies are more common, agents with defective behavior on the other hand benefit from a group with more cooperative strategies. We demonstrate that group reputation decreases cooperation with the in-group and increases cooperation with the out-group.

The Prisoner's Dilemma and the Public Goods Game are models to study mechanisms leading to the evolution of cooperation. From a simplified rational and egoistic perspective there should be no altruistic cooperation in these games at all. Previous studies observed circumstances under which cooperation can emerge. This paper demonstrates that high-order punishment opportunities can maintain a higher cooperation level in an agent based simulation of the evolution of cooperation.