11 citations · 43 across the 24 of their papers we have counts for
25 papers
ARCCS: An Automated Regulatory Compliance Checking System
Giorgos Filandrianos, José Menezes, Chrysoula Zerva +1
Regulatory compliance checking - deciding whether a target document satisfies the obligations of a regulation - requires interpreting dense legal text, identifying which provisions…
Detecting Dynamic Relationships in Object-Centric Event Logs
Alessandro Gianola, Zeeshan Hameed, Marco Montali +3
Object-centric process mining examines how processes interact with multiple co-evolving objects, and has gained great interest in recent years. However, object-centric event logs (…
To bind or not to bind? Discovering Stable Relationships in Object-centric Processes (Extended Version)
Anjo Seidel, Sarah Winkler, Alessandro Gianola +2
Object-centric process mining investigates the intertwined behavior of multiple objects in business processes. From object-centric event logs, object-centric Petri nets (OCPN) can…
Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended)
Jacobo Casas-Ramos, Sarah Winkler, Alessandro Gianola +3
Despite growing interest in process analysis and mining for data-aware specifications, alignment-based conformance checking for declarative process models has focused on pure contr…
Object-centric Processes with Structured Data and Exact Synchronization (Extended Version)
Alessandro Gianola, Marco Montali, Sarah Winkler
Real-world processes often involve interdependent objects that also carry data values, such as integers, reals, or strings. However, existing process formalisms fall short to combi…
A General Automata Model for First-Order Temporal Logics (Extended Version)
Luca Geatti, Alessandro Gianola, Nicola Gigante
First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general…
Object-Centric Conformance Alignments with Synchronization (Extended Version)
Alessandro Gianola, Marco Montali, Sarah Winkler
Real-world processes operate on objects that are inter-dependent. To accurately reflect the nature of such processes, object-centric process mining techniques are needed, notably c…
Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata (Extended Version)
Alessandro Gianola, Marco Montali, Sarah Winkler
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-…
Decidable Fragments of LTLf Modulo Theories (Extended Version)
Luca Geatti, Alessandro Gianola, Nicola Gigante +1
We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by firs…
Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)
Silvio Ghilardi, Alessandro Gianola, Marco Montali +1
Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Dat…
Conformance Checking with Uncertainty via SMT (Extended Version)
Paolo Felli, Alessandro Gianola, Marco Montali +2
Logs of real-life processes often feature uncertainty pertaining the recorded timestamps, data values, and/or events. We consider the problem of checking conformance of uncertain l…
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
Luca Geatti, Alessandro Gianola, Nicola Gigante
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spir…
General Interpolation and Strong Amalgamation for Contiguous Arrays
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur +1
Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the dat…
SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version)
Diego Calvanese, Alessandro Gianola, Andrea Mazzullo +1
In the context of verification of data-aware processes (DAPs), a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety pr…
CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version)
Paolo Felli, Alessandro Gianola, Marco Montali +2
Conformance checking is a key process mining task for comparing the expected behavior captured in a process model and the actual behavior recorded in a log. While this problem has…
Span(Graph): a Canonical Feedback Algebra of Open Transition Systems
Elena Di Lavore, Alessandro Gianola, Mario Román +2
We show that Span(Graph)*, an algebra for open transition systems introduced by Katis, Sabadini and Walters, satisfies a universal property. By itself, this is a justification of t…
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
In this paper, the theory of McCarthy's extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. I…
SMT-based Safety Verification of Parameterised Multi-Agent Systems
Paolo Felli, Alessandro Gianola, Marco Montali
In this paper we study the verification of parameterised multi-agent systems (MASs), and in particular the task of verifying whether unwanted states, characterised as a given state…
Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)
Silvio Ghilardi, Alessandro Gianola, Marco Montali +1
During the last decade, various approaches have been put forward to integrate business processes with different types of data. Each of such approaches reflects specific demands in…
Uniform Interpolants in EUF: Algorithms using DAG-representations
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the form…
Combined Covers and Beth Definability (Extended Version)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle infinite-state model checking problems. Motivated by applications to the verification of…
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
We propose DAB -- a data-aware extension of BPMN where the process operates over case and persistent data (partitioned into a read-only database called catalog and a read-write dat…
Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
We propose DAB -- a data-aware extension of the BPMN de-facto standard with the ability of operating over case and persistent data (partitioned into a read-only catalog and a read-…
Verification of Data-Aware Processes via Array-Based Systems (Extended Version)
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola +2
We study verification over a general model of artifact-centric systems, to assess (parameterized) safety properties irrespectively of the initial database instance. We view such ar…