ABSTRACT. In event-triggered control systems, events are typically generated when a static function of the output (or state) of the system exceeds a given threshold. Recently, event-generators have been proposed that generate events based on an additional dynamic variable, with dynamics that depend on the output of the system. It is shown that these dynamic event-generators are able to guarantee the same performance as their static counterparts, while typically generating significantly fewer events. However, all dynamic event-generators available in literature require continuous measuring of the output of the plant, which is difficult to realize on digital platforms. In this paper, we propose new dynamic event-generators for linear systems, which require only periodic sampling of the output, and are therefore easy to implement on digital platforms. Based on hybrid modelling techniques combined with constructive designs of Lyapunov/storage functions for the resulting hybrid models, it is shown that these (dynamic periodic) event-generators lead to closed-loop systems which are globally exponentially stable (GES) with a guaranteed decay rate and L2-stable with a guaranteed L2-gain. The benefits of these new event-generators are also demonstrated via a numerical example.

ABSTRACT. Modern control synthesis methods that are capable of delivering safety guarantees typically rely on finding invariant sets. Computing and/or representing such sets becomes intractable for high-dimensional systems and often constitutes the main bottleneck of computational procedures. In this paper we instead analytically study a particular high-dimensional system and propose a control strategy that we prove renders a set invariant whenever it is possible to do so. The control problem---the mode-counting problem with two modes in one dimension---is inspired by scheduling of thermostatically controlled loads (TCLs) and exhibits a trade-off between local safety constraints and a global counting constraint. We improve upon a control strategy from the literature to handle heterogeneity and derive sufficient conditions for the strategy to solve the problem at hand. In addition, we show that the conditions are also necessary for the problem to have a solution, which implies a type of optimality of the proposed control strategy. We outline more general problem instances where the same control strategy can be implemented and we give sufficient (but not necessary) conditions for the closed-loop system to satisfy its specification. We illustrate our results on a TCL scheduling example.

ABSTRACT. Modern control systems are by and large implemented via digital microcontrollers, which are designed to work in an embedded environment, within a dynamical plant that can present physical components. This poses a new dimension to the problem of controllers synthesis, which is classically studied in the digital control literature. In this study, we plan to provide a principled approach to extend this literature in a number of directions: we focus on automated correct-by-construction synthesis algorithms, as opposed to verification (or validation) objectives over a designed architecture; and we encompass the complete range of approximations, related to time discretisation, quantisation effects, and finite-precision representations (with related rounding errors). To this end, we propose a CEGIS-based solution that uses inductive synthesis in conjunction with a digital verification algorithm to find a parametric solution for a digital controller given a continuous plant specification.

ABSTRACT. The problem of verifying properties of large, networked cyber-physical systems (CPS) is beyond the reach of most computational tools today. Two common "divide-and-conquer" techniques for CPS verification are assume-guarantee contracts from the formal methods literature and input-output properties from the control theory literature. Combining these two approaches, we first introduce the notion of a parametric assume-guarantee contract, which lets reason about system behavior abstractly in a parameter domain. We next show how a finite gain property can be encoded in this form and provide a generalized small-gain theorem for parametric assume-guarantee contracts.

This theorem recovers the classical small gain theorem as a special case and its derivation highlights the connection between assume-guarantee reasoning and small-gain results. This new small-gain theorem applies to behaviors beyond bounded deviation from a nominal point to include a fragment of linear temporal logic with parametrized predicates that can encode safety, recurrence, and liveness properties. Our results are validated with an example which certifies that the interconnection of two freeway segments experiences intermittent congestion.

ABSTRACT. Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and $\delta$-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter $\delta$ used in $\delta$-decidability when it is used to verify MTL properties. We present an application of this result in the form of an algorithm that generates new constraints to the $\delta$-decision procedure from falsification runs, which speeds up the verification run. We then establish new conditions under which robust testing, based on the robust semantics, is in fact a quasi-semidecision procedure. These results allow us to delimit what is possible with fast robustness-based methods, accelerate (near-)exhaustive verification, and further bridge the gap between verification and simulation.

ABSTRACT. We investigate a sampling-based method for optimal control of continuous-time and continuous-state (possibly nonlinear) systems under co-safe linear temporal logic specifications. We express the temporal logic specification as a deterministic, finite automaton (the specification automaton), and link the automaton's discrete transitions to the traversal of the continuous system state through specified regions over time. The optimal (hybrid) controller can be characterized by a set of coupled partial differential equations, however, it can be difficult to solve these equations in practice. Thus we propose a sampling based technique to solve the controller through an approximate value function. We adopt model reference adaptive search---an importance sampling based optimization algorithm---to identify weights of the approximate value function expressed in a finite set of basis functions. Under mild technical assumptions, the proposed algorithm converges, with probability one, to an optimal weight that ensures the satisfaction of temporal logic constraints, while minimizing an upper bound for the optimal cost. We demonstrate the correctness and efficiency of the method through numerical experiments, including temporal logic planning for a linear system, and a nonlinear mobile robot.

ABSTRACT. We present a technique to extend the notion of time-frequency logic to investigate abnormal behaviors of signals in both time and frequency domains using the continuous wavelet transform. Abnormal signal behaviors such as unexpected oscillations, called hunting behavior, can be challenging to capture in the time domain; however, these behaviors can be naturally captured in the time-frequency domain. We introduce the concept of parameter time-frequency logic and propose a parameter synthesis approach that can be used to classify hunting behavior. We perform a comparative analysis between the proposed algorithm, a support vector machine approach using linear classification, and a method that infers a signal temporal logic formula as a data classifier. We present experimental results based on data from a hydrogen fuel cell vehicle application and electrocardiogram data extracted from the MIT-BIH Arrhythmia Database

ABSTRACT. We provide conditions under which trajectory outcomes in mechanical systems subject to unilateral constraints depend piecewise–differentiably on initial conditions, even as the sequence of constraint activations and deactivations varies. This builds on prior work that provided conditions ensuring existence, uniqueness, and continuity of trajectory outcomes, and extends previous differentiability results ghat applied only to fixed constraint (de)activation sequences. We discuss extensions of our result and methods for assessing stability and controllability in piecewise–differentiable systems.

ABSTRACT. Differential Algebraic Equations (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs do not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive and well-founded mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

ABSTRACT. Bipedal robotic running remains a challenging benchmark in the field of control and robotics because of its highly dynamic nature and its necessarily underactuated hybrid dynamics. Previous results have achieved bipedal running experimentally with a combination of theoretical results and heuristic application thereof. In particular, formal analysis of the hybrid system stability is given based on a theoretical model, but due to the gap between theoretical concepts and experimental reality, excessive tuning is necessary to achieve experimental success. In this paper, we present a formal approach to bridge this gap, starting from theoretical gait generation to a provably stable control implementation, resulting in bipedal robotic running. We first use a large-scale optimization to generate an energy-efficient running gait, subject to hybrid zero dynamics conditions and feasibility constraints which incorporate practical limitations of the robot model based on physical conditions. The stability of the gait is formally guaranteed in the hybrid system model with an input to state stability (ISS) based control law. This implementation improves the stability under practical control limitations of the system, informing its practical implementation. Finally, the methodology is experimentally realized on the planar spring-legged bipedal robot, DURUS-2D, resulting in running at 1.75 m/s. The paper, therefore, presents a formal methodology that takes the first steps toward bridging the gap between theory and experiment.