arXiv subjects

Riccardo De Masellis

Publications and source records attributed to Riccardo De Masellis.

10 recordsLinked to original sources

arXiv2020

Solving reachability problems on data-aware workflows

Recent advances in the field of Business Process Management have brought about several suites able to model complex data objects along with the traditional control flow perspective. Nonetheless, when it comes to formal verification there is still the lack of effective verification tools on imperative data-aware process models and executions: the data perspective is often abstracted away and verification tools are often missing. In this paper we provide a concrete framework for formal verification of reachability properties on imperative data-aware business processes. We start with an expressive, yet empirically tractable class of data-aware process models, an extension of Workflow Nets, and we provide a rigorous mapping between the semantics of such models and that of three important paradigms for reasoning about dynamic systems: Action Languages, Classical Planning, and Model Checking. Then we perform a comprehensive assessment of the performance of three popular tools supporting the above paradigms in solving reachability problems for imperative data-aware business processes, which paves the way for a theoretically well founded and practically viable exploitation of formal verification techniques on data-aware business processes.

cs.AI↗

arXiv2020

Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces

Runtime monitoring is one of the central tasks in the area of operational decision support for business process management. In particular, 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 on finite traces (LTLf), and in its extension LDLf. LDLf is a powerful logic that captures all monadic second order logic on finite traces, and that is obtained by combining regular expressions with LTLf, adopting the syntax of propositional dynamic logic (PDL). Interestingly, in spite of its greater expressivity, \LDLf has exactly the same computational complexity of LTLf. We show that LDLf 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 LDLf 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. In addition, we devise a direct translation of LDLf formulae into nondeterministic finite-state automata, avoiding to detour to Buchi automata or alternating automata. We then report on how this approach has been effectively implemented using Java to manipulate LDLf formulae and their corresponding monitors, and the well-known ProM process mining suite as underlying operational decision support infrastructure.

cs.LO↗

arXiv2020

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems

We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems (HDMAS). Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic (ATL), where one can specify properties of the type "a coalition of (at least) $n$ controllable agents can ensure against (at most) $m$ uncontrollable agents that any possible evolution of the system satisfies a given objective $φ$", where $φ$ is specified again as a formula of that language and each of $n$ and $m$ is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic $\mathcal{L}_{HDMAS}$ and define normal form of its formulae. We then prove that every formula in $\mathcal{L}_{HDMAS}$ is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

cs.LO↗

arXiv2017

Enhancing workflow-nets with data for trace completion

The growing adoption of IT-systems for modeling and executing (business) processes or services has thrust the scientific investigation towards techniques and tools which support more complex forms of process analysis. Many of them, such as conformance checking, process alignment, mining and enhancement, rely on complete observation of past (tracked and logged) executions. In many real cases, however, the lack of human or IT-support on all the steps of process execution, as well as information hiding and abstraction of model and data, result in incomplete log information of both data and activities. This paper tackles the issue of automatically repairing traces with missing information by notably considering not only activities but also data manipulated by them. Our technique recasts such a problem in a reachability problem and provides an encoding in an action language which allows to virtually use any state-of-the-art planning to return solutions.

cs.AI↗

arXiv2017

Learning Hybrid Process Models From Events: Process Discovery Without Faking Confidence

Process discovery techniques return process models that are either formal (precisely describing the possible behaviors) or informal (merely a "picture" not allowing for any form of formal reasoning). Formal models are able to classify traces (i.e., sequences of events) as fitting or non-fitting. Most process mining approaches described in the literature produce such models. This is in stark contrast with the over 25 available commercial process mining tools that only discover informal process models that remain deliberately vague on the precise set of possible traces. There are two main reasons why vendors resort to such models: scalability and simplicity. In this paper, we propose to combine the best of both worlds: discovering hybrid process models that have formal and informal elements. As a proof of concept we present a discovery technique based on hybrid Petri nets. These models allow for formal reasoning, but also reveal information that cannot be captured in mainstream formal models. A novel discovery algorithm returning hybrid Petri nets has been implemented in ProM and has been applied to several real-life event logs. The results clearly demonstrate the advantages of remaining "vague" when there is not enough "evidence" in the data or standard modeling constructs do not "fit". Moreover, the approach is scalable enough to be incorporated in industrial-strength process mining tools.

cs.SE↗

arXiv2016

Abducing Compliance of Incomplete Event Logs

The capability to store data about business processes execution in so-called Event Logs has brought to the diffusion of tools for the analysis of process executions and for the assessment of the goodness of a process model. Nonetheless, these tools are often very rigid in dealing with with Event Logs that include incomplete information about the process execution. Thus, while the ability of handling incomplete event data is one of the challenges mentioned in the process mining manifesto, the evaluation of compliance of an execution trace still requires an end-to-end complete trace to be performed. This paper exploits the power of abduction to provide a flexible, yet computationally effective, framework to deal with different forms of incompleteness in an Event Log. Moreover it proposes a refinement of the classical notion of compliance into strong and conditional compliance to take into account incomplete logs. Finally, performances evaluation in an experimental setting shows the feasibility of the presented approach.

cs.AI↗

arXiv2015

A Declarative Framework for Specifying and Enforcing Purpose-aware Policies

Purpose is crucial for privacy protection as it makes users confident that their personal data are processed as intended. Available proposals for the specification and enforcement of purpose-aware policies are unsatisfactory for their ambiguous semantics of purposes and/or lack of support to the run-time enforcement of policies. In this paper, we propose a declarative framework based on a first-order temporal logic that allows us to give a precise semantics to purpose-aware policies and to reuse algorithms for the design of a run-time monitor enforcing purpose-aware policies. We also show the complexity of the generation and use of the monitor which, to the best of our knowledge, is the first such a result in literature on purpose-aware policies.

cs.CR↗

arXiv2014

LTLf and LDLf Monitoring: A Technical Report

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

cs.AI↗

arXiv2014

Description Logic Knowledge and Action Bases

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.

cs.AI↗

arXiv2013

Verification of Artifact-Centric Systems: Decidability and Modeling Issues

Artifact-centric business processes have recently emerged as an approach in which processes are centred around the evolution of business entities, called artifacts, giving equal importance to control-flow and data. The recent Guard-State-Milestone (GSM) approach provides means for specifying business artifacts lifecycles in a declarative manner, using constructs that match how executive-level stakeholders think about their business. However, it turns out that formal verification of GSM is undecidable even for very simple propositional temporal properties. We attack this challenging problem by translating GSM into a well-studied formal framework. We exploit this translation to isolate an interesting class of state-bounded GSM models for which verification of sophisticated temporal properties is decidable. We then introduce some guidelines to turn an arbitrary GSM model into a state-bounded, verifiable model.

cs.SE↗