LTLf declarative specifications of process behavior: foundations, expressiveness, and applications

Across a wide range of modern process-aware systems, behavioral knowledge is captured and used in multiple shapes. The same system may be described at design time through process modeling, observed at runtime through execution data, and acted upon through decision-making components that adapt to changing operational conditions. As a result, process representations must remain consistent across heterogeneous tasks, supporting verification, diagnostics, and optimization, without the need to redefine them from scratch every time the viewpoint changes. Meeting these requirements calls for representations that are expressive enough to capture complex behavioral relations, while remaining susceptible to analytical reasoning, quantitative assessment, and integration with data-driven techniques. These challenges arise in a variety of domains, including business processes, service- oriented architectures, and autonomous and learning-based systems. Among these landscapes, Business Process Management (BPM) provides a particularly illustrative domain in which the value of behavioral process knowledge becomes both operational and measurable. Business information systems generate large amounts of execution data that records how processes unfold in practice. This has fostered the development of process mining techniques, which aim to discover process representations from observed execution traces in the form of event logs and to assess whether observed behavior matches expected behavior. Consequently, process representations should not be regarded as mere design-time artifacts. Instead, they enable organizations to obtain a complete view of their operations, identify inefficiencies and potential deviations, and systematically improve the way work is performed. Indeed, behavioral insights directly translate into measurable performance gains, affecting key performance indicators (KPIs), namely throughput time, resource utilization, regulation compliance, and operational costs. Business process modeling (hereafter process modeling) has traditionally relied on imperative (or procedural) representations (e.g., Workflow net or BPMN) that explicitly define the allowed execution paths of a system. While these models provide precise operational semantics and support automated execution, their explicit nature may restrict analysis and diagnosis in settings characterized by variability, flexibility, or partial observability. Conversely, declarative specifications have received increasing interest, as they suggest a significantly different way of representing processes, describing behavior in terms of constraints that executions must satisfy, offering a more flexible representation that is particularly suited to highly dynamic environments. These constraints are typically expressed as temporal rules grounded in logics such as Linear Temporal Logic on Finite Traces (LTLf), stating what must hold in a process rather than prescribing how it is achieved. As a result, they can serve as an internal behavioral layer that can be reused across multiple analysis and reasoning tasks. Despite their complementary strengths, imperative and declarative paradigms are often treated as separate approaches, adjusting their adoption across different analytical and reasoning tasks. Similar process representation challenges arise in service-based and cyber-physical settings, as well as in autonomous and learning-based systems, where agents must continuously adapt their behavior while still respecting safety and compliance constraints. In these scenarios, behavioral knowledge configures as a basis for monitoring and assessing whether observed or learned policies remain consistent with expected temporal and causal relations. This thesis investigates the use of declarative temporal specifications as a unifying abstraction span the full lifecycle of behavioral reasoning in process-aware systems. The main research objective guiding the work is stated as follows: RO: Declarative Specifications as a Unifying Behavioral Abstraction Investigate the use of declarative temporal specifications as a unifying abstraction for representing, verifying, andexploiting behavioral knowledge in process-aware systems. With this goal in mind, we set three research questions across process representations, verification, and decision making. RQ1: Process Representation Paradigms How can a declarative process specification be systematically derived from an imperative process model, preserving behavioral equivalence between the two representations? First, we discuss the relationship between imperative and declarative process representations in the business processes domain, showing how a declarative specification can be systematically derived from an imperative model while preserving behavioral equivalence. To this end, we introduce a systematic method to synthesize declarative specifications from safe and sound Workflow nets, together with formal guarantees ensuring that the two representations capture exactly the same behavior. This result enables principled transitions between paradigms, allowing analysts to select the most suitable representation depending on the task at hand. RQ2: Conformance Measurement How can the satisfaction of declarative process specifications be quantitatively assessed over observed executions? Once a process has been modeled, the growing availability of execution data makes it natural to quantify how closely observed traces adhere to the normative representation. This is the goal of conformance checking, which measures the degree of correspondence between a model (or specification) and recorded executions. Traditional conformance checking verification techniques for declarative specifications often assess individual rules in isolation, overlooking their mutual interplay and offering primarily binary satisfaction outcomes. We address this gap by proposing a probabilistic framework to quantify the satisfaction of declarative process specifications over event logs. We introduce interestingness measures that characterize the degree to which LTLf declarative constraints are supported by observed behavior. These measures enable behavioral diagnostics and provide a foundation for detecting deviations, changes, and emerging patterns in process executions. RQ3: Decentralized Data Sources How can declarative specifications be checked against execution data that is distributed across multiple independent sources? Capturing specification-level insights becomes even more relevant when execution data are distributed across independent sources, each party observing only a partial view of the process, while a global assessment must be derived from distributed evidence. In these inter-organizational settings, traditional conformance checking approaches are hindered by confidentiality and governance constraints that prevent centralizing raw event logs. To overcome this limitation, we propose CONFINE, a secrecy-preserving framework that enables process mining and declarative conformance checking without disclosing sensitive execution data between collaborating organizations. CONFINE executes mining and checking algorithms inside trusted execution environments (TEEs), where event logs are transmitted and processed under attested confidentiality guarantees. The architecture supports a symmetric collaboration model in which each party can provide execution data and perform joint analyses, enabling behavioral insight to cross organizational boundaries while preserving data sovereignty.