Linear dynamic logic on finite traces in business process management : a compositional approach

One way of modeling workflows in business process management (BPM) is by using a declarative approach, that is, instead of imperatively specifying what needs to be done, and in what order, one can specify constraints on what is allowed. The result is a more flexible model as everything that does not violate the specified constraints is allowed. In recent years, Linear Temporal Logic on finite traces (LTLf) has been one of the available logics used to specify such constraints. However, LTLf lacks the ability to monitor metaconstraints (i.e., constraints overconstraints). To handle this, one can use Linear Dynamic Logic on finite traces (LDLf) instead. In their paper Monitoring Constraints and Metaconstraints withTemporal Logics on Finite Traces, De Giacomo et al. (2020) presented a framework, and a formal way of translating LDLf formula to an executable Deterministic Finite Automaton (DFA), to be used in BPM. The algorithm they used for the translation was LDLf2NFA. This paper investigates if the construction time, and the size, of the DFA can be reduced by using a compositional algorithm, CLDLf, instead. The results show that the time can be reduced for larger formulae, that is, formulae with a length above 20. However, as both algorithms produce a minimal DFA as the end product, no reduction in size (i.e., the number of states) could be made