Random Generation of Small Quantitative Automata for Algorithm Debugging
arXiv:2607.12170 · doi:10.1007/978-3-032-30693-7_13
The paper presents a framework that automatically generates small, non‑degenerate quantitative automata, checks them against a target property, and shrinks any violations to minimal counterexamples, enabling effective debugging of analysis tools like the PTA model checker IMITATOR.
Abstract
Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches -- benchmarks, mutation testing, uniform random generation -- each fail to expose subtle implementation bugs. We present a framework that repeatedly 1) generates random quantitative automata that are non-degenerate by construction, 2) tests each against a target property, and 3) shrinks any violation to a local minimum, yielding a small, actionable counterexample. We implement the framework for parametric timed automata (PTA) and apply it to IMITATOR, a mature model checker for PTA, uncovering 5 previously unknown bugs, one of which was exposed by a counterexample with just 2 locations and 1 transition.
Submitted version. Published version available at doi.org/10.1007/978-3-032-30693-7_13