publications

2025

1. BPM Forum

   From Sound Workflow Nets to LTL_f Declarative Specifications by Casting Three Spells

   Luca Barbaro , Giovanni Varricchione, Marco Montali , and Claudio Di Ciccio

   In Proceedings of the BPM Forum, co-located with BPM 2025 (to appear) , Sep 2025

   Abs PDF

   In process management, effective behavior modeling is essential for understanding execution dynamics and identifying potential issues. Two complementary paradigms have emerged in the pursuit of this objective: the imperative approach, representing all allowed runs of a system in a graph-based model, and the declarative one, specifying the rules that a run must not violate in a constraint-based specification. Ex- tensive studies have been conducted on the synergy and comparisons of the two paradigms. To date, though, whether a declarative specification could be systematically derived from an imperative model such that the original behavior was fully preserved (and if so, how) remained an unanswered question. In this paper, we propose a three-fold contribu- tion. (1) We introduce a systematic approach to synthesize declarative process specifications from safe and sound Workflow nets. (2) We prove behavioral equivalence of the input net with the output specification, alongside related guarantees. (3) We experimentally demonstrate the scalability and compactness of our encoding through tests conducted with synthetic and real-world testbeds.

2024

1. AAAI

   Pure-Past Action Masking

   Giovanni Varricchione, Natasha Alechina , Mehdi Dastani , Giuseppe De Giacomo , Brian Logan , and Giuseppe Perelli

   In Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI 2024) , Feb 2024

   Abs PDF Poster

   We present Pure-Past Action Masking (PPAM), a lightweight aproach to action masking for safe reinforcement learning. In PPAM, actions are disallowed (“masked”) according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL). PPAM can enforce non-Markovian constraints, i.e., constraints based on the history of the system, rather than just the current state of the (possibly hidden) MDP. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent. We prove formally that an agent trained with PPAM can learn any optimal policy that satisfies the safety constraints, and that they are as expressive as shields, another approach to enforce non-Markovian constraints in RL. Finally, we provide empirical results showing how PPAM can guarantee constraint satisfaction in practice.

2. AiML

   Frame Definability in Conditional Logic

   Damiano Fornasiere , Johannes Marti , and Giovanni Varricchione

   In Proceedings of the 15th Conference on Advances in Modal Logic (AiML 2024) , Aug 2024

   Abs PDF

   In this paper we investigate classes of finite partially ordered sets that are definable by non-nested formulas in conditional logic. We discuss examples of such definable classes and introduce the notion of a c-morphism between posets as a tool to show that a class of finite posets is not definable. Using an analogue of the Jankov-Fine formulas from modal logic, we show that a class of finite posets is definable by a set of formulas if and only if it is closed under c-morphic images. Lastly, we prove a Sahlqvist-like correspondence theorem stating that every class of finite posets that is definable by a formula without nested conditionals is also definable by a first-order formula.

3. ECAI

   Maximally Permissive Reward Machines

   Giovanni Varricchione, Natasha Alechina , Mehdi Dastani , and Brian Logan

   In Proceedings of the 27th European Conference on Artificial Intelligence (ECAI 2024) , Oct 2024

   Abs PDF

   Reward machines allow the definition of rewards for temporally extended tasks and behaviors. Specifying “informative” reward machines can be challenging. One way to address this is to generate reward machines from a high-level abstract description of the learning environment, using techniques such as AI planning. However, previous planning-based approaches generate a reward machine based on a single (sequential or partial-order) plan, and do not allow maximum flexibility to the learning agent. In this paper we propose a new approach to synthesising reward machines which is based on the set of partial order plans for a goal. We prove that learning using such “maximally permissive” reward machines results in higher rewards than learning using RMs based on a single plan. We present experimental results which support our theoretical claims by showing that our approach obtains higher rewards than the single-plan approach in practice.

2023

1. EUMAS

   Synthesising Reward Machines for Cooperative Multi-Agent Reinforcement Learning

   Giovanni Varricchione, Natasha Alechina , Mehdi Dastani , and Brian Logan

   In Proceedings of the 20th European Conference on Multi-Agent Systems (EUMAS 2023) , Sep 2023

   Abs PDF Poster

   Reward machines have recently been proposed as a means of encoding team tasks in cooperative multi-agent reinforcement learning. The resulting multi-agent reward machine is then decomposed into individual reward machines, one for each member of the team, allowing agents to learn in a decentralised manner while still achieving the team task. However, current work assumes the multi-agent reward machine to be given. In this paper, we show how reward machines for team tasks can be synthesised automatically from an Alternating-Time Temporal Logic specification of the desired team behaviour and a high-level abstraction of the agents’ environment. We present results suggesting that our automated approach has comparable, if not better, sample efficiency than reward machines generated by hand for multi-agent tasks.