Learning Linear Temporal Properties

ABSTRACT. Making sense of the observed behavior of complex systems is an important problem in practice. It arises, for instance, in debugging (especially in the context of distributed systems), reverse engineering (e. g. , of malware and viruses), specification mining for formal verification, and modernization of legacy systems, to name but a few examples. To help engineers understand the dynamic (i. e. , temporal) behavior of complex systems, we develop algorithms to learn linear temporal properties from data. More precisely, the problem we address in this talk is the following: given two disjoint, finite sets of infinite words, representing positive and negative examples, construct a (minimal) LTL formula such that all positive examples satisfy the formula, while all negative example do not. As the resulting formulas are meant to be read and understood by humans, our learning algorithms are designed to learn minimal LTL formulas, or at least "small" formulas with a "simple" structure. We also discuss interesting directions for future work.

Authors

• Daniel Neider TU Dortmund University; Research Center Trustworthy Data Science and Security, University Alliance Ruhr

Keywords

No keywords are indexed for this paper.