PALM: A Technique for Process ALgebraic Specification Mining

We propose a technique to automatically generate a formal specification of the model of a system from a set of observations of its behaviour. We aim to free systems modellers from the burden of explicitly formalising the behaviour of an existing system to analyse it. We take advantage of an algorithm introduced by the process mining community, which takes as input an event log and generates a formal specification that can be combined with other specifications to obtain a global model of the overall behaviour of a system. Specifically, we have adapted a known process discovery algorithm to produce a specification in mCRL2, a formal specification language based on process algebras. The availability of mCRL2 specifications enables us to take advantage of its rich toolset for verifying systems properties and for effectively reasoning over distributed scenarios where multiple organizations interact to reach common goals. This is an aspect that is not supported by the approaches based on Petri Nets, usually used for process mining. The methodology has been integrated in a stand-alone tool and has been validated using custom-made and real event logs.