We introduce a novel notion of invariance feedback entropy to quantify the state information that is required by any controller that enforces a given subset of the state space to be invariant. We establish a number of elementary properties, e.g., we provide conditions that ensure that the invariance feedback entropy is finite and show for the deterministic case that we recover the well-known notion of entropy for deterministic control systems. We prove the data rate theorem, which shows that the invariance entropy is a tight lower bound of the data rate of any coder controller that achieves invariance in the closed loop. We analyze uncertain linear control systems and derive a universal lower bound of the invariance feedback entropy. The lower bound depends on the absolute value of the determinant of the system matrix and a ratio involving the volume of the invariant set and the set of uncertainties. Furthermore, we derive a lower bound of the data rate of any static, memoryless coder controller. Both lower bounds are intimately related and for certain cases it is possible to bound the performance loss due to the restriction to static coder controllers by 1 bit/time unit. We provide various examples throughout the article to illustrate and discuss different definitions and results.

The article addresses the issue of reliability of complex embedded control systems in the safety-critical environment. In this article, we propose a novel approach to design controller that (i) guarantees the safety of nonlinear physical systems, (ii) enables safe system restart during runtime, and (iii) allows the use of complex, unverified controllers (e.g., neural networks) that drive the physical systems toward complex specifications. We use abstraction-based controller synthesis approach to design a formally verified controller that provides application and system-level fault tolerance along with safety guarantee. Moreover, our approach is implementable using a commercial-off-the-shelf (COTS) processing unit. To demonstrate the efficacy of our solution and to verify the safety of the system under various types of faults injected in applications and in the underlying real-time operating system (RTOS), we implemented the proposed controller for the inverted pendulum and three degrees-of-freedom (3-DOF) helicopter.

We present novel results on the solution of a class of leavable, undiscounted optimal control problems in the minimax sense for nonlinear, continuous-state, discrete-time plants. The problem class includes entry-(exit-)time problems as well as minimum-time, pursuit-evasion, and reach-avoid games as special cases. We utilize auxiliary optimal control problems (“abstractions”) to compute both upper bounds of the value function, i.e., of the achievable closed-loop performance, and symbolic feedback controllers realizing those bounds. The abstractions are obtained from discretizing the problem data, and we prove that the computed bounds and the performance of the symbolic controllers converge to the value function as the discretization parameters approach zero. In particular, if the optimal control problem is solvable on some compact subset of the state space, and if the discretization parameters are sufficiently small, then we obtain a symbolic feedback controller solving the problem on that subset. These results do not assume the continuity of the value function or any problem data, and they fully apply in the presence of hard state and control constraints.

While many studies and tools target the basic stabilizability problem of networked control systems (NCS), nowadays modern systems require more sophisticated objectives such as those expressed as formulae in linear temporal logic or as automata on infinite strings. One general technique to achieve this is based on so-called symbolic models, where complex systems are approximated by finite abstractions, and then, correct-by-construction controllers are automatically synthesized for them. We present tool SENSE for the construction of finite abstractions for NCS and the automated synthesis of controllers. Constructed controllers enforce complex specifications over plants in NCS by taking into account several non-idealities of the communication channels. Given a symbolic model of the plant and network parameters, SENSE can efficiently construct a symbolic model of the NCS, by employing operations on binary decision diagrams (BDDs). Then, it synthesizes symbolic controllers satisfying a class of specifications. It has interfaces for the simulation and the visualization of the resulting closed-loop systems using OMNETPP and MATLAB. Additionally, SENSE can generate ready-to-implement VHDL/Verilog or C/C++ codes from the synthesized controllers.

We propose an algorithm to over-approximate the reachable set of nonlinear systems with bounded, time-varying parameters and uncertain initial conditions. The algorithm is based on the conservative representation of the nonlinear dynamics by a differential inclusion consisting of a linear term and the Minkowsky sum of two convex sets. The linear term and one of the two sets are obtained by a conservative first-order over-approximation of the nonlinear dynamics with respect to the system state. The second set accounts for the effect of the time-varying parameters. A distinctive feature of the novel algorithm is the possibility to over-approximate the reachable set to any desired accuracy by appropriately choosing the parameters in the computation. We provide an example that illustrates the effectiveness of our approach.

We consider a compositional construction of approximate abstractions of interconnected control systems. In our framework, an abstraction acts as a substitute in the controller design process and is itself a continuous control system. The abstraction is related to the concrete control system via a so-called simulation function: a Lyapunov-like function, which is used to establish a quantitative bound between the behavior of the approximate abstraction and the concrete system. In the first part of the paper, we provide a small gain type condition that facilitates the compositional construction of an abstraction of an interconnected control system together with a simulation function from the abstractions and simulation functions of the individual subsystems. In the second part of the paper, we restrict our attention to linear control system and characterize simulation functions in terms of controlled invariant, externally stabilizable subspaces. Based on those characterizations, we propose a particular scheme to construct abstractions for linear control systems. We illustrate the compositional construction of an abstraction on an interconnected system consisting of four linear subsystems. We use the abstraction as a substitute to synthesize a controller to enforce a certain linear temporal logic specification.

Bipedal robots are prime examples of complex cyber–physical systems (CPSs). They exhibit many of the features that make the design and verification of CPS so difficult: hybrid dynamics, large continuous dynamics in each mode (e.g., 10 or more state variables), and nontrivial specifications involving nonlinear constraints on the state variables. In this paper, we propose a two-step approach to formally synthesize controllers for bipedal robots so as to enforce specifications by design and thereby generate physically realizable stable walking. In the first step, we design outputs and classical controllers driving these outputs to zero. The resulting controlled system evolves on a lower dimensional manifold and is described by the hybrid zero dynamics governing the remaining degrees of freedom. In the second step, we construct an abstraction of the hybrid zero dynamics that is used to synthesize a controller enforcing the desired specifications to be satisfied on the full order model. Our two step approach is a systematic way to mitigate the curse of dimensionality that hampers the applicability of formal synthesis techniques to complex CPS. Our results are illustrated with simulations showing how the synthesized controller enforces all the desired specifications and offers improved performance with respect to a classical controller. The practical relevance of the results is illustrated experimentally on the bipedal robot AMBER 3.

We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.

We study a class of leavable, undiscounted, minimax optimal control problems for perturbed, continuous-valued, nonlinear control systems. Leaving or “stopping” is mandatory and the costs are assumed to be non-negative, extended real-valued functions. In a previous contribution, we have shown that this class of optimal control problems is amenable to the solution based on symbolic models of the plant in the sense that an arbitrarily precise upper bound on the value function (measured in terms of its hypograph) can be computed from a given abstraction with prescribed precision on every compact subset of state space. In this work, we propose an algorithm to compute arbitrarily precise abstractions of discrete-time plants that represent the sampled behavior of continuous-time, perturbed, nonlinear control systems and establish the convergence rate of the precision in dependence of the discretization parameters of the algorithm. We illustrate the algorithm by approximately solving an optimal control problem involving a two dimensional version of the cart-pole swing-up problem.

This report documents the program and the outcomes of Dagstuhl Seminar 17201 "Formal Synthesis of Cyber-Physical Systems." Formal synthesis is the application of algorithmic techniques based on automata and logic to the design of controllers for hybrid systems in which continuous components interact with discrete ones. The Dagstuhl seminar brought together researchers from control theory and from computer science to discuss the state-of-the-art and current challenges in the field.

Legged anthropomorphic robots are a prime example of complex, highly nonlinear control systems. For example, the dynamics of the DLR C-Runner (Compliant Runner), a legged robot designed at the German Aerospace Center (DLR) [1], is described by a nonlinear, high-dimensional hybrid system, see Fig. 1. The different hybrid domains, defined by whether the feet of the robot are in contact with the ground, are defined by complex, physically motivated constraints. This makes the control of bipedal robots one of the most challenging controller synthesis tasks of today. The goal of this master thesis is to develop a two-step approach, similar to [2], to synthesize a controller that generates a stable, physical realizable walking gait for the DLR C-Runner. In the first step, a classical controller is designed to drive certain outputs of the system to zero. The resulting controlled system evolves on a lower dimensional manifold and is described by the so-called hybrid zero dynamics. In the second step, the symbolic synthesis approach [3] is used to design a controller for the hybrid zero dynamics to enforce a given specification. Here, the specification has to be designed so that its satisfaction implies a stable, physical realizable walking gait on the bipedal robot. Relaying on the symbolic synthesis for the stabilization, a controller is obtained which guarantees the specification. Therefore resulting in an improvement as compared to state-of-the-art approaches based on numerical optimization. The resulting controller should be first, evaluated in simulation and second, implemented and analyzed on the DLR C-Runner. If time permits, an alternative, passivity-based technique (which is known to be less sensitive to modeling error than feedback linearization) should be applied and implemented to control the outputs of the system to zero.

We introduce a notion of invariance feedback entropy for discrete-time, nondeterministic control systems as a measure of necessary state information to enforce a given subset of the state space to be invariant. We provide conditions that guarantee finiteness and show that the well-known notion of invariance feedback entropy for deterministic systems is recovered in the deterministic case. We establish the data rate theorem which shows that the entropy equals the largest lower bound on the data rate of any coder-controller that achieves invariance. For finite systems, the invariance feedback entropy is characterized by the value function of an appropriately designed mean-payoff game. We use several examples throughout the paper to instantiate the various definitions and results.

In this paper we propose a compositional framework for the construction of approximations of the interconnection of a class of stochastic hybrid systems. As special cases, this class of systems includes both jump linear stochastic systems and linear stochastic hybrid automata. In the proposed framework, an approximation is itself a stochastic hybrid system, which can be used as a replacement of the original stochastic hybrid system in a controller design process. We employ a notion of so-called stochastic simulation function to quantify the error between the approximation and the original system. In the first part of the paper, we derive sufficient conditions which facilitate the compositional quantification of the error between the interconnection of stochastic hybrid subsystems and that of their approximations using the quantified error between the stochastic hybrid subsystems and their corresponding approximations. In particular, we show how to construct stochastic simulation functions for approximations of interconnected stochastic hybrid systems using the stochastic simulation function for the approximation of each component. In the second part of the paper, we focus on a specific class of stochastic hybrid systems, namely, jump linear stochastic systems, and propose a constructive scheme to determine approximations together with their stochastic simulation functions for this class of systems. Finally, we illustrate the effectiveness of the proposed results by constructing an approximation of the interconnection of four jump linear stochastic subsystems in a compositional way.

This report documents the program and the outcomes of Dagstuhl Seminar 17201 “Formal Synthesis of Cyber-Physical Systems.” Formal synthesis is the application of algorithmic techniques based on automata and logic to the design of controllers for hybrid systems in which continuous components interact with discrete ones. The Dagstuhl seminar brought together researchers from control theory and from computer science to discuss the state-of-the-art and current challenges in the field. Seminar May 14–19, 2017 – http://www.dagstuhl.de/17201 1998 ACM Subject Classification I.2.8 Problem Solving, Control Methods, and Search—Control theory; I.2.2 Automatic Programming; F.3.1 Specifying and Verifying and Reasoning about Programs

In a previous work, we extended the notion of invariance entropy, also known as topological feedback entropy, of deterministic nonlinear control systems to systems with nondeterministic disturbances and showed that this notion of invariance feedback entropy characterizes the necessary data rate of any coder-controller scheme that communicates via digital, noiseless channel and achieves invariance of a given subset of the state space. In this paper, we derive an intrinsic lower bound of the invariance feedback entropy for linear systems with bounded disturbances in terms of the absolute value of the determinant of the system matrix and a ratio involving the volume of the invariant set as well as the volume of the disturbance set. Additionally, we derive a lower bound of the data rate associated with static, memoryless coder-controllers. If the data rate of a static coder-controller matches the lower bound, we obtain the remarkable property that its data rate is not larger than 1 bit/time unit compared to the best dynamically achievable data rate. The lower bounds are tight for some classes of systems.

We consider the symbolic controller synthesis approach to enforce safety specifications on perturbed, nonlinear control systems. In general, in each state of the system several control values might be applicable to enforce the safety requirement and in the implementation one has the burden of picking a particular control value out of possibly many. We present a class of implementation strategies to obtain a controller with certain performance guarantees. This class includes two existing implementation strategies from the literature, based on discounted payoff and mean-payoff games. We unify both approaches by using games characterized by a single discount factor determining the implementation. We evaluate different implementations from our class experimentally on two case studies. We show that the choice of the discount factor has a significant influence on the average long-term costs, and the best performance guarantee for the symbolic model does not result in the best implementation. Comparing the optimal choice of the discount factor here with the previously proposed values, the costs differ by a factor of up to 50. Our approach therefore yields a method to choose systematically a good implementation for safety controllers with quantitative objectives.

This paper addresses the problem of synthesizing controllers for reactive missions carried out by dynamical systems operating in environments of known physical geometry but consisting of uncontrolled elements that the system must react to at execution time. Such problems have value in semi-structured industrial automation settings, especially those in which robots must behave collaboratively yet safely with their human counterparts. The proposed synthesis framework addresses cases where there exists no satisfying controller for the mission, given the dynamical system and the environment's assumed behaviors. We introduce an approach that leverages information about an abstraction of the dynamical system to automatically generate a concise set of revisions to such specifications. We provide a graphical visualization tool as a design aid, allowing the revisions to be conveyed to the user interactively and added to the specification at the user's discretion. Any accepted statements become certificates that, if satisfied at runtime, provide guarantees for the current mission on the given dynamics. Our approach is cast into a general framework that works with various discrete representations (i.e. abstractions) of the system dynamics. We present case studies that illustrate application of our approach to controller synthesis for two example robotic missions employing different abstractions of the system.