Spotlight on Lablet Research #20 - Resilient Control of Cyber-Physical Systems with Distributed Learning

Spotlight on Lablet Research #20 -

Resilient Control of Cyber-Physical Systems with Distributed Learning

Lablet: University of Illinois at Urbana-Champaign
Sub-Lablet: University of Texas at Austin (UT Austin)

The goal of this project is to bring together techniques from Machine Learning (ML) and formal verification to improve resiliency and risk-reduction in autonomous systems and Cyber-Physical Systems (CPS) (e.g., autonomous vehicles, drones, and manufacturing systems). Verification solves the problem of catching design bugs and vulnerabilities, and it can provide high-assurance guarantees. Led by Principal Investigator (PI) Sayan Mitra and Co-PIs Geir Dullerud and Sanjay Shakkottai, the research team is exploring how existing model-based verification methods like statistical model checking and reachability analysis can be improved using ML techniques like multi-armed bandits algorithms. The research aims to provide theoretical bounds of how testing and validation budgets can be best allocated based on metrics like sample complexity (i.e., how many test samples are needed to draw to answer a risk/resiliency question). Thus, the project would expand the range of applicability as well as guide optimal resource usage for verification.

This project was motivated by the complex interaction of dynamics and decision-making, given that the integration of hundreds of components exposes CPS to I/O attacks and component compromises. This project addresses resiliency and risk-reduction in CPS through rigorous monitoring and verification, going beyond model-based approaches. In going beyond model-based approaches, researchers exploit models when it makes sense but otherwise get (gracefully degrading) guarantees with black-box executables. The team also focuses on the marginal benefits of models/executable fidelity in security and risk reduction. The developed approaches are being evaluated on case studies drawn from autonomous vehicles and aircraft systems.

The research team has formulated a new direction of scientific inquiry into the safety and security analysis of systems. The approach relies on distributed and sample-efficient optimization techniques that have been developed in the context of the multi-armed bandit problem. Researchers have shown how these optimization algorithms can be used effectively for statistical model checking of Markov decision processes. They have built a suite of benchmarks related to online safety analysis of autonomous and semi-autonomous vehicles, and initial results are very promising as the data usage and the running time of the algorithms can be several orders of magnitude better than existing model checking approaches such as Storm and Prism. The prototype tool has been made available online. In a related thread, researchers have also developed an algorithm for probabilistic reachability analysis that can work on black-box dynamical systems.

Additional information on this project can be found here.