Runtime verification (RV) examines whether a system’s run satisfies its specification. This typically requires full knowledge of the run, but many applications face imprecise or missing inputs, e.g., from noisy sensors. We aim to develop a symbolic RV procedure that can handle noisy inputs and is able to exploit assumptions that encode background knowledge about the system in order to produce reliable monitoring verdicts. As the symbolic setting in general induces increasingly large monitoring states, we aim to identify fragments of specifications where monitoring requires constant memory. After providing a formalization of the problem at hand, we propose an RV procedure and give formal correctness statements and proofs. We empirically validate our approach in two realistic case studies. The developed RV procedure is the first to effectively handle both uncertainties and assumptions in the expressive setting of Lola, and we identify relevant and expressive fragments where our procedure requires constant memory. Our evaluation witnesses the practical applicability of the approach. RV with uncertainties and assumptions is feasible in the Lola setting, and needs only constant memory in some relevant fragments. Future work will explore further theories and adapt the approach to specific applications.

This paper presents a manifesto that articulates the conceptual foundations of Agentic Business Process Management (APM), an extension of Business Process Management (BPM) for governing autonomous agents executing processes in organizations. From a management perspective, APM represents a paradigm shift from the traditional view on business processes. This shift is driven by the realization of process awareness by agent-oriented abstractions: software and human agents act as primary functional entities that perceive, reason, and act within explicit process frames. Thus, APM moves away from automation-oriented BPM towards systems in which autonomy is constrained, aligned, and made operational through process aware agents. We introduce the core abstractions and architectural elements required to realize APM systems and elaborate on four key capabilities that agents in APM systems must support: framed autonomy , explainability , conversational actionability , and self-modification . These capabilities jointly ensure that agents’ goals are aligned with organizational goals and that agents behave in a framed yet proactive manner in pursuing those goals. We discuss the extent to which the capabilities can be realized and identify research challenges whose resolution requires further advances in BPM, AI, and multi-agent systems. The manifesto thus serves as a roadmap for bridging these communities and for guiding the development of APM systems in practice.

Together with Information Systems, we celebrate the journal’s 50th anniversary and the 10th anniversary of our joint work on a systematic framework for compliance monitoring functionalities.

Business process management employs process models and event logs to represent the behavior of the information systems under study. Traditional case-centric notions consider the order of activities and events in isolated process instances. The emerging field of object-centric processes challenges this assumption by putting objects in the center. Object-centric process mining and modeling approaches identify the structure of co-evolving data objects that influence the behavior of an information system to provide a comprehensive view of the system behavior. Object-centricity has been investigated independently in process modeling and in process mining, which resulted in the coexistence of seemingly contradictory assumptions and definitions. As a community effort, this research manifesto relates and aligns existing terminologies, definitions, and perspectives to provide a common ground for current and future research in object-centric business process management. Based on the current state of research, we propose a conceptualization that sets process models and event logs in relation to the information system’s behavior and the execution data it generates. The conceptualization aims at aligning different terminologies and, thus, providing a basis to model and analyze behavioral characteristics. Building on this common ground, we identify open research challenges along the most relevant research areas in object-centric process management. For each research area, its current status is investigated and an outline of the most relevant research challenges is presented.

Counterfactual explanations are one of the prominent eXplainable Artificial Intelligence (XAI) techniques, and suggest changes to input data that could alter predictions, leading to more favourable outcomes. Existing counterfactual methods do not readily apply to temporal domains, such as that of process mining, where data take the form of traces of activities that must obey to temporal background knowledge expressing which dynamics are possible and which not. Specifically, counterfactuals generated off-the-shelf may violate the background knowledge, leading to inconsistent explanations. This work tackles this challenge by introducing a novel approach for generating temporally constrained counterfactuals, guaranteed to comply by design with background knowledge expressed in Linear Temporal Logic on process traces (LTLp). We do so by infusing automata-theoretic techniques for LTLp inside a genetic algorithm for counterfactual generation. The empirical evaluation shows that the generated counterfactuals are temporally meaningful and more interpretable for applications involving temporal dependencies.

We propose a novel algorithm for epistemic planning based on dynamic epistemic logic (DEL). The novelty is that we limit the depth of reasoning of the planning agent to an upper bound b, meaning that the planning agent can only reason about higher-order knowledge to at most (modal) depth b. We then compute a plan requiring the lowest reasoning depth by iteratively incrementing the value of b. The algorithm relies at its core on a new type of "canonical" b-bisimulation contraction that guarantees unique minimal models by construction. This yields smaller states wrt. standard bisimulation contractions, and enables to efficiently check for visited states. We show soundness and completeness of our planning algorithm, under suitable bounds on reasoning depth, and that, for a bound b, it runs in (b+1)-EXPTIME. We implement the algorithm in a novel epistemic planner, DAEDALUS, and compare it to the EFP 2.0 planner on several benchmarks from the literature, showing effective performance improvements.

State-of-the-art approaches for integrating symbolic knowledge with deep learning architectures have demonstrated promising results in static domains. However, methods to handle temporal logic specifications remain underexplored. The only existing approach relies on an explicit representation of a finite-state automaton corresponding to the temporal specification. Instead, we aim at directly injecting the temporal knowledge into the neural model without having to rely on a separate symbolic structure. Specifically, we propose a neurosymbolic framework designed to incorporate temporal logic specifications, expressed in Linear Temporal Logic over finite traces (LTLf), directly into deep learning architectures for sequence-based tasks. We extend the Iterative Local Refinement (ILR) neurosymbolic algorithm, leveraging the recent introduction of fuzzy LTLf interpretations. We name this proposed method Temporal Iterative Local Refinement (T-ILR). We assess T-ILR on an existing benchmark for temporal neurosymbolic architectures, consisting of the classification of image sequences in the presence of temporal knowledge. The results demonstrate improved accuracy and computational efficiency compared to the state-of-the-art method.

Krohn-Rhodes theory encompasses the techniques for the study of finite automata and their decomposition into elementary automata. The famous result of Krohn and Rhodes roughly states that each finite automaton can be decomposed into elementary components which correspond to permutation and reset automata connected by a cascade product. However, this outcome is not easy to access for the working computer scientist. This paper provides a short introduction into Krohn-Rhodes theory based on the valuable work of Ginzburg.

In the context of process mining, alignments are increasingly being adopted for conformance checking, due to their ability in providing sophisticated diagnostics on the nature and extent of deviations between observed traces and a reference process model. On the downside, deriving alignments is challenging from the computational point of view, even more so when dealing with multiple perspectives in the process, such as, in particular, data. In fact, every observed trace must in principle be compared with infinitely many model traces. In this work, we tackle this computational bottleneck by borrowing the classical idea of encoding from machine learning. Instead of computing alignments directly and exactly, we do so in an approximate way after applying a lossy trace encoding that maps each trace into a corresponding compact, vectorial representation that retains only certain information of the original trace. We study trace encoding-based approximate alignments for processes equipped with event data attributes, from three different angles. First, we indeed show that computing approximate alignments in this way is much more efficient than in the exact setting. Second, we evaluate how accurate such approximate alignments are, considering different encoding strategies that focus on different features of the trace. Our findings suggest that sufficiently rich encodings actually yield good accuracy. Third, we consider the impact of frequency and density of model variants, comparing the effectiveness of using standard approximate multi-perspective alignments as opposed to a variant that incorporates probabilities. As a by-product of this analysis, we also obtain insights on how these two approaches perform in the presence of noise. • Approximate multi-perspective alignments based on trace encodings. • Formal framework to compute approximate alignments against Data Petri nets. • Extension dealing with trace probabilities. • Experimental evaluation witnessing efficiency and accuracy, also in the presence of noise.

Temporal logics over finite traces have recently seen wide application in a number of areas, from business process modelling, monitoring and mining to planning and decision-making. However, real-life dynamic systems contain a degree of uncertainty which cannot be handled with classical logics. We thus propose a new probabilistic temporal logic over finite traces using superposition semantics, where all possible evolutions are possible, until observed. We study the properties of the logic and provide automata-based mechanisms for deriving probabilistic inferences from its formulas. We then study a fragment of the logic with better computational properties. Notably, formulas in this fragment can be discovered from event log data using off-the-shelf existing declarative process discovery techniques.

Given a specification of Linear-time Temporal Logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. In this paper we study, for the first time, the foundations of reactive synthesis for DECLARE, a well-established declarative, pattern-based business process modelling language grounded in LTLf. We provide a threefold contribution. First, we define a reactive synthesis problem for DECLARE. Second, we show how an arbitrary DECLARE specification can be polynomially encoded into an equivalent pure-past one in LTLf, and exploit this to define an EXPTIME algorithm for DECLARE synthesis. Third, we derive a symbolic version of this algorithm, by introducing a novel translation of pure-past temporal formulas into symbolic deterministic finite automata.

The need to model and analyse dynamic systems operating over complex data is ubiquitous in AI and neighboring areas, in particular business process management. Analysing such data-aware systems is a notoriously difficult problem, as they are intrinsically infinite-state. Existing approaches work for specific datatypes, and/or limit themselves to the verification of safety properties. In this paper, we lift both such limitations, studying for the first time linear-time verification for so-called data-aware processes modulo theories (DMTs), from the foundational and practical point of view. The DMT model is very general, as it supports processes operating over variables that can store arbitrary types of data, ranging over infinite domains and equipped with domain-specific predicates. Specifically, we provide four contributions. First, we devise a semi-decision procedure for linear-time verification of DMTs, which works for a very large class of datatypes obeying to mild model-theoretic assumptions. The procedure relies on a unique combination of automata-theoretic and cover computation techniques to respectively deal with linear-time properties and datatypes. Second, we identify an abstract, semantic property that guarantees the existence of a faithful finite-state abstraction of the original system, and show that our method becomes a decision procedure in this case. Third, we identify concrete, checkable classes of systems that satisfy this property, generalising several results in the literature. Finally, we present an implementation and an experimental evaluation over a benchmark of real-world data-aware business processes.

The integration of business process management (BPM) with artificial intelligence (AI) is driving unprecedented advancements in the creation of trustworthy, intelligent information systems. On the one hand, BPM poses unconventional, relevant questions about processes and the event data produced during their execution. On the other hand, AI offers established techniques that must be adapted and further enhanced to address these questions effectively. This synergy is particularly impactful in the case of flexible processes, which are best represented using a declarative approach – emphasising the temporal constraints that must be respected by the process, instead of explicitly detailing all the acceptable flows of activities. In this article, we overview how automated reasoning and learning techniques for temporal logics on finite traces provide robust foundations for representing, mining, and synthesising declarative processes. We cover established results as well as frontier research in this area.

Abstract With the growing use of temporal logics in areas ranging from robot planning to runtime verification, it is critical that users have a clear understanding of what a specification means. Toward this end, we have been developing a catalog of semantic errors and a suite of test instruments targeting various user-groups. The catalog is of interest to educators, to logic designers, to formula authors, and to tool builders, e.g., to identify mistakes. The test instruments are suitable for classroom teaching or self-study. This paper reports on five sets of survey data collected over a three-year span. We study misconceptions about finite-trace $$\textsc {ltl}_{f}$$ L T L f in three ltl-aware audiences, and misconceptions about standard ltl in novices. We find several mistakes, even among experts. In addition, the data supports several categories of errors in both $$\textsc {ltl}_{f}$$ L T L f and ltl that have not been identified in prior work. These findings, based on data from actual users, offer insights into what specific ways temporal logics are tricky and provide a groundwork for future interventions.

Data Petri nets (DPNs) have gained traction as a model for data-aware processes, thanks to their ability to balance simplicity with expressiveness, and because they can be automatically discovered from event logs. While model checking techniques for DPNs have been studied, more complex analysis tasks that are highly relevant for BPM are beyond methods known in the literature. We focus here on equivalence and inclusion of process behaviour with respect to language and configuration spaces, optionally taking data into account. Such comparisons are important in the context of key process mining tasks, namely process repair and discovery, and related to conformance checking. To solve these tasks, we propose approaches for bounded DPNs based on constraint graphs, which are faithful abstractions of the reachable state space. Though the considered verification tasks are undecidable in general, we show that our method is a decision procedure DPNs that admit a finite history set. This property guarantees that constraint graphs are finite and computable, and was shown to hold for large classes of DPNs that are mined automatically, and DPNs presented in the literature. The new techniques are implemented in the tool ada, and an evaluation proving feasibility is provided.

A model of an information system describes its processes and how resources are involved in these processes to manipulate data objects. This paper presents an extension to the Petri nets formalism suitable for describing information systems in which states refer to object instances of predefined types and resources are identified as instances of special object types. Several correctness criteria for resource- and object-aware information systems models are proposed, supplemented with discussions on their decidability for interesting classes of systems. These new correctness criteria can be seen as generalizations of the classical soundness property of workflow models concerned with process control flow correctness.

Capturing stochastic behaviour in business and work processes is essential to quantitatively understand how nondeterminism is resolved when taking decisions within the process. This is of special interest in process mining, where event data tracking the actual execution of the process are related to process models, and can then provide insights on frequencies and probabilities. Variants of stochastic Petri nets provide a natural formal basis to represent stochastic behaviour and support different data-driven and model-driven analysis tasks in this spectrum. However, when capturing business processes, such nets inherently need a labelling that maps between transitions and activities. In many state of the art process mining techniques, this labelling is not 1-on-1, leading to unlabelled transitions and activities represented by multiple transitions. At the same time, they have to be analysed in a finite-trace semantics, matching the fact that each process execution consists of finitely many steps. These two aspects impede the direct application of existing techniques for stochastic Petri nets, calling for a novel characterisation that incorporates labels and silent transitions in a finite-trace semantics. In this article, we provide such a characterisation starting from generalised stochastic Petri nets and obtaining the framework of labelled stochastic processes (LSPs). On top of this framework, we introduce different key analysis tasks on the traces of LSPs and their probabilities. We show that all such analysis tasks can be solved analytically, in particular reducing them to a single method that combines automata-based techniques to single out the behaviour of interest within an LSP, with techniques based on absorbing Markov chains to reason on their probabilities. Finally, we demonstrate the significance of how our approach in the context of stochastic conformance checking, illustrating practical feasibility through a proof-of-concept implementation and its application to different datasets.

We study verification of reachability properties over Communicating Datalog Programs (CDPs), which are networks of relational nodes connected through unordered channels and running Datalog-like computations. Each node manipulates a local state database (DB), depending on incoming messages and additional input DBs from external services. Decidability of verification for CDPs has so far been established only under boundedness assumptions on the state and channel sizes, showing at the same time undecidability of reachability for unbounded states with only two unary relations or unbounded channels with a single binary relation. The goal of this paper is to study the open case of CDPs with bounded states and unbounded channels, under the assumption that channels carry unary relations only. We discuss the significance of the resulting model and prove the decidability of verification of variants of reachability, captured in fragments of first-order CTL. We do so through a novel reduction to coverability problems in a class of high-level Petri Nets that manipulate unordered data identifiers. We study the tightness of our results, showing that minor generalizations of the considered reachability properties yield undecidability of verification, both for CDPs and the corresponding Petri Net model.

In the context of verification of data-aware processes, a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety properties. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here Ontology-Based Processes, which are a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs), where, instead of managing a database, we operate over a description logic (DL) ontology. We prove that when the DL is expressed in (a slight extension of) RDFS, it enjoys suitable model-theoretic properties, and that by relying on such DL we can define Ontology-Based Processes to which backward reachability can still be applied. Relying on these results we are able to show that in this novel setting, verification of safety properties is decidable in PSPACE.

We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the trace prefix seen so far, and all its possible finite-length, future continuations. This makes monitoring at least as hard as satisfiability and validity. Traces consist of finite sequences of assignments of a fixed set of variables to numerical values. Properties are specified in a logic we call ALTLf, combining LTLf (LTL on finite traces) with linear arithmetic constraints that may carry lookahead, i.e., variables may be compared over multiple instants of the trace. While the monitoring problem for this setting is undecidable in general, we show decidability for (a) properties without lookahead, and (b) properties with lookahead that satisfy the abstract, semantic condition of finite summary, studied before in the context of model checking. We then single out concrete, practically relevant classes of constraints guaranteeing finite summary. Feasibility is witnessed by a prototype implementation.

The use of Dynamic Epistemic Logic (DEL) in multi-agent planning has led to a widely adopted action formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. As such expressive power comes at the cost of undecidability, several decidable fragments have been isolated, mainly based on syntactic restrictions of the action formalism. In this paper, we pursue a novel semantic approach to achieve decidability. Namely, rather than imposing syntactical constraints, the semantic approach focuses on the axioms of the logic for epistemic planning. Specifically, we augment the logic of knowledge S5n and with an interaction axiom called (knowledge) commutativity, which controls the ability of agents to unboundedly reason on the knowledge of other agents. We then provide a threefold contribution. First, we show that the resulting epistemic planning problem is decidable. In doing so, we prove that our framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest. Second, we study different generalizations of the commutativity axiom, with the goal of obtaining decidability for more expressive fragments of DEL. Finally, we show that two well-known epistemic planning systems based on action templates, when interpreted under the setting of knowledge, conform to the commutativity axiom, hence proving their decidability.

Within the growing area of data-aware processes, Data Petri nets (DPNs) with arithmetic data have recently gained popularity thanks to their ability to balance simplicity with expressiveness. DPNs can be automatically mined from event data, but these process discovery techniques typically come without any correctness guarantees. In particular, the generated models may violate the crucial property of data-aware soundness. While data-aware soundness can be checked automatically for a large class of models, nothing is known about how to repair such processes once a violation is detected. In this paper we are concerned with repairing DPNs so that the refined model satisfies the desired soundness properties. Our approach is based on conservative behavioural changes, which are minimally invasive in the sense that the behaviour of the repaired model coincides with that of the original model except for (prefixes of) traces that caused the violation. We show experimentally that the approach can be used to repair unsound DPNs from the literature.

Plan Recognition is the task of identifying the goals and plans of an agent by observing its behavior within the environment. The problem has been extensively studied in the context of planning, in particular bringing forward stochastic techniques dealing with probability distributions over the possible agent goals, under the assumption that observations are reliable. More recently, a connection between this problem and process mining techniques has been established, paving the way towards the application of alignment-based conformance checking techniques from process mining to tackle plan recognition problems in a setting where observations may be faulty. In this work, we reconcile these two lines of research in a unified framework that deals at once with uncertainty over the goals and the faithfulness of observations. Instead of using ad-hoc techniques to solve this problem, we cast it as a probabilistic trace alignment problem, trading off between the similarity of observations and plans, and the likelihood that the agent is performing those plans. We assess the effectiveness of our approach by conducting a comparative experimental evaluation on state-of-the-art benchmarks.

Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management and Database Theory. To make these systems amenable to verification, the amount of information stored in each state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We lift these restrictions by introducing the framework of Relational Action Bases (RABs), which generalizes existing frameworks and in which unbounded relational states are evolved through actions that can (1) quantify both existentially and universally over the data, and (2) use arithmetic constraints. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.

In this paper, we summarise the main technical results obtained for specification probability. That is, we compute the probability that if a bounded stochastic Petri net produces a trace, that trace satisfies a given specification.

Complexity of medical treatments can vary from prescribing medicine for a specific ailment to managing a complex set of simultaneous medical issues. In the latter case, doctors are assisted by clinical guidelines which outline standard medical procedures, tests, treatments, etc. To facilitate the use of such guidelines, they can be digitized as processes and adopted in complex process engines offering additional help to health providers such as decision support while monitoring active treatments so as to detect flaws in treatment procedures and suggest possible reactions on them. For example, a patient may present symptoms of multiple diseases simultaneously (requiring multiple clinical guidelines to be followed), while also being allergic to some often-used drugs (requiring additional constraints to be respected). This can easily lead to treating a patient based on a set of process specifications which are not fully compatible with each other. While a scenario like that commonly occurs in practice, research in that direction has thus far given little consideration to how to specify multiple clinical guidelines and how to automatically combine their specifications in the context of the monitoring task. In our previous work (Alman et al., 20222), we presented a conceptual framework for handling the above cases in the context of monitoring. In this paper, we present the algorithms necessary for implementing key components of this conceptual framework. More specifically, we provide formal languages for representing clinical guideline specifications and formalize a solution for monitoring the interplay of such specifications expressed as a combination of (data-aware) Petri nets and temporal logic rules. The proposed solution seamlessly handles combination of the input process specifications and provides both early conflict detection and decision support during process execution. We also discuss a proof-of-concept implementation of our approach and present the results of extensive scalability experiments.

Virtual Knowledge Graphs (VKGs) constitute one of the most promising paradigms for integrating and accessing legacy data sources. A critical bottleneck in the integration process involves the definition, validation, and maintenance of mapping assertions that link data sources to a domain ontology. To support the management of mappings throughout their entire lifecycle, we identify a comprehensive catalog of sophisticated mapping patterns that emerge when linking databases to ontologies. To do so, we build on well-established methodologies and patterns studied in data management, data analysis, and conceptual modeling. These are extended and refined through the analysis of concrete VKG benchmarks and real-world use cases, and considering the inherent impedance mismatch between data sources and ontologies. We validate our catalog on the considered VKG scenarios, showing that it covers the vast majority of mappings present therein.

Conformance checking, one of the central tasks in process mining, compares the expected behavior described by a reference process model to the actual behavior recorded in an event log, with the goal of detecting deviations. Traditionally, it is assumed that the log provides a faithful and complete digital footprint of reality. However, assuming perfect logs is often unrealistic: real-life logs typically suffer from data quality issues, exposing uncertainty in their events, timestamps, and data attributes. We attack this problem by introducing a comprehensive framework for multi-perspective conformance checking dealing with uncertainty along three perspectives: control-flow, time, and data. From the modeling point of view, we consider process models formalized as Petri nets operating over data variables, and event logs presenting uncertainty at the event- and attribute-level. We cast conformance checking as an alignment problem, extending the traditional notions of alignment and cost function to deal with uncertainty along the three aforementioned perspectives. From the operational point of view, we show how (optimal) alignments can be computed through well-established automated reasoning techniques from Satisfiability Modulo Theories (SMT). Specifically, we show how previous results on data-aware SMT-based conformance checking can be lifted to this more sophisticated setting, obtaining a flexible framework that can seamlessly handle different variants of the problem. We formally prove correctness of our approach and implement it in the conformance checker cocomot. Finally, we perform a thorough experimental evaluation on synthetic and real-life logs, demonstrating the overall promising performance of our framework.

So far, approaches for business process modeling, enactment and monitoring have mainly based on process specifications consisting of a single process model. This setting aptly captures monolithic scenarios from domains in which all possible behaviors can be folded into a single model. However, this strategy cannot be applied to domains where multiple interacting (procedural) processes simultaneously work over the same objects, in the presence of additional (declarative) constraints relating activities from the same or different processes. A relevant example for this setting is that of healthcare, where co-morbid patients may be subject to multiple clinical pathways at once, in the presence of additional, general constraints capturing basic medical knowledge. To fill this gap, we have previously presented the M3 Framework and an accompanying monitoring technique, which allows for a hybrid representation of a process using both procedural and declarative models, and supports the modular creation of multi-process specifications where domain experts can focus on specific procedures and domain constraints without being forced to merge them into one single specification. In this paper, we make significant extensions to this framework, allowing us to go from simple toy examples towards addressing practical real-life scenarios. We achieve this by introducing a richer form of integration between the interacting process components, in particular supporting asynchronous and synchronous activities that may operate over local and global (shared) data variables. This is framed by a discussion of the business meaning of these concepts, the introduction of the corresponding modeling patterns, and the application of our approach to real-life business processes, the latter being the driving-force behind this paper.

Conformance checking is a key process mining task to confront the normative behavior imposed by a process model with the actual behavior recorded in a log. While this problem has been extensively studied for pure control-flow processes, data-aware conformance checking has received comparatively little attention. In this paper, we tackle the conformance checking problem for the challenging scenario of processes that combine data and control-flow dimensions. Concretely, we adopt the formalism of data Petri nets (DPNs) and show how solid, well-established automated reasoning techniques from the area of Satisfiability Modulo Theories (SMT) can be effectively harnessed to compute conformance metrics and optimal data-aware alignments. To this end, we introduce the CoCoMoT (Computing Conformance Modulo Theories) framework, with a fourfold contribution. First, we show how SMT allows to leverage SAT-based encodings for the pure control-flow setting to the data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering, to speed up the computation of conformance checking outputs. Third, we show how our approach extends seamlessly to the more comprehensive conformance checking artifacts of multi- and anti-alignments. Fourth, we describe a proof-of-concept implementation based on state-of-the-art SMT solvers, and report on experiments. Finally, we discuss how CoCoMoT directly lends itself to further process mining tasks like log analysis by clustering and model repair, and the use of SMT facilitates the support of even richer multi-perspective models, where, for example, more expressive DPN guards languages are considered or generic datatypes (other than integers or reals) are employed.

As the need to understand and formalise business processes into a model has grown over the last years, the process discovery research field has gained more and more importance, developing two different classes of approaches to model representation: procedural and declarative. Orthogonally to this classification, the vast majority of works envisage the discovery task as a one-class supervised learning process guided by the traces that are recorded into an input log. In this work instead, we focus on declarative processes and embrace the less-popular view of process discovery as a binary supervised learning task, where the input log reports both examples of the normal system execution, and traces representing a “stranger” behaviour according to the domain semantics. We therefore deepen how the valuable information brought by both these two sets can be extracted and formalised into a model that is “optimal” according to user-defined goals. Our approach, namelyNegDis, is evaluated w.r.t. other relevant works in this field, and shows promising results regarding both the performance and the quality of the obtained solution.

Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet concise framework of data-aware dynamic systems (DDS), extending it with linear arithmetic, and providing the following contributions. First, we introduce a new, semantic property of “finite summary”, which guarantees the existence of a faithful finite-state abstraction. We rely on this to show that checking whether a witness exists for a linear-time, finite-trace property is decidable for DDSs with finite summary. Second, we demonstrate that several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. This also gives rise to new decidability results. Third, we show how the abstract, uniform property of finite summary leads to modularity results: a system enjoys finite summary if it can be partitioned appropriately into smaller systems that possess the property. Our results allow us to analyze systems that were out of reach in earlier approaches. Finally, we demonstrate the feasibility of our approach in a prototype implementation.

We address the problem of model checking first-order dynamic systems where new objects can be injected in the active domain during execution. Notable examples are systems induced by a first-order action theory, e.g., expressed in the Situation Calculus. Recent results have shown that, under the state-boundedness assumption, such systems, in spite of having a first-order representation of the state, admit decidable model checking for full first-order mu-calculus. However, interestingly, model checking remains undecidable in the case of first-order LTL (LTL-FO). In this paper, we show that in LTL-FOp, which is the fragment of LTL-FO in which quantification is over objects that persist along traces, model checking state-bounded systems becomes decidable over finite and infinite traces. We then employ this result to show how to handle monitoring of LTL-FOp properties against a trace stemming from an unknown state-bounded dynamic system, simultaneously considering the finite trace up to the current point, and all its possibly infinite future continuations.

Abstract Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that covers may not exist in the combined theories, even in case combined quantifier-free interpolants do exist. However, we exhibit a cover transfer algorithm operating also in the non-convex case for special kinds of theory combinations; these combinations (called ‘tame combinations’) concern multi-sorted theories arising in many model-checking applications (in particular, the ones oriented to verification of data-aware processes).

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 ltl f , a variant of the classical ltl (Linear-time Temporal Logic) that is interpreted over finite traces, and in its extension ldl f , a powerful logic obtained by combining ltl f with regular expressions. We show that ldl f 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 ldl f 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 ldl f formulae and their corresponding monitors, and the RuM rule mining suite as underlying infrastructure.

Abstract This special issue of Theory and Practice of Logic Programming consists of extended versions of five selected papers from the 3rd International Joint Conference on Rules and Reasoning (RuleML+RR 2019). RuleML+RR 2019 was held in conjunction with the 5th Global Conference on Artificial Intelligence, GCAI 2019, as part of the Bolzano Rules and Artificial INtelligence Summit in Bolzano, Italy, from 17 to 19 of September 2019.

We study the problem of verifying whether a given parameterized multi-agent system (PMAS) is safe, namely whether none of its possible executions can lead to bad states. These are captured by a state formula existentially quantifying over agents. As the MAS is parameterized, it only describes the finite set of possible agent templates, while the actual number of concrete agent instances that will be present at runtime, for each template, is unbounded and cannot be foreseen. We solve this problem via infinite-state model checking based on satisfiability modulo theories (SMT), relying on the theory of array-based systems. We formally characterize the soundness, completeness and termination guarantees of our approach under specific assumptions. This gives us a technique that is implementable on top of third-party, SMT-based model checkers. Finally, we discuss how this approach lends itself to richer parameterized and data-aware MAS settings beyond the state-of-the-art solutions in the literature.

Alignments provide sophisticated diagnostics that pinpoint deviations in a trace with respect to a process model. Alignment-based approaches for conformance checking have so far used crisp process models as a reference. Recent probabilistic conformance checking approaches check the degree of conformance of an event log as a whole with respect to a stochastic process model, without providing alignments. For the first time, we introduce a conformance checking approach based on trace alignments using stochastic Workflow nets. This requires to handle the two possibly contrasting forces of the cost of the alignment on the one hand and the likelihood of the model trace with respect to which the alignment is computed on the other.

Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isolation, however, especially in BPM it is also of interest to express properties over the entire log, i.e., properties that relate multiple traces of the log at once. In the case of infinite-traces, HyperLTL has been proposed to express these ``hyper'' properties. In this paper, motivated by BPM, we introduce HyperLDLf, a logic that extends LDLf with the hyper features of HyperLTL. We provide a sound, complete and computationally optimal technique, based on DFAs manipulation, for the model checking problem in the relevant case where the set of traces (i.e., the log) is a regular language. We illustrate how this form of model checking can be used for verifying log of business processes and for advanced forms of process mining.

Traditionally Business Process Modeling has only focused on the control-flow perspective, thus allowing process designers to specify the constraints on the activities of the process: the order and potential concurrency of their execution, their mutual exclusivity, the possibility of being repeated, etc. However, activities are executed by different resources, manipulate data objects and are constrained by the state of such objects. This requires that the traditional notion of soundness, typically introduced for control-flow-only models, is extended so as to consider data. Intuitively, a (data-aware) process model is sound if (1) it does not contain deadlocks, (2) no more activities are enabled when the process instance is marked as completed and finally (3) there are no parts of the model that cannot be executed. Although several data-aware notations have been introduced in the literature, not all of these are given a formal semantics. In this paper, we propose a technique for checking the data-aware soundness for a specific class of such integrated models, with a simple syntax and semantics, building on Data Petri Nets (DPNs). These are Petri nets enriched with case variables, where transitions are guarded by formulas that inspect and update such variables, and are of the form variable-operator-variable or variable-operator-constant. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data, allowing to model complex data-aware decisions. We show that, if a DPN is data-aware sound, the Constraint Graph is a finite-state automaton; however, a finite-state Constraint Graph does not guarantee data-aware soundness, but provides a finite structure through which this property can be checked. Finally, we investigate further properties beyond data-aware soundness, such as the problem of verifying that an actor participating in the business process can unilaterally enforce data-aware soundness by restricting the possible executions of a bounded DPN, assuming this actor to be able to control the firing of some transitions and decide the value of some of the case variables whenever these are updated.

This special issue contains revised and extended versions of papers presented at the 33rd Italian Conference on Computational Logic -CILC 2018 -which was held in Bolzano, Italy, on September 20-22, 2018.CILC is the annual conference organized by GULP (Group of researchers and Users of Logic Programming).Since the first event of the series, which took place in Genoa in 1986, the annual GULP conference represents the main opportunity for Italian users, researchers and developers working in the field of computational logic to meet and exchange ideas.Over the years the conference broadened its horizons from the specific field of logic programming to include declarative programming and applications in neighboring areas such as artificial intelligence and deductive databases.The authors of selected papers were invited to submit an improved, extended version to this special issue of Fundamenta Informaticae.Those papers went through a careful review by qualified international referees.The three papers in the special issue witness the multifaceted nature of CILC, covering important topics in temporal databases, description logics, and formal verification:

Enterprise Application Integration (EAI) constitutes the cornerstone in enterprise IT landscapes that are characterized by heterogeneity and distribution. Starting from established Enterprise Integration Patterns (EIPs) such as Content-based Router and Aggregator, EIP compositions are built to describe, implement, and execute integration scenarios. The EIPs and their compositions must be correct at design and runtime in order to avoid functional errors or incomplete functionalities. However, current EAI system vendors use many of the EIPs as part of their proprietary integration scenario modeling languages that are not grounded on any formalism. This renders correctness guarantees for EIPs and their composition impossible. Thus this work advocates responsible EAI based on the formalization, implementation, and correctness of EIPs. For this, requirements on an EIP formalization are collected and based on these requirements an extension of db-net, i.e., timed db-net , is proposed, fully equipped with execution semantics. It is shown how EIPs can be realized based on timed db-nets and how the correctness of these realizations can be shown. Moreover, the simulation of EIP realizations based on timed db-nets is enabled which is essential for later implementation. The concepts are evaluated in many ways, including a proof-of-concept implementation and case studies. The EIP formalization based on timed db-nets constitutes the first step towards responsible EAI.

Abstract Uniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

Temporal logics over finite traces have recently seen wide application in a number of areas, from business process modelling, monitoring, and mining to planning and decision making. However, real-life dynamic systems contain a degree of uncertainty which cannot be handled with classical logics. We thus propose a new probabilistic temporal logic over finite traces using superposition semantics, where all possible evolutions are possible, until observed. We study the properties of the logic and provide automata-based mechanisms for deriving probabilistic inferences from its formulas. We then study a fragment of the logic with better computational properties. Notably, formulas in this fragment can be discovered from event log data using off-the-shelf existing declarative process discovery techniques.

Previous works on formalizing enterprise application integration (EAI) scenarios showed an emerging need for setting up formal foundations for integration patterns, the EAI building blocks, in order to facilitate model-driven development of enterprise applications and ensure their correctness. So far, the formalization requirements were focusing on more "conventional" integration scenarios, in which control-flow, transactional persistent data and time aspects were considered. However, none of these works took into consideration another arising EAI trend that covers social and multimedia computing. In this work we propose a Petri net-based formalism that addresses requirements arising from the multimedia domain. We also demonstrate how to realize some of the most frequently used multimedia patterns and discuss which implications our formal proposal may bring into the area of the multimedia EAI development.

The integrated modeling and analysis of dynamic systems and the data they manipulate has been long advocated, on the one hand, to understand how data and corresponding decisions affect the system execution, and on the other hand to capture how actions occurring in the systems operate over data. KR techniques proved successful in handling a variety of tasks over such integrated models, ranging from verification to online monitoring. In this paper, we consider a simple, yet relevant model for data-aware dynamic systems (DDSs), consisting of a finite-state control structure defining the executability of actions that manipulate a finite set of variables with an infinite domain. On top of this model, we consider a data-aware version of reactive synthesis, where execution strategies are built by guaranteeing the satisfaction of a desired linear temporal property that simultaneously accounts for the system dynamics and data evolution.

Abstract In recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

The prominent role of normative primitives for regulating interactions in enterprise systems makes their representation and inspection a crucial task. In particular, querying the states of norms is essential to assess the accountability and compliance of interacting parties, as well as to reconstruct the historical evolution of their mutual contractual relationships. The main issue, however, is that the temporal data stored during the operation of the enterprise system are typically at a low level of abstraction, and do not directly refer to norms and their states. To overcome this problem, we propose the QUEN framework for querying norm states on top of legacy relational databases. QUEN builds on the temporal extension of the well-established framework of Ontology-Based Data Access (OBDA) to semantically represent normative primitives and their temporal states, and to map them to the underlying legacy data. The distinctive feature of QUEN is that mappings are not arbitrarily expressed by the modeler, but are instead automatically synthesized starting from a specification that explicitly indicates how the constitutive components of a normative primitive, as well as its lifecycle, can be reconstructed from the legacy data.

Checking the compliance of a business process execution with respect to a set of regulations is an important issue in several settings. A common way of representing the expected behavior of a process is to describe it as a set of business constraints. Through monitoring facilities, it is possible to continuously determine the state of constraints on the current process execution, and to promptly detect violations at runtime. A plethora of studies has demonstrated that in several settings business constraints can be formalized in terms of temporal logic rules. However, in most of the existing works, the process behavior is mainly modeled in terms of control-flow rules, neglecting other equally important perspectives like data or time. In this paper, we overcome this limitation by presenting a novel monitoring approach based on MP-Declare, a multi-perspective version of the declarative process modeling language Declare. The approach has been implemented in the process mining tool ProM and has been experimented using artificial and real-life event logs.

A prominent research direction of the database theory community is to develop techniques for verification of database-driven systems operating over relational and numerical data. Along this line, we lift the framework of database manipulating systems \citeAbdullaAAMR-pods-16 which handle relational data to also accommodate numerical data and the natural order on them. We study an under-approximation called recency bounding under which the most basic verification problem --reachability, is decidable. Even under this under-approximation the reachability space is infinite in multiple dimensions -- owing to the unbounded sizes of the active domain, the unbounded numerical domain it has access to, and the unbounded length of the executions. We show that, nevertheless, reachability is ExpTime complete. Going beyond reachability to LTL model checking renders verification undecidable.

Abstract The Decision Model and Notation (DMN) is a recent Object Management Group standard for the elicitation and representation of decision models and for managing their interconnection with business processes. DMN builds on the notion of decision tables and their combination into more complex decision requirements graphs (DRGs), which bridge between business process models and decision logic models. DRGs may rely on additional, external business knowledge models, whose functioning is not part of the standard. In this work, we consider one of the most important types of business knowledge, namely, background knowledge that conceptually accounts for the structural aspects of the domain of interest, and propose decision knowledge bases (DKBs), which semantically combine DRGs modeled in DMN, and domain knowledge captured by means of first-order logic with datatypes. We provide a logic-based semantics for such an integration, and formalize different DMN reasoning tasks for DKBs. We then consider background knowledge formulated as a description logic (DL) ontology with datatypes, and show how the main verification tasks for DMN in this enriched setting can be formalized as standard DL reasoning services and actually carried out in ExpTime. We discuss the effectiveness of our framework on a case study in maritime security.

Enterprise Integration Patterns (EIPs) and their extensions denote the informally described building blocks of current Enterprise Application Integration (EAI) systems. Although a recent approach strives to provide an EIP formalization based on Coloured Petri Nets (CPNs), it does not completely consider EAI requirements, such as complex data, transacted resources and time. In the absence of a comprehensive formal definition, the patterns cannot be verified, and thus a formal foundation of EAI is missing. In this work, we leverage the novel db-net approach that finds a better balance between the data and process-related aspects than CPNs and we extend it according to the EAI requirements that we systematically collect on a pattern level. Then we discuss pattern realizations, and evaluate our approach for comprehensiveness, test correctness, and show its applicability.

The compliance verification task amounts to establishing if the execution of a system, given in terms of observed happened events, does respect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to assess compliance in differen t domains, such as normative multi-agent systems, business process management and service oriented computing. In this work we review the LTL and SCIFF frameworks in the light of compliance evaluation, and formally investigate the relationship between the two approaches. We define a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by providing a translation procedure from LTL to SCIFF which preserves compliance.

The capability to store data about Business Process (BP) executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provi sion of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions in the BP community. In this paper, we introduce the notion of Structured Processes with Observability and Time (SPOT models), able to support incompleteness (of traces and logs), and temporal constraints on the activity duration and between activities. Then, we exploit the power of abduction to provide a flexible, yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform way.

The need to extend business process languages with the capability to model complex data objects along with the control flow perspective has lead to significant practical and theoretical advances in the field of Business Process Modeling (BPM).On the practical side, there are several suites for control flow and data modeling; nonetheless, when it comes to formal verification, the data perspective is abstracted away due to the intrinsic difficulty of handling unbounded data. On the theoretical side, there is significant literature providing decidability results for expressive data-aware processes. However, they struggle to produce a concrete impact as being far from real BPM architectures and, most of all, not providing actual verification tools. In this paper we aim at bridging such a gap: we provide a concrete framework which, on the one hand, being based on Petri Nets and relational models, is close to the widely used BPM suites, and on the other is grounded on solid formal basis which allow to perform formal verification tasks. Moreover, we show how to encode our framework in an action language so as to perform reachability analysis using virtually any state-of-the-art planner.

The capability to store data about Business Process executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provision of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions. In this paper we exploit the power of abduction to provide a flexible, and yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform and effective way.

We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a (DMS) modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. (DMS) is a highly expressive model and can be thought of as a succinct representation of an infinite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of (DMS) against (MSO-FO) is undecidable. Towards decidability, we propose under-approximate model checking of (DMS), where the under-approximation parameter is the "bound on recency". In a k-recency-bounded run, only the most recent k elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of (DMS) against (MSO-FO) is decidable, by a reduction to the satisfiability problem of MSO over nested words.

Abstract Petri nets with name creation and management ( ν -PNs) have been recently introduced as an expressive model for dynamic (distributed) systems, whose dynamics are determined not only by how tokens flow in the system, but also by the pure names they carry. On the one hand, this extension makes the resulting nets strictly more expressive than P/T nets: they can be exploited to capture a plethora of interesting systems, such as distributed systems enriched with channels and name passing, service interaction with correlation mechanisms, and resource-constrained workflow nets that explicitly account for process instances. On the other hand, fundamental properties like coverability, termination and boundedness are decidable for ν -PNs. In this work, we go one step beyond the verification of such general properties, and provide decidability and undecidability results of model checking ν -PNs against variants of first-order μ -calculus, recently proposed in the area of data-aware process analysis. While this model checking problem is undecidable in the general case, decidability can be obtained by considering different forms of boundedness, which still give raise to an infinite-state transition system. We then ground our framework to tackle the problem of soundness checking over workflow nets enriched with explicit process instances and resources. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of data-aware business processes working over full-fledged relational databases with constraints. In this light, our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and that of foundations of data-aware processes, which has not been extensively investigated so far.

We study the extension of relational multiagent systems (RMASs), where agents manipulate full-fledged relational databases, with data types and facets equipped with domain-specific, rigid relations (such as total orders). Specifically, we focus on design-time verification of RMASs against rich first-order temporal properties expressed in a variant of first-order mu-calculus with quantification across states. We build on previous decidability results under the state-bounded assumption, i.e., in each single state only a bounded number of data objects is stored in the agent databases, while unboundedly many can be encountered over time. We recast this condition, showing decidability in presence of dense, linear orders, and facets defined on top of them. Our approach is based on the construction of a finite-state, sound and complete abstraction of the original system, in which dense linear orders are reformulated as non-rigid relations working on the active domain of the system only. We also show undecidability when including a data type equipped with the successor relation.

In recent years, monitoring the compliance of business processes with relevant regulations, constraints, and rules during runtime has evolved as major concern in literature and practice. Monitoring not only refers to continuously observing possible compliance violations, but also includes the ability to provide fine-grained feedback and to predict possible compliance violations in the future. The body of literature on business process compliance is large and approaches specifically addressing process monitoring are hard to identify. Moreover, proper means for the systematic comparison of these approaches are missing. Hence, it is unclear which approaches are suitable for particular scenarios. The goal of this paper is to define a framework for Compliance Monitoring Functionalities (CMF) that enables the systematic comparison of existing and new approaches for monitoring compliance rules over business processes during runtime. To define the scope of the framework, at first, related areas are identified and discussed. The CMFs are harvested based on a systematic literature review and five selected case studies. The appropriateness of the selection of CMFs is demonstrated in two ways: (a) a systematic comparison with pattern-based compliance approaches and (b) a classification of existing compliance monitoring approaches using the CMFs. Moreover, the application of the CMFs is showcased using three existing tools that are applied to two realistic data sets. Overall, the CMF framework provides powerful means to position existing and future compliance monitoring approaches.

In this paper we study when an LTL formula on finite traces (LTLf formula) is insensitive to infiniteness, that is, it can be correctly handled as a formula on infinite traces under the assumption that at a certain point the infinite trace starts repeating an end event forever, trivializing all other propositions to false. This intuition has been put forward and (wrongly) assumed to hold in general in the literature. We define a necessary and sufficient condition to characterize whether an LTLf formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTLf specification patterns used in process and service modeling in CS, as well as trajectory constraints in Planning and transition-based LTLf specifications of action domains in KR, are indeed very often insensitive to infiniteness. This may help to explain why the assumption of interpreting LTL on finite and on infinite traces has been (wrongly) blurred. Possibly because of this blurring, virtually all literature detours to Buechi automata for constructing the NFA that accepts the traces satisfying an LTLf formula. As a further contribution, we give a simple direct algorithm for computing such NFA.

Artifact-centric business process models have gained increasing momentum recently due to their ability to combine structural (i.e., data related) with dynamical (i.e., process related) aspects. In particular, two main lines of research have been pursued so far: one tailored to business artifact modeling languages and methodologies, the other focused on the foundations for their formal verification. In this paper, we merge these two lines of research, by showing how recent theoretical decidability results for verification can be fruitfully transferred to a concrete UML-based modeling methodology. In particular, we identify additional steps in the methodology that, in significant cases, guarantee the possibility of verifying the resulting models against rich first-order temporal properties. Notably, our results can be seamlessly transferred to different languages for the specification of the artifact lifecycles.

Checking the compliance of a business process execution with respect to a set of regulations is an important issue in several settings. A common way of representing the expected behavior of a process is to describe it as a set of business constraints. Runtime verification and monitoring facilities allow us to continuously determine the state of constraints on the current process execution, and to promptly detect violations at runtime. A plethora of studies has demonstrated that in several settings business constraints can be formalized in terms of temporal logic rules. However, in virtually all existing works the process behavior is mainly modeled in terms of control-flow rules, neglecting the equally important data perspective. In this paper, we overcome this limitation by presenting a novel monitoring approach that tracks streams of process events (that possibly carry data) and verifies if the process execution is compliant with a set of data-aware business constraints, namely constraints not only referring to the temporal evolution of events, but also to the temporal evolution of data. The framework is based on the formal specification of business constraints in terms of first-order linear temporal logic rules. Operationally, these rules are translated into finite state automata for dynamically reasoning on partial, evolving execution traces. We show the versatility of our approach by formalizing (the data-aware extension of) Declare, a declarative, constraint-based process modeling language, and by demonstrating its application on a concrete case dealing with web security.

To support the whole business process compliance lifecycle, one also needs to monitor the actual processes and not just check their design. Recently, many approaches have been proposed that utilize a broad range of constraint languages and techniques to realize compliance monitoring solutions. Due to this diversity, the comparison of existing approaches is difficult and consequently hampers the evaluation of which approaches are suitable for which application scenarios. This paper provides a framework to compare and evaluate existing compliance monitoring approaches. The framework is based on ten typical Compliance Monitoring Functionalities (CMFs). These have been derived using a systematic literature review and five case studies from different domains. Existing approaches are evaluated based on the CMF framework, resulting in a list of open questions and a discussion of new challenges in this field.

In this work we survey the research on foundations of data-aware (business) processes that has been carried out in the database theory community. We show that this community has indeed developed over the years a multi-faceted culture of merging data and processes. We argue that it is this community that should lay the foundations to solve, at least from the point of view of formal analysis, the dichotomy between data and processes still persisting in business process management.

Data-centric dynamic systems are systems where both the process controlling the dynamics and the manipulation of data are equally central. We study verification of (first-order) mu-calculus variants over relational data-centric dynamic systems, where data are maintained in a relational database, and the process is described in terms of atomic actions that evolve the database. Action execution may involve calls to external services, thus inserting fresh data into the system. As a result such systems are infinite-state. We show that verification is undecidable in general, and we isolate notable cases where decidability is achieved. Specifically we start by considering service calls that return values deterministically (depending only on passed parameters). We show that in a mu-calculus variant that preserves knowledge of objects appeared along a run we get decidability under the assumption that the fresh data introduced along a run are bounded, though they might not be bounded in the overall system. In fact we tie such a result to a notion related to weak acyclicity studied in data exchange. Then, we move to nondeterministic services and we investigate decidability under the assumption that knowledge of objects is preserved only if they are continuously present. We show that if infinitely many values occur in a run but do not accumulate in the same state, then we get again decidability. We give syntactic conditions to avoid this accumulation through the novel notion of "generate-recall acyclicity", which ensures that every service call activation generates new values that cannot be accumulated indefinitely.

Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where the unique name assumption is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order mu-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.

Today, large business processes are composed of smaller, autonomous, interconnected subsystems, achieving modularity and robustness. Quite often, these large processes comprise software components as well as human actors, they face highly dynamic environments and their subsystems are updated and evolve independently of each other. Due to their dynamic nature and complexity, it might be difficult, if not impossible, to ensure at design-time that such systems will always exhibit the desired/expected behaviors. This, in turn, triggers the need for runtime verification and monitoring facilities. These are needed to check whether the actual behavior complies with expected business constraints, internal/external regulations and desired best practices. In this work, we present Mobucon EC, a novel monitoring framework that tracks streams of events and continuously determines the state of business constraints. In Mobucon EC, business constraints are defined using the declarative language Declare. For the purpose of this work, Declare has been suitably extended to support quantitative time constraints and non-atomic, durative activities. The logic-based language Event Calculus (EC) has been adopted to provide a formal specification and semantics to Declare constraints, while a light-weight, logic programming-based EC tool supports dynamically reasoning about partial, evolving execution traces. To demonstrate the applicability of our approach, we describe a case study about maritime safety and security and provide a synthetic benchmark to evaluate its scalability.

We propose $${\mathcal{B}}$$ -Tropos as a modeling framework to support agent-oriented systems engineering, from high-level requirements elicitation down to execution-level tasks. In particular, we show how $${\mathcal{B}}$$ -Tropos extends the Tropos methodology by means of declarative business constraints, inspired by the ConDec graphical language. We demonstrate the functioning of $${\mathcal{B}}$$ -Tropos using a running example inspired by a real-world industrial scenario, and we describe how $${\mathcal{B}}$$ -Tropos models can be automatically formalized in computational logic, discussing formal properties of the resulting framework and its verification capabilities.

Despite their dynamic nature, social commitments have rarely been used for monitoring purposes. Little attention has been paid to the relationship between commitments and the temporal dimension and to the corresponding run-time verification. Building on previous work, we present a declarative axiomatization of time-aware social commitments, extending their basic life cycle with time-related transitions and compensation mechanisms. The formalization is based on a reactive version of the event calculus, able to monitor the commitment's evolution during a system's execution, to check whether the interacting agents are honoring them or not. The resulting monitoring framework can be used in the context of agent-based simulation, either to dynamically evaluate whether a running simulation is compliant with a commitment-based contract or to provide useful information to the interacting agents, helping them to behave in a compliant manner.

Since its introduction, the Event Calculus (ℰ𝒞) has been recognized for being an excellent framework to reason about time and events, and it has been applied to a variety of domains. However, its formalization inside logic-based frameworks has been

We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework’s theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and it is guaranteed to terminate when applied to models that contain loops.

Service-oriented computing, an emerging paradigm for architecting and implementing business collaborations within and across organizational boundaries, is currently of interest to both software vendors and scientists. While the technologies for implementing and interconnecting basic services are reaching a good level of maturity, modeling service interaction from a global viewpoint, that is, representing service choreographies, is still an open challenge. The main problem is that, although declarativeness has been identified as a key feature, several proposed approaches specify choreographies by focusing on procedural aspects, leading to over-constrained and over-specified models. To overcome these limits, we propose to adopt DecSerFlow, a truly declarative language, to model choreographies. Thanks to its declarative nature, DecSerFlow semantics can be given in terms of logic-based languages. In particular, we present how DecSerFlow can be mapped ontoLinear Temporal Logicand ontoAbductive Logic Programming. We show how the mappings onto both formalisms can be concretely exploited to address the enactment of DecSerFlow models, to enrich its expressiveness and to perform a variety of different verification tasks. We illustrate the advantages of using a declarative language in conjunction with logic-based semantics by applying our approach to a running example.

In semantic Web technologies, searching for a service means to identify components that can potentially satisfy the user needs in terms of outputs and effects (discovery), and that, when invoked by the customer, can fruitfully interact with her (contracting). In this paper, we present an application framework that encompasses both the discovery and the contracting steps, in a unified search process. In particular, we accommodate service discovery by ontology-based reasoning, and contracting by automated reasoning about policies published in a formal language. To this purpose, we consider a formal approach grounded on computational logic, and abductive logic programming in particular. We propose a framework, called SCIFF reasoning engine, able to establish, by ontological and abductive reasoning, if a semantic Web service and a requester can fruitfully inter-operate, taking as input the behavioral interfaces of both the participants, and producing as output a sort of a contract.

Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user.In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules; suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined.Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies. We adapt the SCIFF\ framework for the new settings, and propose a heir of SCIFF, the framework AlLoWS (Abductive Logic Web-service Specification).. AlLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, AlLoWS has a declarative and an operational semantics. We show examples of how AlLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, AlLoWS deals seamlessly with other cases involving constraints and deadlines

We propose to adopt a formalism, based on social integrity constraints (ICs), for specifying social interactions between actors involved in a guideline. ICs allow us to represent interaction protocols using a logic formalism and to perform an on-the-fly verification of the protocol's application compliance, based on an abductive proof procedure which operates on relevant events occurred during its application. The paper presents the results of a first trial performed on a microbiological clinical guideline which exploits the potentialities of the formalism in representing and verifying the compliance to medical guidelines.