General past-time linear temporal logic specification mining

Specification mining is an automated or semi-automated process for inferring models or properties from computer programs or systems and is a useful way to aid program understanding, monitoring, and verification. There have been many works on mining various forms of specifications, of which mining for temporal logic specifications is becoming increasingly interesting, as temporal logic is capable of formally describing and reasoning about software behaviors in terms of temporal order. Several approaches have been proposed to mine linear temporal logic (LTL) specifications. But compared to LTL, past-time linear temporal logic (PTLTL) enables specifying many system behaviors in more natural forms, such as a specification G(a→ Ob) stating “Once event a happens, another event b must have happened before it”, which is much more intuitive than the equivalent LTL specification ¬((¬b)U(a∧¬b)) for users and easier to check because of its shorter form. In this paper, we propose a general approach to mining PTLTL specifications. In addition, we present a cache strategy and a parallel strategy to make it faster and more scalable. We implement a tool named Past Time Linear Temporal Logic Miner (PTLM) and evaluate it. The result is encouraging.