Visible to the public Resilient Control of Cyber-Physical Systems with Distributed Learning - April 2020Conflict Detection Enabled

PI(s) and Co-PI(s): Sayan Mitra and Geir Dullerud and Sanjay Shakkotai (U. Texas at Austin)

Researchers: Dawei Sun and Negin Musavi

HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.

Resiliency: Effective verification of safety and security properties of autonomous and cyber-physical systems

Metrics: How much data is necessary to achieve a certain level of confidence regarding a safety/security claim

PUBLICATIONS
Papers written as a result of your research from the current quarter only.

Working paper:

Optimistic Optimization for Statistical Model Checking with Regret Bounds, Musavi, Sun, Mitra, Shakkottai, and Dullerud, April 2020. Available online from https://arxiv.org/abs/1911.01537

HOOVER tool available from: https://github.com/sundw2014/HooVer

Related recent publications:

Differential Privacy for Sequential Algorithms, Yu Wang, Hussein Sibai, Sayan Mitra, and Geir Dullerud, submitted.

Verifying PCTL Specifications on Markov Decision Processes via Reinforcement Learning, Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan and Geir Dullerud, submitted.

Convergence Guarantees of Policy Optimization Methods for Markovian Jump Linear Systems, Joao Porto, Bin Hu, and Geir Dullerud, to appear in Proceedings of the American Control Conference, 2020.

Policy Learning of MDPs with Mixed Continuous/Discrete Variables: A Case Study on Model-Free Control of Markovian Jump Systems, Joao Porto, Bin Hu, and Geir Dullerud, to appear in the Proceedings of the Learning for Dynamics and Control Workshop, 2020.

The Gossiping Insert-Eliminate Algorithm for Multi-Agent Bandits, Ronshee Chawla, Abishek Sankararaman, Ayalvadi J. Ganesh and Sanjay Shakkottai, accepted to appear in AISTATS 2020, Palermo, Sicily, June 2020.

Data-driven safety verification of complex cyber-physical systems, Chuchu Fan and Sayan Mitra. A chapter in the book titled Design Automation for Cyber-Physical Systems, edited by Mohammad Abdullah Al Faruquqe and Arquimedes Canedo, pages 107-143, Springer, 2019.

Using symmetry transformations in equivariant dynamical systems for their safety verification Hussein Sibai, Navid Mokhlesi and Sayan Mitra; accepted for publication in the proceedings of the Seventeenth International Symposium on Automated Technology for Verification and Analysis (ATVA), October 28-31, 2019, Taipei City, Taiwan. Nominated for best paper award

KEY HIGHLIGHTS
Each effort should submit one or two specific highlights. Each item should include a paragraph or two along with a citation if available. Write as if for the general reader of IEEE S&P.
The purpose of the highlights is to give our immediate sponsors a body of evidence that the funding they are providing (in the framework of the SoS lablet model) is delivering results that "more than justify" the investment they are making.

Three PhD students have been recruited and are dedicating their research time to the project. We have formulated a new direction of scientific enquiry into 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. We have shown how these optimization algorithms can be used effectively for statistical model checking of markov decision processes. We have build a suite of benchmarks related to online safety analysis of autonomous and semi-autonomous vehicles. Our initial results are very promising as the data usage and the running time of our 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.

Sayan Mitra received a Siebel Energy Institute Fellowship, 2019.

Mitra gave an invited lecture at the 10th Anniversary of the Distinguished Colloquium Series of University of Maryland (sponsored by Booz, Allen, and Hamilton) on Verification for safe autonomy: Challenges and recent developments, May 3rd, 2019.

COMMUNITY ENGAGEMENTS

Hyper-parameter Tuning for ML Models: A Monte-Carlo Tree Search (MCTS) Approach. EE Seminar, Indian Institute of Science, lecture given by Sanjay Shakkottai, January 2, 2020.

Invited Speaker, "On the Throughput vs Accuracy Trade-Off for Streaming Unsupervised Classification", Sanjay Shakkottai, Workshop on Learning Theory 2, Tata Institute of Fundamental Research, January 3, 2020.

Invited Speaker, Formal Methods in Mathematics Workshop, Mathematics, Carnegie Mellon University, "Learning and Statistical Validation of Complex Cyber-PhysicalSystems", Geir Dullerud, January 7th, 2020 on logic in engineering systems.

CES Symposium Lecture, University of Texas, Austin, "Statistical Validation and Principle-Based Simulation of Complex Cyber-Controlled Systems", Geir Dullerud, December 3rd, 2019.

EDUCATIONAL ADVANCES

The second edition of PI Mitra's new course Principles of Safe Autonomy at University of Illinois is coming to a successful conclusion this semester with a larger class size (38 students) despite the setbacks from the COVID19 outbreak. The course takes a deep dive into the seminal topics in object recognition, localization, decision making, path planning, and safety verification. Graduate and undergraduate students from ECE and CS are completing the course. The course team has designed 6 New programming assignments involving topics such as lane detection, road-sign recognition, localization with particle filters, decision making with reinforcement learning, path planning with rapidly expanding random trees, and safety verification using simulation-driven proofs. With support from the Illinois Center for Autonomy, we have setup a laboratory with 7 workstations with GPUs for performing simulation-based experiments. The students are using ROS, Gazebo, for testing their programming assignments. Find out more about the safe autonomy course and the student projects at https://publish.illinois.edu/safe-autonomy/