ABSTRACT. In control theory, complex models of physical processes, such as systems of differential equations, are analyzed or controlled from simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition systems. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. In this talk, I will discuss a set of approaches to formal synthesis of control strategies for dynamical systems from temporal logic specifications. I will first show how automata games for finite systems can be extended to obtain conservative control strategies for low dimensional linear and multilinear dynamical systems. I will then present several methods to reduce conservativeness and improve the scalability of the control synthesis algorithms for more general classes of dynamics. I will illustrate the usefulness of these approaches with examples from robotics and traffic control.

ABSTRACT. Partial differential equations (PDEs) mathematically describe a wide range of phenomena such as fluid dynamics, or quantum mechanics. Although great achievements have been accomplished in the field of numerical methods for solving PDEs, from a safety verification (or falsification) perspective, methods are still needed to verify (or falsify) a system whose dynamics is specified as a PDE that may depend not only on space, but also on time. As many cyber-physical systems (CPS) involve sensing and control of physical phenomena modeled as PDEs, reachability analysis of PDEs provides novel methods for safety verification and falsification. As a first step to address this challenging problem, we propose a reachability analysis approach leveraging the well-known Galerkin Finite Element Method (FEM) for a class of one-dimensional linear parabolic PDEs with fixed but uncertain inputs and initial conditions, which is a subclass of PDEs that is useful for modeling, for instance, heat flows. In particular, a continuous approximate reachable set of the parabolic PDE is computed using linear interpolation. Since a complete conservativeness is hardly achieved by using the approximate reachable set, to enhance the conservativeness, we investigate the error bound between the numerical solution and the exact analytically unsolvable solution to bloat the continuous approximate reachable set. This bloated reachable set is then used for safety verification and falsification. In the case that the safety specification is violated, our approach produces a numerical trace to prove that there exists an initial condition and input that lead the system to an unsafe state.

ABSTRACT. Counterexamples encountered in formal verification are typically used as evidence for violation of specification. They also play a crucial role in CEGAR based techniques, where the counterexample guides the refinements to be performed on the abstractions. While several scalable techniques for verification have been developed for safety verification of hybrid systems, less attention has been paid to extracting the various types of counterexamples for safety violations. Since these systems are infinite state systems, the number of counterexamples for safety violations are potentially infinite and hence searching for the right counterexample becomes a challenging task. In this paper, we present a technique for providing various types of counterexamples for a safety violation of the linear dynamical system. More specifically, we develop algorithms to extract the longest counterexample — the execution that stays in the unsafe set for most time, and deepest counterexample — the execution that ventures the most into the unsafe set in a specific direction provided by the user.

ABSTRACT. Safety proofs of discrete and continuous systems often use related proof approaches, and insight can be obtained by comparing reasoning methods across domains. For example, proofs using inductive invariants in discrete systems are analogous to barrier certificate methods in continuous systems. In this paper, we present and prove the soundness of continuous and hybrid analogs to the k-induction proof rule, which we call t-barrier certificates. The method combines symbolic reasoning and time-bounded reachability along the barrier in order to prove system safety. Compared with traditional barrier certificates, a larger class of functions can be shown to be t-barrier certificates, so we expect them to be easier to find. Compared with traditional reachability analysis, t-barrier certificates can be computationally tractable in nonlinear settings despite large initial sets, and they prove time-unbounded safety. We demonstrate the feasibility of the approach with a nonlinear harmonic oscillator example, using sympy and Z3 for symbolic reasoning and Flow* for reachability analysis.

ABSTRACT. We present an approach to learn and formally verify feedback laws for data-driven models of neural networks. Neural networks are emerging as powerful and general data-driven representations for functions. This has led to their increased use in data-driven plant models and the representation of feedback laws in control systems. However, it is hard to formally verify properties of such feedback control systems. The proposed learning approach uses a receding horizon formulation that samples from the initial states and disturbances to enforce properties such as reachability, safety and stability. Next, our verification approach uses an over-approximate reachability analysis over the system, supported by range analysis for feedforward neural networks. We report promising results obtained by applying our techniques on several challenging nonlinear dynamical systems.

ABSTRACT. Non-asymptotic bounded-error state estimators that provide hard bounds on the estimation error are crucial for safety-critical applications. This paper proposes a class of optimal bounded-error affine estimators to achieve a novel property we are calling Equalized Recovery that can be computed by leveraging ideas from the dual problem of affine finite horizon optimal control design. In particular, by using Q-parametrization, the estimator design problem is reduced to a convex optimization problem. An extension of this estimator to handle missing data (e.g., due to package drops or sensor glitches) is also proposed. These ideas are illustrated with a numerical example motivated by vehicle safety systems.

ABSTRACT. This work deals with the observability analysis for LHS’s considering both known and unknown inputs and constrained discrete dynamics, modeled by Petri nets. For this, the concept of eventual observability is recalled as the possibility of uniquely determining both the discrete and the continuous states after a finite number of switchings. In this way, the information provided by the continuous and the discrete outputs of the LHS can be combined to determine the discrete state after a finite number of switchings. Next, based on the knowledge of the visited locations, a continuous observer can estimate the continuous state. It is shown that under this approach the observability conditions are greatly relaxed with respect to other approaches in the literature, in particular, neither the observability of the linear systems nor the observability of the underlying discrete event system are required.

ABSTRACT. In this paper we introduce and characterize the notion of approximate predictability for the general class of metric systems, which are a powerful modeling framework to deal with complex heterogeneous systems such as hybrid systems. Approximate predictability corresponds to the possibility of predicting the occurrence of specific states belonging to a particular subset of interest, in advance with respect to their occurrence, on the basis of observations corrupted by measurement errors. We establish a relation between approximate predictability of a given metric system and approximate predictability of a metric system that approximately simulates the given one. This relation allows checking approximate predictability of a system with an infinite number of states, provided that one is able to construct a metric system with a finite number of states and inputs, approximating the original one in the sense of approximate simulation. The analysis of approximate predictability of Piecewise Affine (PWA) systems is carried out as an application of the proposed approach.

ABSTRACT. This paper considers the design of separating input signals in order to discriminate among a finite number of uncertain nonlinear models. Each nonlinear model corresponds to a system operating mode, unobserved intents of other drivers or robots, or to fault types or attack strategies, etc., and the separating inputs are designed such that the output trajectories of all the nonlinear models are guaranteed to be distinguishable from each other under any realization of uncertainties in the initial condition, model discrepancies or noise. We propose a two-step approach. First, using an optimization-based approach, we over-approximate nonlinear dynamics by uncertain affine models, as abstractions that preserve all its system behaviors such that any discrimination guarantees for the affine abstraction also hold for the original nonlinear system. Then, we propose a novel solution in the form of a mixed-integer linear program (MILP) to the active model discrimination problem for uncertain affine models, which includes the affine abstraction and thus, the nonlinear models. Finally, we demonstrate the effectiveness of our approach for identifying the intention of other vehicles in a highway lane changing scenario.

ABSTRACT. Mechanistic models in biology often involve numerous parameters about which we do not have direct experimental information. The traditional approach is to fit these parameters using extensive numerical simulations (e.g. by the Monte-Carlo method), and eventually revising the model if the predictions do not correspond to the actual measurements. In this work we propose a methodology for hybrid system model revision, when new types of functions are needed to capture time varying parameters. To this end, we formulate a hybrid optimal control problem with intermediate points as successive infinite-dimensional linear programs (LP) on occupation measures. Then, these infinite-dimensional LPs are solved using a hierarchy of semidefinite relaxations. The whole procedure is applied on a recent model for haemoglobin production in erythrocytes.

ABSTRACT. Safety control consists in maintaining the state of a given system inside a specified set of safe states. Traditionally, the problem is tackled using set-theoretic methods, which are mostly qualitative: states are partitioned between safety-controllable (i.e. states that belong to the maximal controlled invariant subset of the safe set) and safety-uncontrollable states. In this paper, we present a quantitative approach to safety controller synthesis. Our approach makes it possible to compute a measure of safety, which quantifies how far from the unsafe set (respectively, how close to the safe set) one can stay when starting from a given controllable (respectively, uncontrollable) state. For finite transition systems, such a measure can be computed in finite-time using a functional fixed-point iteration. In addition, we show that the level sets of the functional fixed-point coincide with the maximal controlled invariant subsets of a parameterized family of sets and that one can synthesize a common safety controller for all the sets of the family. In the second part of the paper, we show how the approach can be used in the framework of abstraction-based synthesis to lift these results to infinite transition systems with finite abstractions. To illustrate the effectiveness of the approach, we show an application of the approach to a simple boost DC-DC converter.

ABSTRACT. In this paper, we develop a method for computing controlled invariant sets using Semidefinite Programming. We apply our method to the controller design problem for switching affine systems with polytopic safe sets. The task is reduced to a semidefinite programming problem by enforcing an invariance relation in the dual space of the geometric problem. The paper ends with an application to safety critical model predictive control.

ABSTRACT. Model Predictive Control (MPC) is a well consolidated technique to design optimal control strategies, leveraging the capability of a mathematical model to predict the system’s behavior over a predictive horizon. However, building physics-based models for large scale systems, such as buildings and process control, can be cost and time prohibitive. To overcome this problem we propose in this paper a methodology to exploit machine learning techniques (i.e. regression trees and random forests) in order to build a state-space switched affine dynamical model of a large scale system only using historical data. Finite Receding Horizon Control (RHC) setup using control-oriented data-driven models based on regression trees and random forests is presented as well. A comparison with an optimal MPC benchmark and a related methodology is provided on an energy management system to show the performance of the proposed modeling framework. Simulation results show that the proposed approach is very close to the optimum and provides better performance with respect to the related methodology in terms of cost function optimization.

ABSTRACT. We study the problem of stabilizing the origin of a plant, modeled as a discrete- time linear system, for which the communication with the controller is ensured by a wireless network. The transmissions over the wireless channel are characterized by the so-called stochastic allowable transmission intervals (SATI), that is a stochastic version of the maximum allowable transmission interval (MATI). Instead of deterministic transmissions, SATI gives stability conditions in terms of the cumulative probability of successful transmission over N steps. We argue that SATI is well-suited for wireless networked control systems to cope both with the stochastic nature of the communications and the design of energy-efficient communication strategies. Our objective is to synthesize a stabilizing state-feedback controller and SATI parameters simultaneously. We model the overall closed-loop system as a Markov jump linear system and we first provide linear conditions for the stability of the wireless networked control systems in a mean-square sense. We then provide linear matrix inequalities conditions for the design of state-feedback controllers to ensure stability of the closed-loop system. These conditions can be used to obtain both the controller and the SATI. A numerical example is presented to illustrate our results.

ABSTRACT. We address formally the problem of opinion dynamics when the agents of a social network (e.g., consumers) are not only influenced by their neighbors but also by an external influential entity referred to as a marketer. The influential entity tries to sway the overall opinion to its own side by using a specific influence budget during discrete-time advertising campaigns; consequently, the overall closed-loop dynamics becomes a linear-impulsive (hybrid) one. The main technical issue addressed is finding how the marketer should allocate its budget over time (through marketing campaigns) and over space (among the agents) such that the agents’ opinion be as close as possible to a desired opinion; for instance, the marketer may prioritize certain agents over others based on their influence in the social graph. The corresponding space-time allocation problem is formulated and solved for several special cases of practical interest. Valuable insights can be extracted from our analysis. For instance, for most cases we prove that the marketer has an interest in investing most of its budget at the beginning of the process and that budget should be shared among agents according to the famous water-filling allocation rule. Numerical examples illustrate the analysis.

ABSTRACT. This paper concerns an output-tracking technique based on a standalone integrator with variable gain. The control algorithm, recently proposed by the authors, appears to have a wide scope in linear and nonlinear systems while aiming at simple and efficient computations in the loop. For a class of memoryless systems it resembles a Newton-Raphson flow for solving the loop equation, but it is applicable to a broader class of dynamical systems. Furthermore, the technique is suitable for tracking constant as well as time-dependent reference signals, and its convergence performance is robust with respect to computational errors in the loop. The objective of this paper is to test the technique on a control problem arising in multi-agent systems. Specifically, we are motivated by regulating trajectories of follower agents by a lead agent in a platoon or swarm of multi-agent networks connected by the graph Laplacian. We study a particular example, which is challenging from the standpoint of control, with the aim of identifying the limits of the technique and investigating their possible extensions.

ABSTRACT. We present a hybrid system model describing the behavior of multiple agents cooperating to solve an optimal coverage problem under energy depletion and repletion constraints. The model captures the controlled switching of agents between coverage (when energy is depleted) and battery charging (when energy is replenished) modes. Our analysis contains three parts. The first part shows how the model guarantees the feasibility of the coverage problem by defining a guard function on each agent’s battery level to prevent it from dying on its way to a charging station. The second part provides two scheduling algorithms to solve the contention problem of agents competing for the only charging station in the mission space. The third part shows the optimality of the motion plan adopted in the proposed model.

ABSTRACT. This paper presents a mixed logical dynamical (MLD) approach for modelling a multi-energy system. The electrical and thermal energy streams are linked through the operation of combined cycle power plants (CCPPs). The MLD approach is used to develop detailed models of the gas turbines (GTs), steam turbines (STs) and boilers. The power trajectories followed by the GTs, STs and boilers during various start-up methods are also modelled. The utility of the developed model is demonstrated by formulating and solving an optimal scheduling problem to satisfy both electrical and thermal loads in the system. The cost benefit of including flexible loads in the scheduling problem formulation is demonstrated through suitable case studies.

ABSTRACT. In this paper a two-layer controller is proposed to tackle the building energy management problem for hybrid systems at different levels of abstraction and different time scales. In the upper layer a relaxed long term energy allocation problem with a large decision time step is defined, taking into account the energy prices, the comfort requirements, and a global power constraint. The discrete decision variables are considered only in the lower layer, where the continuous global solution computed by the first optimization is projected into local mixed-integer programming (MIP) tracking problems with a shorter prediction horizon and a higher sampling rate. To fulfill the building global power constraint each load has a specific priority to access the available power, following a non-iterative priority algorithm.

ABSTRACT. We present a new technique for verifying nonlinear and hybrid models with inputs. We observe that once an input signal is fixed, the sensitivity analysis of the model can be computed much more precisely. Based on this result, we propose a new simulation-driven verification algorithm and apply it to a suite of nonlinear and hybrid models of CMOS digital circuits under different input signals. The models are low-dimensional but with highly nonlinear ODEs, with nearly hundreds of logarithmic and exponential terms. Some of our experiments analyze the metastability of bistable circuits with very sensitive ODEs and rigorously establish the connection between metastability recovery time and sensitivity.

ABSTRACT. Time delays pose an important challenge in networked control systems, which are now ubiquitous. Focusing on switched systems, we introduce a framework that provides an upper bound for errors caused by switching delays. Our framework is based on approximate bisimulation, a notion that has been previously utilized mainly for symbolic (discrete) abstrac- tion of state spaces. Notable in our framework is that, in deriving an approximate bisimulation and thus an error bound, we use a simple incremental stability assumption (namely δ-GUAS) that does not itself refer to time delays. That this is the same assumption used for state-space discretization enables a two-step workflow for control synthesis for switched systems, in which a single Lyapunov-type stability certificate serves for two different purposes of state discretization and coping with time delays. We demonstrate the proposed framework with a boost DC-DC converter, a common example of switched systems.

ABSTRACT. In this paper, we consider the problem of symbolic model design for the class of incrementally stable switched systems. Contrarily to the existing results in the literature where switching is considered as periodically controlled, in this paper, we consider aperiodic time sampling resulting either from uncertain or event-based sampling mechanisms. Firstly, we establish sufficient conditions ensuring that usual symbolic models computed using periodic time-sampling remain approximately bisimilar to a switched system when the sampling period is uncertain and belongs to a given interval; estimates on the bounds of the interval are provided. Secondly, we propose a new method to compute symbolic models related by feedback refinement relations to incrementally stable switched systems, using an event-based approximation scheme. For a given precision, these event-based models are guaranteed to enable transitions of shorter duration and are likely to allow for more reactiveness in controller design. Finally, an example is proposed in order to illustrate the proposed results and simulations are performed for a Boost dc-dc converter structure.

ABSTRACT. In this paper, we explain how, under the one-sided Lipschitz (OSL) hypothesis, one can find an error bound for a variant of the Euler-Maruyama approximation method for stochastic switched systems. We then explain how this bound can be used to control stochastic switched switched system in order to stabilize them in a given region. The method is illustrated on several examples of the literature.