Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces

Runtime monitoring is a central operational decision support task in business process management. It helps process executors to check on-the-fly whether a running process instance satisfies business constraints of interest, providing an immediate feedback when deviations occur. We study runtime monitoring of properties expressed in ltlf, a variant of the classical ltl (Linear-time Temporal Logic) that is interpreted over finite traces, and in its extension ldlf, a powerful logic obtained by combining ltlf with regular expressions. We show that ldlf is able to declaratively express, in the logic itself, not only the constraints to be monitored, but also the de facto standard rv-LTL monitors. On the one hand, this enables us to directly employ the standard characterization of ldlf based on finite-state automata to monitor constraints in a fine-grained way. On the other hand, it provides the basis for declaratively expressing sophisticated metaconstraints that predicate on the monitoring state of other constraints, and to check them by relying on standard logical services instead of ad hoc algorithms. We then report on how this approach has been effectively implemented using Java to manipulate ldlf formulae and their corresponding monitors, and the RuM rule mining suite as underlying infrastructure.