Abstract
Runtime monitoring is one of the central tasks to provide operational decision support to running business processes, and check on-the-fly whether they comply with constraints and rules. We study runtime monitoring of properties expressed in LTL on finite traces (LTFf) and its extension LDFf. LDFf is a powerful logic that captures all monadic second order logic on finite traces, which is obtained by combining regular expressions with LTFf, adopting the syntax of propositional dynamic logic (PDL). Interestingly, in spite of its greater expressivity, LDFf has exactly the same computational complexity of LTFf. We show that LDFf is able to capture, in the logic itself, not only the constraints to be monitored, but also the de-facto standard RV-LTL monitors. This makes it possible to declaratively capture monitoring metaconstraints, i.e., constraints about the evolution of other constraints, and check them by relying on usual logical services for temporal logics instead of ad-hoc algorithms. This, in turn, enables to flexibly monitor constraints depending on the monitoring state of other constraints, e.g., “compensation” constraints that are only checked when others are detected to be violated. In addition, we devise a direct translation of LDFf formulas into nondeterministic automata, avoiding to detour to Büchi automata or alternating automata, and we use it to implement a monitoring plug-in for the ProM suite.