Learning Temporal Properties from Few, Positive Examples

Angelina Göbl

Specification mining refers to the problem of automatically inferring formal specifications from data. In contrast to traditional methods, which require both positive and negative examples, we focus on using positive data only, as negative examples are often hard to obtain. The main challenge is presented by the unrestricted search space being caused by using positive examples only. Existing algorithms to mine specifications for temporal properties with only positive trace data require an upper bound on the size of the resulting properties in order to avoid overly specific solutions. In addition, a large amount of examples needs to be provided. We, on the other hand, introduce a statistical learning approach to alleviate the need to provide such a bound by using the Minimum Description Length (MDL) principle for model selection. We focus on mining LTL formulas. Using MDL, we define ranking functions consisting of a simplicity and specificity score. The simplicity score is based on the size of the formula, while the specificity score reasons about the number of models fulfilling the formula. We experience, that our statistical learning approach is able to mine both liveness and safety properties with less data than related work.

Saarland University (Bachelor Thesis) November 2023
Contact Data Privacy Policy Imprint
Home People Publications
More