ABSTRACT. In this work, we propose a stratified sampling method to statistically check Probabilistic Computation Tree Logic (PCTL) formulas on discrete-time Markov chains with sequential probability ratio test. Distinct from previous statistical verification methods using independent Monte Carlo sampling, our algorithm uses stratified samples that are negatively correlated, thus give lower variance. The experiments demonstrate that the new algorithm uses a smaller number of samples for a given confidence level on several benchmark examples.

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. It is well known that for switched systems the overall dynamics can be unstable despite stability of all individual modes. We show that this phenomenon can indeed occur for a linearized DAE model of power grids. By making certain topological assumptions on the power grid, we can ensure stability under arbitrary switching for the linearized DAE model.

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 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. 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. 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 discuss the problem of efficient fluid mixing which is tackled by means of (approximate) dynamic programming from a switched systems perspective. In current practice, typically pre-determined periodic mixing protocols are used. As we will show in this paper, feedback control can be used to improve mixing significantly. To make this control problem tractable, temporal and spatial discretization is used by means of the cell-mapping method on the original infinite-dimensional fluid models. This translates the original control problem into the design of a (sub)optimal switching law that determines discrete mixing actions for a discrete-time switched linear system. Exploiting this switched systems perspective, a novel feedback law for mixing fluids is proposed inspired by suboptimal rollout policies in dynamic programming contexts. By design, this feedback law for mixing guarantees a performance improvement over any given (open-loop) periodic mixing protocol. This new design methodology is validated by means of simulations for the benchmark journal bearing flow showing improved performance with respect to periodic mixing strategies.

ABSTRACT. In this work, we investigate some Razumikhin-type criteria for the uniform global practical asymptotic stability on arbitrary time domains, for time-varying dynamic equations. Using Lyapunov-type functions on time scales, we develop appropriate inequalities ensuring that trajectories decay to the neighborhood of the trivial solution asymptotically. Some numerical examples are discussed to illustrate our results.

ABSTRACT. We introduce a new formalism of higher-dimensional timed automata, based on van Glabbeek’s higher-dimensional automata and Alur’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also show how to use tensor products to combat state-space explosion and how to extend the setting to higher-dimensional hybrid automata.

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. The time scale theory is introduced to study the stability of a class of switched linear systems on non-uniform time domains, where the dynamical system commutes between a continuous-time linear subsystem and a discrete-time linear subsystem during a certain period of time. Without assuming that matrices are pairwise commuting, some conditions are derived to guarantee the exponential stability of the switched system by considering that the continuous-time subsystem is stable and the discrete-time subsystem can be stable or unstable. Some examples show the effectiveness of the proposed scheme.

ABSTRACT. Chance-constrained optimization problems optimize a cost function in the presence of probabilistic constraints. They are convex in very special cases and, in practice, they are solved using approximation techniques. In this paper, we study approximation of chance constraints for the class of probability distributions that satisfy a concentration of measure property. We show that using concentration of measure, we can transform chance constraints to constraints on expectations, which can then be solved based on scenario optimization. Our approach depends solely on the concentration of measure property of the uncertainty and does not require the objective or constraint functions to be convex. We also give bounds on the required number of scenarios for achieving a certain confidence. We demonstrate our approach on a non-convex chanced-constrained optimization, and benchmark our technique against alternative approaches in the literature on chance-constrained LQG problem.

ABSTRACT. Controller synthesis techniques based on symbolic abstractions appeal by producing correct-by-design controllers, under intricate behavioural constraints. Yet, being relations between abstract states and inputs, such controllers are immense in size, which makes them futile for embedded platforms. Control-synthesis tools such as PESSOA, SCOTS, and CoSyMA tackle the problem by storing controllers as binary decision diagrams (BDDs). However, due to redundantly keeping multiple inputs per-state, the resulting controllers are still too large. In this work, we first show that choosing an optimal controller determinization is an NP-complete problem. Further, we consider the previously known controller determinization technique and discuss its weaknesses. We suggest several new approaches to the problem, based on greedy algorithms, symbolic regression, and (muli-terminal) BDDs. Finally, we empirically compare the techniques and show that some of the new algorithms can produce up to ≈ 85% smaller controllers than those obtained with the previous technique.

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. 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. 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. Component-driven proof automation (CDPA) exploits component structure to automate deductive verification of large-scale hybrid systems with non-trivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolchain for designing and verifying safety of 2-dimensional roller coaster track designs. Specifically, we verify velocity and acceleration bounds. CoasterX starts with a graphical front-end for point-and-click design of tracks. The CoasterX back-end then automatically specifies and verifies the track in differential dynamic logic (dL) with a custom procedure built in the KeYmaera X theorem prover. We show that the CDPA approach scales, testing real coasters of up to 56 components.

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. 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. 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. Motivated by the synthesis of controllers from high-level temporal specifications, we present two algorithms to compute dominant strategies for continuous two-player zero- sum games based on the Counter-Example Guided Inductive Synthesis (CEGIS) paradigm. In CEGIS, we iteratively propose candidate dominant strategies and find counterexamples. For scalability, past work has constrained the number of counterexamples used to generate new candidates, which leads to oscillations and incompleteness, even in very simple examples. The first algorithm combines Satisfiability Modulo Theory (SMT) solving with optimization to efficiently implement CEGIS. The second abstracts previously refuted strategies, while maintaining a finite counterexample set. We characterize sufficient conditions for soundness and termination, and show that both algorithms are sound and terminate. Additionally, the second approach can be made complete to within an arbitrary factor. We conclude by comparing across different variants of CEGIS.

ABSTRACT. This paper is concerned with a compositional approach for constructing finite abstractions (a.k.a. finite Markov decision processes) of interconnected discrete-time stochastic control systems. The proposed framework is based on a notion of so-called stochastic simulation function enabling us to use an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the distance in probability between the interconnection of stochastic control subsystems and that of their (finite or infinite) abstractions. In the second part of the paper, we construct finite abstractions together with their corresponding stochastic simulation functions for the class of linear stochastic control systems. We apply our results to the temperature regulation in a circular building by constructing compositionally a finite abstraction of a network containing 1000 rooms. We use the constructed finite abstractions as substitutes to synthesize policies compositionally regulating the temperature in each room for a bounded time horizon.

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. This work introduces a new abstraction technique for reducing the state space of large, discrete-time labelled Markov chains. The abstraction leverages the semantics of interval Markov decision processes and the existing notion of approximate probabilistic bisimulation. Whilst standard abstractions make use of abstract points that are taken from the state space of the concrete model and which serve as representatives for sets of concrete states, in this work the abstract structure is constructed considering abstract points that are not necessarily selected from the states of the concrete model, rather they are a function of these states. The resulting model presents a smaller one-step bisimulation error, when compared to a like-sized, standard Markov chain abstraction. We outline a method to perform probabilistic model checking, and show that the computational complexity of the new method is comparable to that of standard abstractions based on approximate probabilistic bisimulations.

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.

ABSTRACT. Abstraction-based synthesis techniques are limited to systems with moderate size. Thus to contribute towards scalability of these techniques, in this paper we propose a compositional abstraction-based synthesis for cascade interconnected discrete-time control systems. Given a cascade interconnection of several components, we provide results on the compositional construction of finite abstractions based on the notion of approximate cascade composition. Then, we provide a compositional controller synthesis for cascade interconnection. Finally, we demonstrate the applicability and effectiveness of the results using a numerical example and compare it with different abstraction and controller synthesis schemes.

ABSTRACT. This paper presents a control synthesis algorithm for dynamical systems to satisfy specifications given in a fragment of linear temporal logic. It is based on an abstraction- refinement scheme with nonuniform partitions of the state space. A novel encoding of the resulting transition system is proposed that uses binary decision diagrams for efficiency. We discuss several factors affecting scalability and present some benchmark results demonstrating the effectiveness of the new encodings. These ideas are also being implemented on a publicly available prototype tool, ARCS, that we briefly introduce in the paper.

ABSTRACT. Building Automation Systems (BAS) are exemplars of Cyber-Physical Systems (CPS), incorporating digital control architectures over underlying continuous physical processes. We provide a modular model library for BAS drawn from expertise developed on a real BAS setup. The library allows to build models comprising either physical quantities or digital control modules. The structure, operation, and dynamics of the model can be complex, incorporating (i) stochasticity, (ii) non-linearities, (iii) numerous continuous variables or discrete states, (iv) various input and output signals, and (v) a large number of possible discrete configurations. The modular composition of BAS components can generate useful CPS benchmarks. We display this use by means of three realistic case studies, where corresponding models are built and engaged with different analysis goals. The benchmarks, the model library and associated data collected from the BAS setup at the University of Oxford, are kept on-line at https://github.com/ natchi92/BASBenchmarks

ABSTRACT. The formal verification and controller synthesis for general Markov decision processes (gMDPs) that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximate abstractions. In this paper, we contribute to the state of the art of control synthesis for temporal logic properties by computing and quantifying a less conservative gridding of the continuous state space of linear stochastic dynamic systems and by giving a new approach for control synthesis and verification that is robust to the incurred approximation errors. The approximation errors are expressed as both deviations in the outputs of the gMDPs and in the probabilistic transitions.

ABSTRACT. We consider the stability and the input-output analysis problems of a class of large-scale hybrid systems composed of continuous dynamics coupled with discrete dynamics defined over finite alphabets, e.g., deterministic finite state machines (DFSMs). This class of hybrid systems can be used to model physical systems controlled by software. For such classes of systems, we use a method based on dissipativity theory for compositional analysis that allows us to study stability, passivity and input-output norms. We show that the certificates of the method based on dissipativity theory can be computed by solving a set of semi-definite programs. Nonetheless, the formulation based on semi-definite programs become computationally intractable for relatively large number of discrete and continuous states. We demonstrate that, for systems with large number of states consisting of an interconnection of smaller hybrid systems, accelerated alternating method of multipliers can be used to carry out the computations in a scalable and distributed manner. The proposed methodology is illustrated by an example of a system with 60 continuous states and 18 discrete states.

ABSTRACT. The goal of this paper is to study sufficient conditions to stabilize an autonomous discrete-time switched system, for which the switching law should belong to a constrained language characterized by a nondeterministic automaton. Based on a decomposition into strongly connected components of the automaton, it is shown that it suffices to consider only a nontrivial strongly connected component. Sufficient conditions are provided as a set of Linear Matrix Inequalities (LMIs) related to the automaton states and associated with a min-switching strategy. Equivalence with the periodic stabilization is investigated. A numerical example is provided to illustrate the main result.

ABSTRACT. This paper studies estimation of reach probability for a generalized stochastic hybrid system (GSHS). For diffusion processes a well-developed approach in reach probability estimation is to introduce a suitable factorization of the reach probability and then to estimate these factors through simulation of an Interacting Particle System (IPS). The theory of this IPS approach has been extended to arbitrary strong Markov processes, which includes GSHS executions. Because Monte Carlo simulation of GSHS particles involves sampling of Brownian motion as well as sampling of random discontinuities, the practical elaboration of the IPS approach for GSHS is not straightforward. The aim of this paper is to elaborate the IPS approach for GSHS by using complementary Monte Carlo sampling techniques. For a simple GSHS example, it is shown that and why the specific technique selected for sampling discontinuities can have a major influence on the effectiveness of IPS in reach probability estimation.

ABSTRACT. Arguments are presented in favor of modeling sewer systems and in particular Dutch sewer systems as a sampled data system with events. Basic limitations on controlling these systems when ignoring their hybrid nature are stated. The traditional control scheme for the Dutch systems is given as an example of event driven local control. Basic limitations on systems using a sampled data approach without an event driven component are derived. To provide context a brief description of a sampled data controller for a sewer system based on set-point tracking is given. This is followed by an explanation of how the absence of event driven control limits its effectiveness.

ABSTRACT. A new algorithm of motion planning based on set-membership approach is presented. The goal of this algorithm is to find a safe and optimal path taking into account various sources of bounded uncertainties on the dynamical model of the plant, on the model of the environment, while being robust with respect to the numerical approximations introduced by numerical integration methods. The main approach is based on a sliding horizon method to predict the behavior of the system allowing the computation of an optimal path. As an example, the motion planning algorithm is applied to an Autonomous Underwater Vehicle (AUV) case study, showing the benefit of the proposed approach.

ABSTRACT. We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.

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. The synthesis of controllers guaranteeing linear temporal logic specifications on partially observable Markov decision processes (POMDP) via their belief models causes computational issues due to the continuous spaces. In this work, we construct a finite-state abstraction on which a control policy is synthesized and refined back to the original belief model. We introduce a new notion of label- based approximate stochastic simulation to quantify the deviation between belief models. We develop a robust synthesis methodology that yields a lower bound on the satisfaction probability, by compensating for deviations a priori, and that utilizes a less conservative control refinement.

ABSTRACT. In this paper, we present extensions to Unmanned Systems Autonomy Services (UxAS) to handle mission specifications that require a synchronization of task execution. UxAS uses Process Algebra (PA) as a formal language to specify mission requirements for unmanned aerial vehicle (UAV) operations. However, the current implementation of PA in UxAS utilizes assigned semantics which does not guarantee the order of task completion and is unable to provide a mission planning required vehicle-synchronization. To enable the capability of UxAS in operating synchronized mission specifications, we introduce a notion of Synchronized Process Algebra (SPA) which extends PA by adding a synchronized composition operator to the syntax of PA. Such an operator allows us to specify the task’s duration and enforce the next task is executed after the previous one has terminated. Moreover, we provide a new service in UxAS, called Temporal Service (TS) to control the flow of the planning process with respect to timing specifications. We apply SPA and TS to specify and operate the mission specification of a forest fire rescue scenario required the synchronized arrivals of multiple UAVs.

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. 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. Value functions arising from dynamic programming can be used to synthesize optimal control inputs for general nonlinear systems with state and/or input constraints; however, the inputs generated by steepest descent on these value functions often lead to chattering behavior. In [Traft & Mitchell, 2016] we proposed the Gradient Sampling Particle Filter (GSPF), which combines robot state estimation and nonsmooth optimization algorithms to alleviate this problem. In this paper we extend the GSPF to velocity controlled unicycle (or equivalently differential drive) dynamics. We also show how the algorithm can be adapted to classify whether an exogenous input—such as one arising from shared human-in-the-loop control—is desirable. The two algorithms are demonstrated on a ground robot.

ABSTRACT. In this paper, we introduce operators, semantics, and conditions that, when possible, are solution-independent to guarantee basic temporal logic specifications for hybrid dynamical systems. Employing sufficient conditions for forward invariance and finite time attractivity of sets for such systems, we derive such sufficient conditions for the satisfaction of formulas involving temporal operators and atomic propositions. Furthermore, we present how to certify formulas that have more than one operator. Academic examples illustrate the results throughout the paper.

ABSTRACT. This paper considers control synthesis for polynomial control systems. The developed method leans upon Lyapunov stability and Bernstein certificates of positivity. We strive to develop an algorithm that computes a polynomial control and a polynomial Lyaponov function in the simplicial Bernstein form. Subsequently, we reduce the control synthesis problem to a finite number of evaluations of a polynomial within Bernstein coefficient bounds representing controls and Lyapunov functions. As a consequence, the equilibrium is asymptotically stable with this control.

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. Reachability analysis is a powerful tool which is being used extensively and efficiently for the analysis and control of dynamical systems, especially when linear systems and convex sets are involved. In this note, we investigate whether exact or approximate reachability operations can be performed efficiently for the affine–semialgebraic setting, that is when we are dealing with general affine dynamics and basic semialgebraic sets. We show that it is partially true, we pinpoint the underlying challenges when this is not possible and indicate some directions for this case.

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. 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. 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.