Verifying and Explaining Failures of Autonomous Systems

Overview

The goal of this project is to improve both the robustness and the trustworthiness of autonomous Cyber-Physical Systems (CPSs) that rely on black-box components, yet must still comply to a formal specification. Think of an autonomous car, driven by a Neural-Netwrok (NN) controller, trained to avoid any collision.

Unpacking

The first part of the project is concerned with formal verification of such systems. Since these rely on black-box components, they cannot be certified through direct analysis of their model. Instead, we shall examine the complementary problem of falsification, i.e., proactively looking for scenes in which the system would fail its specification, conveying system vulnerabilities. If/Once these are found, they can be used as a basis from which to improve and robustify the system, to make sure these failures will not repeat during operation. The technical challenge is searching for such falsifying examples efficiently, through smart test-case selection, as random guessing would be impractical.

Our journal publication (Elimelech et al., 2026) introduced the system-agnostic, highly-efficient meta-planning approach for falsification. According to this approach, we can use a sampling-based motion planner to search the space of tests (system simulations), through gradual test mutation towards promising directions. This is a great example of using planning to benefit learning. Experimentation in this work was done using our very own Literacer (Elimelech et al., 2024) autonomous car simulator.

A follow up publication (Elimelech* et al., 2026) introduced an approach for explaining failures, such as those found through system falsification, by extending the framework of Actual Causality to the case of CPSs. The technical challenge, which this framework helps solve, is effectively sifting through possibly numerous causes for the event, pointing out to the actual cause of the failure. This work serves as a bridge between verification an explainability.

An autonomous car on an obstructed track.

References

2026

Journal

Falsification of Autonomous Systems in Rich Environments

Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi

ACM Transactions on Cyber-Physical Systems (TCPS), May 2026

DOI Bib

@article{Elimelech26tcps,
  bibtex_show = true,
  author = {Elimelech, Khen and Lahijanian, Morteza and Kavraki, Lydia E. and Vardi, Moshe Y.},
  author+an = {1=KE},
  title = {Falsification of Autonomous Systems in Rich Environments},
  journal = {{ACM} Transactions on Cyber-Physical Systems ({TCPS})},
  year = {2026},
  issue_date = {July 2026},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {10},
  number = {3},
  issn = {2378-962X},
  url = {https://doi.org/10.1145/3801740},
  doi = {10.1145/3801740},
  month = may,
  articleno = {35},
  numpages = {32}
}

Conference
Explaining Failures of Cyber-Physical Systems with Actual Causality

Khen Elimelech^*, Tom Yaacov^*, David A. Kelly, Hana Chockler, and Moshe Y. Vardi

In IEEE International Conference on Robotics and Automation (ICRA), Vienna, Austria, Jun 2026

Abs Bib

Modern autonomous Cyber-Physical Systems (CPSs), such as self-driving cars, face increasingly complex demands, and yet are expected to act reliably. The black-box nature often characterizing such systems, especially those relying on neural components, makes it impossible to fully verify the system behavior prior to deployment. Unfortunately, unexpected failures—cases when the system does not comply with its specification—are inevitable and may have catastrophic implications. To improve trust in the system and facilitate future mitigation after a failure occurs, it is important to try to derive an explanation for the unexpected system behavior. This paper introduces the novel concept of leveraging the framework of actual causality for CPS failure explanation. Up until now, this framework was only used to derive explanations in the context of simple systems, such as image classifiers. This paper addresses the theoretical gaps and provides the guidance needed to allow for correct explanation derivation in the CPS domain. Beyond the theoretical contribution, the paper presents two novel, practical, system-agnostic explanation derivation algorithms, allowing to prioritize either explanation optimality or derivation efficiency. The approach is demonstrated and evaluated in the context of a neural-network-controlled autonomous car, designed to avoid collisions.
@inproceedings{Elimelech26icra, bibtex_show = true, author = {Elimelech, Khen and Yaacov, Tom and Kelly, David A. and Chockler, Hana and Vardi, Moshe Y.}, author+an = {1=KE+jointfirst;2=jointfirst}, title = {Explaining Failures of Cyber-Physical Systems with Actual Causality}, booktitle = {{IEEE} International Conference on Robotics and Automation ({ICRA})}, year = {2026}, month = jun, location = {Vienna, Austria} }

2024

Workshop

LiteRacer: a lightweight autonomous vehicle simulator for benchmarking and development of formal verification techniques

Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi

In Workshop on Software Challenges in Formal Methods for Robotics (FMR), in conjunction with IEEE International Conference on Robotics and Automation (ICRA), Yokohama, Japan, May 2024

Bib Website

@inproceedings{Elimelech24icra_ws,
  bibtex_show = true,
  author = {Elimelech, Khen and Lahijanian, Morteza and Kavraki, Lydia E. and Vardi, Moshe Y.},
  author+an = {1=KE},
  title = {LiteRacer: a lightweight autonomous vehicle simulator for benchmarking and development of formal verification techniques},
  booktitle = {Workshop on Software Challenges in Formal Methods for Robotics (FMR), in conjunction with {IEEE} International Conference on Robotics and Automation ({ICRA})},
  year = {2024},
  month = may,
  location = {Yokohama, Japan},
  keywords = {workshop}
}