ABSTRACT. Ambient Intelligence has been a goal for more than 20 years. Are we getting close? What if we focus ambient intelligence on smart healthcare, are we getting close? What role does CPS play in ambient intelligence? This talk is motivated by these questions. Various challenges, research directions, and research results from my group’s work will be used to (partially) address these themes for smart healthcare. The talk includes discussions of the vision, the role of CPS, cognitive assistants on wearables, solutions supporting mental health, and lessons learned from real deployments. There is also a brief discussion on two key challenges: the need for robust models and dealing with uncertainties due to the environment and human behaviors.

ABSTRACT. Self-triggered controllers have the potential to improve the state-of-the-art of Cyber-Physical Systems (CPSs) by enhancing the performance of the underlying closed-loop control systems. However, a major concern in deploying a self-triggered controller in a safety-critical CPS is that the stabilizing self-triggered controller may not always guarantee the satisfaction of the safety constraints. We propose a self-triggered control scheme that deals with the safe scheduling of control tasks for uncertain continuous-time linear systems. We derive a computationally efficient scheduling function that computes an upper bound on the next sampling period as a function of the current state in the presence of additive disturbance. To deal with the conservativeness of the reachability analysis, we compute a large sequence of reachable sets offline and use these precomputed sets to derive a low-complexity online scheduling function that computes sufficiently large bounds in real-time. We evaluate our algorithm on three high-dimensional benchmark control systems, where two of the examples have a twelve-dimensional joint state plus feedback input. Experimental results demonstrate that our self-triggered control algorithm guarantees the safety of the closed-loop control system through negligible online computation, establishing the feasibility of its practical implementation.

ABSTRACT. As part of the development of Lyapunov techniques for cyber-physical systems, we study and compare graph-based stability certificates with respect to their conservatism. Previous work have highlighted the dependence of this ordering with respect to the properties of the chosen template of candidate Lyapunov functions. We extend here previous results from the literature to the case of templates closed under addition, as for instance the set of quadratic functions. In this context, we provide a characterization of the ordering, using an approach based on abstract operations on graphs, called lifts, which encode in a combinatorial way the algebraic properties of the chosen template. We finally provide a numerical method to algorithmically check the ordering relation.

ABSTRACT. This short paper presents a lazy symbolic output-feedback controller synthesis algorithm for state-based safety specifications over large transition systems. The novel idea of our approach is to integrate an iterative algorithm for observer design with an online adaptable safety controller synthesis algorithm. This allows us to iteratively update the safety controller to observer refinements and to guide these refinements by the existing controller. This results in efficient lazy synthesis of a safety controller whose domain increases with the time spent in synthesis. We present simulation results for a synthetic robot motion planning example showing the benefits of our algorithm compared to the standard approach.

ABSTRACT. Hybrid system identification techniques seek hybrid system models  of various forms that can approximate given observation data involving the states and outputs of the system.  They promise to derive relatively simple dynamical models that can be interpreted and analyzed using many of the available tools for safety, stability and controller synthesis developed by the HSCC community. Although hybrid system identification techniques have been well-studied,   the problem itself is known to be computationally hard. We motivate the continued need for efficient algorithms for identifying hybrid system models,  despite the successes enjoyed by neural network-based dynamical models identified using  variants of stochastic gradient descent. We present some recent results that combine  ideas from  areas such as approximation algorithms and non-smooth optimization.  Finally, we will conclude by examining some of the key open problems in this area. 

Based on joint work with Guillaume Berger, Monal Narasimhamurthy, Kandai Watanabe and Morteza Lahijanian.

ABSTRACT. We prove continuity of a large class of thresholded mode-switched ODEs, which we view as a function of mode-switch input signals to solutions that are discretized via constant thresholds. This includes classical hybrid systems as well as recent digital circuit delay models. We further detail several instances of these systems and discuss the implications of our continuity result.

ABSTRACT. We present a novel framework for formal control of discrete-time switched stochastic systems with additive noise of uncertain distri- bution against probabilistic reach-avoid specifications. In particular, we assume that the noise distribution lies in an ambiguity set of distributions that are epsilon−close to a nominal one according to the Wasserstein distance. We derive control synthesis algorithms that are robust against all these distributions and maximize the proba- bility that the system satisfies the specification. The framework we present first learns an abstraction of a switched stochastic system as a robust Markov decision process by accounting for both the stochas- ticity of the system and the uncertainty in the noise distribution. Then, it synthesizes a strategy on the resulting robust MDP that maximizes the satisfaction probability of a reach-avoid specifica- tion and is robust to all uncertanity in the system. This strategy is then refined into a switching strategy for the original stochastic system. By exploiting tools from optimal transport, we show that syntesizing such a strategy reduces to solving a set of linear pro- grams, thus guaranteeing efficiency. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems showing the efficacy of our framework.

ABSTRACT. Interval Markov Decision Processes (IMDPs) are uncertain Markov models, where the transition probabilities belong to intervals. Recently, there has been a surge of research on employing IMDPs as abstractions of stochastic systems for control synthesis. However, due to the absence of algorithms for synthesis over IMDPs with continuous action-spaces, the action-space is assumed discrete a-priori, which is a restrictive assumption for many applications. Motivated by this, we introduce continuous-action IMDPs (caIMDPs), where the bounds on transition probabilities are functions of the action variables, and study value iteration for maximizing expected cumulative rewards. Specifically, we show that solving the max-min problem associated to value iteration is equivalent to solving $|Q|$ max problems, where $|Q|$ is the number of states of the caIMDP. Then, exploiting the simple form of these max problems, we identify cases where value iteration over caIMDPs can be solved efficiently (e.g., with linear or convex programming). We also gain other interesting insights: e.g., in the case where the action set $A$ is a polytope and the transition bounds are linear, synthesizing over a discrete-action IMDP, where the actions are the vertices of $A$, is sufficient for optimality. We demonstrate our results on a numerical example. Finally, we include a short discussion on employing caIMDPs as abstractions for control synthesis.

ABSTRACT. We present SySCoRe, a MATLAB toolbox that synthesizes controllers for stochastic continuous-state systems to satisfy temporal logic specifications. Starting from a system description and a co-safe temporal logic specification, SySCoRe provides all necessary functions for synthesizing a robust controller and quantifying the associated formal robustness guarantees. It distinguishes itself from other available tools by supporting nonlinear dynamics, complex co-safe temporal logic specifications over infinite horizons and model-order reduction. To achieve this, SySCoRe first generates a finite-state abstraction of the provided model and performs probabilistic model checking. Then, it establishes a probabilistic coupling to the original stochastic system encoded in an approximate simulation relation, based on which a lower bound on the satisfaction probability is computed. SySCoRe provides non-trivial lower bounds for infinite-horizon properties and unbounded disturbances since its computed error does not grow linear in the horizon of the specification. It exploits a tensor representation to facilitate the efficient computation of transition probabilities. We showcase these features on several benchmarks and compare the performance of the tool with existing tools.