Good knowledge of Python, familiar with (or eager to learn about) neural networks and deep learning libraries like tensorflow, eager to learn about basics of hybrid systems verification.
Hybrid automata (HA) are a formal model for cyber-physical systems, i.e., systems characterised by digital components (discrete) that control and interact with the physical environment (continuous). HAs have been applied to system designs in numerous domains including avionics, automotive, medical devices, and robotics. Formal verification of HAs can establish, with provable correctness guarantees, whether or not there exist a trajectory of the HA model that can reach some unsafe state. This kind of analysis is crucial for safety-critical applications, but computationally expensive, and thus, suitable only for offline design-time analysis.
In collaboration with the University of Trieste and Stony Brook University, we developed neural predictive monitoring (NPM), a method based on machine learning for predicting, at runtime, reachability of HA models. The method consists of three main components:
- A predictor, that is, a neural network model for reachability prediction, trained offline via supervision from a precise (expensive) reachability checker
- A rejection rule, which uses measures of prediction uncertainty to optimally decide whether or not a reachability prediction can be trusted
- An active learning procedure, which identifies the HA states for retraining that best improve the predictor and the rejection rule
In this project, you will consolidate existing code for NPM to produce a usable software tool, including interfacing with the main HA model checkers, evaluation on an extended benchmark of case studies, and efficient compilation into mobile and IoT devices.
- Henzinger, Thomas A. “The theory of hybrid automata.” Verification of Digital and Hybrid Systems. Springer, Berlin, Heidelberg, 2000. 265-292.
Bortolussi, Luca, et al. “Neural Predictive Monitoring.” International Conference on Runtime Verification. Springer, Cham, 2019.
- Phan, Dung, et al. “Neural state classification for hybrid systems.” International Symposium on Automated Technology for Verification and Analysis. Springer, Cham, 2018.
- Proceedings of ARCH 19 (collection of HA benchmarks and tools)
- Two introductory tutorials on HA from the Georgia Tech module on “Control of Mobile Robots”: video 1 and video 2