csteidl/ltlchecker

The LTL Checker, a ProM framework plug-in

The LTL Checker, a ProM framework plug-in

In 2004, as part of my Masters in Computer Science and Engineering at the University of Technology Eindhoven (TU/e), I did an internship at the Information Systems group of the Technology and Society department (TeMa). This group worked on process mining, which is the process of extracting valuable information from event logs that are generated by processes. This group developed a tool in Java, called ProM, to mine (large) XML-based process logs.

In my internship I developed a plug-in for their ProM framework to check event logs for traces that do or do not conform to certain properties specified in a linear temporal logic (LTL). In LTL one can specify properties such as:

• Step X always follows step Y
• All cases valued over $45.000 are handled by manager B
• All issues created in the weekend are confirmed in two days maximum
• And so on.

For more information about this plug-in, I refer to its manual and a paper I co-authored with my supervising professor: W.M.P. van der Aalst and H.T. de Beer and B.F. van Dongen (2005) Process Mining and Verification of Properties: An Approach based on Temporal Logic (PDF).

As both the ProM framework and the LTL Checker plug-in have been developed further since then by others, I refer you to the latest version of the ProM framework to try out the LTL Checker plugin: http://www.processmining.org/.