# Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components

arXiv: https://arxiv.org/abs/2202.03360 · HTML: https://mlsanity.com/paper/2202.03360/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 47 references that are in the map.
- First posted on arXiv 7 Feb 2022.

## Builds on (most cited first, 21 of 21)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [On Calibration of Modern Neural Networks](https://mlsanity.com/paper/1706.04599/) (2017)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [A Survey of Deep Learning Techniques for Autonomous Driving](https://mlsanity.com/paper/1910.07738/) (2019)
- [Distribution-Free, Risk-Controlling Prediction Sets](https://mlsanity.com/paper/2101.02703/) (2021)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Multivariate Confidence Calibration for Object Detection](https://mlsanity.com/paper/2004.13546/) (2020)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Uncertainty Quantification with Statistical Guarantees in End-to-End Autonomous Driving Control](https://mlsanity.com/paper/1909.09884/) (2019)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Assuring the Machine Learning Lifecycle: Desiderata, Methods, and Challenges](https://mlsanity.com/paper/1905.04223/) (2019)
- [Conformal Bayesian Computation](https://mlsanity.com/paper/2106.06137/) (2021)
- [Deep Learning for Large-Scale Traffic-Sign Detection and Recognition](https://mlsanity.com/paper/1904.00649/) (2019)
- [DeepTake: Prediction of Driver Takeover Behavior using Multimodal Data](https://mlsanity.com/paper/2012.15441/) (2020)
- [Optimal Cost Almost-sure Reachability in POMDPs](https://mlsanity.com/paper/1411.3880/) (2014)
- [Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications](https://mlsanity.com/paper/1409.3360/) (2014)
- [Detection and Mitigation of Rare Subclasses in Deep Neural Network Classifiers](https://mlsanity.com/paper/1911.12780/) (2019)
- [Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis](https://mlsanity.com/paper/2111.03781/) (2021)
- [Maintaining driver attentiveness in shared-control autonomous driving](https://mlsanity.com/paper/2102.03298/) (2021)

## Built on by (most cited first, 5 of 5)

- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Is Certifying ℓp Robustness Still Worthwhile?](https://mlsanity.com/paper/2310.09361/) (2023)
- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)
- [Mind the Prompt: Self-adaptive Generation of Task Plan Explanations via LLMs](https://mlsanity.com/paper/2604.21092/) (2026)

## Abstract (arXiv)

We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method addresses this challenge by integrating DNN verification with the synthesis of verified Markov models. The synthesised models correspond to discrete-event controllers guaranteed to satisfy the safety, dependability and performance requirements of the autonomous system, and to be Pareto optimal with respect to a set of optimisation objectives. We use the method in simulation to synthesise controllers for mobile-robot collision mitigation and for maintaining driver attentiveness in shared-control autonomous driving.