We present a novel framework for formal control of uncertain discrete-time switched stochastic systems against probabilistic reach-avoid specifications. In particular, we consider stochastic systems with additive noise, whose distribution lies in an ambiguity set of distributions that are ε − close to a nominal one according to the Wasserstein distance. For this class of systems we derive control synthesis algorithms that are robust against all these distributions and maximize the probability of satisfying a reach-avoid specification, defined as the probability of reaching a goal region while being safe. The framework we present first learns an abstraction of a switched stochastic system as a robust Markov decision process (robust MDP) by accounting for both the stochasticity of the system and the uncertainty in the noise distribution. Then, it synthesizes a strategy on the resulting robust MDP that maximizes the probability of satisfying the property and is robust to all uncertainty in the system. This strategy is then refined into a switching strategy for the original stochastic system. By exploiting tools from optimal transport and stochastic programming, we show that synthesizing such a strategy reduces to solving a set of linear programs, thus guaranteeing efficiency. We experimentally validate the efficacy of our framework on various case studies, including both linear and non-linear switched stochastic systems. Our results represent the first formal approach for control synthesis of stochastic systems with uncertain noise distribution.
In real world applications, uncertain parameters are the rule rather than the exception. We present a reachability algorithm for linear systems with uncertain parameters and inputs using set propagation of polynomial zonotopes. In contrast to previous methods, our approach is able to tightly capture the non-convexity of the reachable set. Building up on our main result, we show how our reachability algorithm can be extended to handle linear time-varying systems as well as linear systems with time-varying parameters. Moreover, our approach opens up new possibilities for reachability analysis of linear time-invariant systems, nonlinear systems, and hybrid systems. We compare our approach to other state of the art methods, with superior tightness on two benchmarks including a 9-dimensional vehicle platooning system.
DNN-based Adaptive Cruise Control (ACC) systems are very convenient but also safety critical. Although prior work has explored physical adversarial attacks on DNN models, those attacks are mostly static and their effects on a real-world ACC system are not clear. In this work, we propose the first end-to-end attack on ACC systems, and we test the safety indication on the state-of-the-art ACC products. The experimental results show that our approach can make the vehicle driving with ACC accelerate unsafely and cause a rear-end collision.
State-of-the-art industrial IoT solutions struggle to handle applications in which timing is important and deterministic event ordering is crucial. We illustrate this on the basis of a simple parking lot occupancy sensing use case that is easy to explain but virtually impossible to implement using commercially available IoT infrastructure. In this paper, we compare an implementation using AWS IoT Core against one using Lingua Franca, a time-centric coordination language for constructing deterministic concurrent and distributed reactive software. Our preliminary evaluation shows that Lingua Franca can reliably address our use case.
Cyber-physical systems (CPSs) are complex systems comprised of computational processes, communication networks, and elements interacting with the physical world. The design of the CPSs involves many domain-specific tools and design flows created by engineers with diverse domain knowledge. As the scale of the systems increases, the heterogeneity nature of CPS design prolongs the CPS design process, making exhaustive design-space exploration infeasible. The symbiotic design methodology, in which the designers interact with optimization tools during the design process, is therefore promising to facilitate the design process by performing design exploration in a properly restricted design space. We present a symbiotic design methodology, which explores the design space iteratively and optimizes the system by exploiting the collaboration between designers and tools. The optimization tools perform the design space exploration, while the human designers use their expertise to guide the exploration by restricting the design space. Experimental results based on a robot car configuration problem and an unmanned aerial vehicle design problem show that the methodology can efficiently and effectively discover unconventional designs while optimizing the design objectives.
