A Systematic Literature Review on Mining LTL Specifications

Linear Temporal Logic (LTL) specifications play a crucial role in the verification process of cyber-physical systems, increasing the guarantees of their correctness. These specifications are vital for ensuring that both hardware and software components behave as expected, especially in complex real-world scenarios. In the last decades, researchers have developed several methodologies and tools to automatically generate LTL specifications, creating an urgent need to organize and synthesize existing literature to ease entry into this field and guide future research efforts. Therefore, starting from a pool of over 3000 papers extracted from the Scopus database in the temporal range 2000-2024, this paper employs the Preferred Reporting Items for Systematic Reviews and Meta-Analyses (PRISMA) methodology to produce a systematic review of mining LTL specifications of hardware and software systems. In particular, we provide a taxonomy of the methods and describe with significant detail all the relevant techniques present at the state of the art. Finally, we discuss the challenges of mining LTL specifications and explore potential directions and opportunities for future research.