Learning Interpretable Temporal Properties from Positive Examples Only
This work addresses the challenge of explaining temporal behavior in systems where negative examples are hard to obtain, offering a method for interpretable model learning in domains like verification or diagnostics.
The authors tackled the problem of learning interpretable temporal models, such as deterministic finite automata and linear temporal logic formulas, from black-box systems using only positive examples, and developed algorithms with theoretical guarantees that were evaluated on synthetic data.
We consider the problem of explaining the temporal behavior of black-box systems using human-interpretable models. To this end, based on recent research trends, we rely on the fundamental yet interpretable models of deterministic finite automata (DFAs) and linear temporal logic (LTL) formulas. In contrast to most existing works for learning DFAs and LTL formulas, we rely on only positive examples. Our motivation is that negative examples are generally difficult to observe, in particular, from black-box systems. To learn meaningful models from positive examples only, we design algorithms that rely on conciseness and language minimality of models as regularizers. To this end, our algorithms adopt two approaches: a symbolic and a counterexample-guided one. While the symbolic approach exploits an efficient encoding of language minimality as a constraint satisfaction problem, the counterexample-guided one relies on generating suitable negative examples to prune the search. Both the approaches provide us with effective algorithms with theoretical guarantees on the learned models. To assess the effectiveness of our algorithms, we evaluate all of them on synthetic data.