Linear Temporal Logic over finite traces for declarative business processes

Business process management (BPM) is a discipline at the intersection between operations management, computer science, and software and systems engineering, whose grand goal is to support managers, analysts, and domain experts in the design, deployment, enactment, and continuous improvement of (work) processes within an organisation. 

In this talk, we review the BPM lifecycle, introducing the main reasoning and analysis tasks needed to support process management from process design to operational support and process mining, a growing area of research that aims at continuous process improvement based on the factual event data recorded inside information systems. 

We then focus on knowledge-intensive processes, which challenge the foundations of BPM and process mining, due to their inherent flexibility. We argue that such processes cannot be satisfactory modelled nor understood using conventional, procedural process modelling languages, but are instead best captured using a declarative approach based on temporal constraints. We ground our discussion on one of the most prominent languages in the declarative BPM spectrum: Declare. We show that Declare is naturally formalised in LTLf, and explain how the automata-theoretic characterisation of LTLf provides a solid, effective basis to elegantly solve a variety of central BPM/process mining tasks: model verification, enactment, anticipatory monitoring, and process discovery. In doing so, we touch on interesting recent extensions of LTLf dealing with data and uncertainty.