Abstract
Declarative process modeling languages such as DECLARE describe the behavior of processes by means of constraints. Such constraints exert rules on the execution of tasks upon the execution of other tasks called activations. The constraint is thus fulfilled both if it is activated and the consequent rule is respected, or if it is not activated at all. The latter case, named vacuous satisfaction, is clearly less interesting than the former. Such a distinction becomes of utmost importance in the context of declarative process mining techniques, where processes are analyzed based on the identification of the most relevant constraints valid in an event log. Unfortunately, this notion of relevance has never been formally defined, and all the proposals existing in the literature use ad-hoc definitions that are only applicable to a pre-defined set of constraint patterns. This makes existing declarative process mining techniques inapplicable when the target constraint language is extensible, and may contain formulae that go beyond the pre-defined patterns. In this paper, we tackle this open challenge, and show how the notion of constraint activation and vacuous satisfaction can be captured semantically, in the case of constraints expressed in arbitrary temporal logics over finite traces. Our solution relies on the annotation of finite state automata to incorporate relevance-related information. We discuss the formal grounding of our approach and describe the implementation thereof. We finally report on experimental results gathered from the application of our approach to real-life data, which show the advantages and feasibility of our solution. © 2018 Elsevier Ltd