# Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Oct 2016.

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

- [Code Integrity Attestation for PLCs using Black Box Neural Network Predictions](https://mlsanity.com/paper/2106.07851/) (2021)
- [Architectural Transformations and Emerging Verification Demands in AI-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2510.00519/) (2025)

## Abstract (arXiv)

Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based system verification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to automatically `verify' such complex systems through a combination of learning, abstraction and refinement from a set of system log traces. We assume that log traces and sampling frequency are adequate to capture `enough' behaviour of the system. Given a safety property and the concrete system log traces as input, LAR automatically learns and refines system models, and produces two kinds of outputs. One is a counterexample with a bounded probability of being spurious. The other is a probabilistic model based on which the given property is `verified'. The model can be viewed as a proof obligation, i.e., the property is verified if the model is correct. It can also be used for subsequent system analysis activities like runtime monitoring or model-based testing. Our method has been implemented as a self-contained software toolkit. The evaluation on multiple benchmark systems as well as a real-world water treatment system shows promising results.