BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Marco Montali

Marco Montali contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Artificial IntelligenceLogic in Computer ScienceDatabasesMultiagent Systems

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
11works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

11 published item(s)

preprint2026arXiv

Monitoring Data-aware Temporal Properties (Extended Version)

Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and verification techniques such as model checking are not applicable. Monitoring is in such cases an attractive alternative, as it evaluates desirable properties along traces generated by an unknown dynamic system. In this work, we consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces (LTLfMT). Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations. Under reasonable assumptions on the background theory, we present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment of LTLfMT. The framework combines automata-theoretic methods to handle the temporal aspects of the logic, with automated reasoning techniques to address the first-order dimension. Moreover, we identify for the first time decidable fragments of this monitoring problem that are practically relevant as they combine linear arithmetic with uninterpreted functions, which covers e.g. data-aware business processes and dynamic systems operating over a read-only database. Feasibility is witnessed by a prototype implementation and preliminary evaluation.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Conformance Checking with Uncertainty via SMT (Extended Version)

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 logs against data-aware reference processes. Specifically, we show how to solve it via SMT encodings, lifting previous work on data-aware SMT-based conformance checking to this more sophisticated setting. Our approach is modular, in that it homogeneously accommodates for different types of uncertainty. Moreover, using appropriate cost functions, different conformance checking tasks can be addressed. We show the correctness of our approach and witness feasibility through a proof-of-concept implementation.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

CTL* model checking for data-aware dynamic systems with arithmetic

The analysis of complex dynamic systems is a core research topic in formal methods and AI, and combined modelling of systems with data has gained increasing importance in applications such as business process management. In addition, process mining techniques are nowadays used to automatically mine process models from event data, often without correctness guarantees. Thus verification techniques for linear and branching time properties are needed to ensure desired behavior. Here we consider data-aware dynamic systems with arithmetic (DDSAs), which constitute a concise but expressive formalism of transition systems with linear arithmetic guards. We present a CTL* model checking procedure for DDSAs that relies on a finite-state abstraction by means of a set of formulas that capture variable configurations. Linear-time verification was shown to be decidable in specific classes of DDSAs where the constraint language or the control flow are suitably confined. We investigate several of these restrictions for the case of CTL*, with both positive and negative results: CTL* verification is proven decidable for monotonicity and integer periodicity constraint systems, but undecidable for feedback free and bounded lookback systems. To demonstrate the feasibility of our approach, we implemented it in the SMT-based prototype ada, showing that many practical business process models can be effectively analyzed.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

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 provide 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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Soundness of Data-Aware Processes with Arithmetic Conditions

Data-aware processes represent and integrate structural and behavioural constraints in a single model, and are thus increasingly investigated in business process management and information systems engineering. In this spectrum, Data Petri nets (DPNs) have gained increasing popularity thanks to their ability to balance simplicity with expressiveness. The interplay of data and control-flow makes checking the correctness of such models, specifically the well-known property of soundness, crucial and challenging. A major shortcoming of previous approaches for checking soundness of DPNs is that they consider data conditions without arithmetic, an essential feature when dealing with real-world, concrete applications. In this paper, we attack this open problem by providing a foundational and operational framework for assessing soundness of DPNs enriched with arithmetic data conditions. The framework comes with a proof-of-concept implementation that, instead of relying on ad-hoc techniques, employs off-the-shelf established SMT technologies. The implementation is validated on a collection of examples from the literature, and on synthetic variants constructed from such examples.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

What Can Database Query Processing Do for Instance-Spanning Constraints?

In the last decade, the term instance-spanning constraint has been introduced in the process mining field to refer to constraints that span multiple process instances of one or several processes. Of particular relevance, in this setting, is checking whether process executions comply with constraints of interest, which at runtime calls for suitable monitoring techniques. Even though event data are often stored in some sort of database, there is a lack of database-oriented approaches to tackle compliance checking and monitoring of (instance-spanning) constraints. In this paper, we fill this gap by showing how well-established technology from database query processing can be effectively used for this purpose. We propose to define an instance-spanning constraint through an ensemble of four database queries that retrieve the satisfying, violating, pending-satisfying, and pending-violating cases of the constraint. In this context, the problem of compliance monitoring then becomes an application of techniques for incremental view maintenance, which is well-developed in database query processing. In this paper, we argue for our approach in detail, and, as a proof of concept, present an experimental validation using the DBToaster incremental database query engine.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Combined Covers and Beth Definability (Extended Version)

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 data-aware processes, we proved in a previous paper that covers are strictly related to model completions, a well-known topic in model theory. 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 (equality interpolation property aka strong amalgamation property) needed to transfer quantifier-free interpolation. 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).

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)

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 the whole process-data integration spectrum. One particular important point is the capability of these approaches to flexibly accommodate processes with multiple cases that need to co-evolve. In this work, we introduce and study an extension of coloured Petri nets, called catalog-nets, providing two key features to capture this type of processes. On the one hand, net transitions are equipped with guards that simultaneously inspect the content of tokens and query facts stored in a read-only, persistent database. On the other hand, such transitions can inject data into tokens by extracting relevant values from the database or by generating genuinely fresh ones. We systematically encode catalog-nets into one of the reference frameworks for the (parameterised) verification of data and processes. We show that fresh-value injection is a particularly complex feature to handle, and discuss strategies to tame it. Finally, we discuss how catalog nets relate to well-known formalisms in this area.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

SMT-based Safety Verification of Parameterised Multi-Agent Systems

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 formula, are reachable in a given MAS, i.e., whether the MAS is unsafe. The MAS is parameterised and the model only describes the finite set of possible agent templates, while the actual number of concrete agent instances for each template is unbounded and cannot be foreseen. This makes the state-space infinite. As safety may of course depend on the number of agent instances in the system, the verification result must be correct irrespective of such number. We solve this problem via infinite-state model checking based on satisfiability modulo theories (SMT), relying on the theory of array-based systems: we present parameterised MASs as particular array-based systems, under two execution semantics for the MAS, which we call concurrent and interleaved. We prove our decidability results under these assumptions and illustrate our implementation approach, called SAFE: the Swarm Safety Detector, based on the third-party model checker MCMT, which we evaluate experimentally. Finally, we discuss how this approach lends itself to richer parameterised and data-aware MAS settings beyond the state-of-the-art solutions in the literature, which we leave as future work.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Verification of Relational Data-Centric Dynamic Systems with External Services

Data-centric dynamic systems are systems where both the process controlling the dynamics and the manipulation of data are equally central. In this paper we study verification of (first-order) mu-calculus variants over relational data-centric dynamic systems, where data are represented by a full-fledged relational database, and the process is described in terms of atomic actions that evolve the database. The execution of such actions may involve calls to external services, providing fresh data inserted into the system. As a result such systems are typically 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 where the assumption of data bounded run would result in a bound on the service calls that can be invoked during the execution and hence would be too restrictive. So 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 takes into consideration that every service call activation generates new values that cannot be accumulated indefinitely.

0 citations0 reviewsNo code linkedOpen access