# Data-Driven Probabilistic Evaluation of Logic Properties with PAC-Confidence on Mealy Machines

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 24 references that are in the map.
- First posted on arXiv 20 Aug 2025.

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

- [Data-driven verification and synthesis of stochastic systems via barrier certificates](https://mlsanity.com/paper/2111.10330/) (2021)
- [Data-Driven Abstraction-Based Control Synthesis](https://mlsanity.com/paper/2206.08069/) (2022)
- [Data-Driven Verification under Signal Temporal Logic Constraints](https://mlsanity.com/paper/2005.05040/) (2020)
- [Neural Abstraction-Based Controller Synthesis and Deployment](https://mlsanity.com/paper/2307.03783/) (2023)
- [PAC Learning-Based Verification and Model Synthesis](https://mlsanity.com/paper/1511.00754/) (2015)

## Abstract (arXiv)

Cyber-Physical Systems (CPS) are complex systems that require powerful models for tasks like verification, diagnosis, or debugging. Often, suitable models are not available and manual extraction is difficult. Data-driven approaches then provide a solution to, e.g., diagnosis tasks and verification problems based on data collected from the system. In this paper, we consider CPS with a discrete abstraction in the form of a Mealy machine. We propose a data-driven approach to determine the safety probability of the system on a finite horizon of n time steps. The approach is based on the Probably Approximately Correct (PAC) learning paradigm. Thus, we elaborate a connection between discrete logic and probabilistic reachability analysis of systems, especially providing an additional confidence on the determined probability. The learning process follows an active learning paradigm, where new learning data is sampled in a guided way after an initial learning set is collected. We validate the approach with a case study on an automated lane-keeping system.