A Baseline Framework for the Qualification of LTL Specification Miners

Over the past few decades, the verification community has developed several specification miners as an alternative to manual assertion definition. However, assessing their effectiveness remains a challenging task. Most studies evaluate these miners using predefined ranking metrics, which often fail to ensure the quality of the inferred specifications, especially when no fixed ground truth exists and the relevance of the specifications varies depending on the use case. This paper presents a comprehensive framework aimed at facilitating the evaluation and comparison of Linear Temporal Logic (LTL) specification miners. Unlike traditional approaches, which struggle with subjective analyses and complex tool configurations, our framework provides a structured method for assessing and comparing the quality of specifications generated by multiple sources, using both semantic and syntactic techniques. To achieve this, the framework offers users an easy-to-extend environment for installing, configuring, and running third-party miners via Docker containers. Additionally’ it supports the inclusion of new evaluation methods through a modular design. Miner comparison can be based either on user-defined designs or on synthetic benchmarks, which are automatically generated to serve as a non-subjective ground truth for the evaluation of the miners. We demonstrate the utility of our framework through comparative analyses with four well-known LTL miners, illustrating its ability to standardize and enhance the specification mining evaluation process.