Publications
2025
- JAAMASBehqvioral QLTL.2025
This paper introduces Behavioral QLTL, a "behavioral" variant of Linear Temporal Logic (LTL) with second-order quantifiers. Behavioral qltl is characterized by the fact that the functions that assign the truth value of the quantified proposi tions along the trace can only depend on the past. In other words, such functions must be "processes". This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and ltl synthesis are expressed in Behavioral QLTL through formulas with a simple quantification alternation. As such alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original qltl (with non-behavioral semantics) and simpler forms of behavioral semantics.
@incollection{J-DP25, author = {{De Giacomo}, Giuseppe and Perelli, Giuseppe}, title = {Behqvioral QLTL.}, booktitle = {Autonomous Agent and Multi-Agent Systems}, year = {2025}, note = {to appear} } - KR-25LTL Synthesis under Multi-Agent Environment Assumptions.In 22nd International Conference on Principles of Knowledge Representation and Reasoning, KR 2025
We investigate LTL synthesis under structured assumptions about the environment. In our setting, the environment is viewed by the protagonist as a collection of peer agents acting together in a shared world. In contrast to the symmetrical frameworks typically studied in multi-agent systems, we take a strikingly asymmetric first-person perspective in which the protagonist ascribes a specification to each of its peer agents and the world, capturing its understanding of their possible strategies. We show that in this setting, LTL synthesis has the same computational complexity as standard LTL synthesis, i.e., 2EXPTIME-complete. We establish this via a sophisti cated, yet fully implementable, argument that builds on the notion of traces compatible with strategies: we use the fact that if the basic specification of the world and of each agent is given in LTL then the sets of traces compatible with the strategies describing the behaviors of the agents are omega- regular. This enables the use of word-automata rather than the more complicated tree-automata.
@inproceedings{C-ADPR25, author = {Aminof, Benjamin and {De Giacomo}, Giuseppe and Perelli, Giuseppe and Rubin, Sasha}, title = {{LTL Synthesis under Multi-Agent Environment Assumptions.}}, booktitle = {22nd International Conference on Principles of Knowledge Representation and Reasoning, {KR}}, year = {2025}, } - IJCAI-25Synthesising Minimum Cost Dynamic Norms.In 34th International Joint Conference on Artificial Intelligence, IJCAI 2025
A key problem in the design of normative multi- agent systems is the cost of enforcing a norm (for the system operator) or complying with the norm (for the system users). If the cost is too high, ensuring compliant behavior may be uneconomic, or users may be deterred from participating in the MAS. In this paper, we consider the problem of synthesizing minimum cost dynamic norms to satisfy a system-level objective specified in Alternating Time Temporal Logic (ATL^∗ ). We show that synthesizing a dynamic norm under a bound on the cost of any prohibited set of actions has the same complexity as synthesizing arbitrary norms. We also show that synthesizing norms that minimize the average cost of the prohibited set of actions is unsolvable; however, synthesizing ε-optimal norms is possible.
@inproceedings{C-ALP25, author = {Alechina, Natasha and Logan, Brian and Perelli, Giuseppe}, title = {{Synthesising Minimum Cost Dynamic Norms.}}, booktitle = {34th International Joint Conference on Artificial Intelligence, {IJCAI}}, year = {2025}, notes = {To appear} } - Enabling decision support over confidential dataMarangone, Edoardo, Nemmi, Eugenio Nerio, Friolo, Daniele, Ateniese, Giuseppe, Weber, Ingo, and Di Ciccio, Claudio2025
Enabling automated decision-making processes by leveraging data-driven analysis is a core goal of Decision Support Systems (DSSs). In multi-party scenarios where decisions rely on distributed and sensitive data, though, ensuring confidentiality, verifiability, transparency, integrity, and consistency at once remains an open challenge for DSSs. To tackle this multi-faceted problem, we propose the Secure Platform for Automated decision Rules via Trusted Applications (SPARTA) approach. By leveraging Trusted Execution Environments (TEEs) at its core, SPARTA ensures that the decision logic and the data remain protected. To guarantee transparency and consistency of the decision process, SPARTA encodes decision rules into verifiable software objects deployed within TEEs. To maintain the confidentiality of the outcomes while keeping the information integrity, SPARTA employs cryptography techniques on notarized data based on user-definable access policies. Based on experiments conducted on public benchmarks and synthetic data, we find our approach to be practically applicable and scalable.Enabling automated decision-making processes by leveraging data-driven analysis is a core goal of Decision Support Systems (DSSs). In multi-party scenarios where decisions rely on distributed and sensitive data, though, ensuring confidentiality, verifiability, transparency, integrity, and consistency at once remains an open challenge for DSSs. To tackle this multi-faceted problem, we propose the Secure Platform for Automated decision Rules via Trusted Applications (SPARTA) approach. By leveraging Trusted Execution Environments (TEEs) at its core, SPARTA ensures that the decision logic and the data remain protected. To guarantee transparency and consistency of the decision process, SPARTA encodes decision rules into verifiable software objects deployed within TEEs. To maintain the confidentiality of the outcomes while keeping the information integrity, SPARTA employs cryptography techniques on notarized data based on user-definable access policies. Based on experiments conducted on public benchmarks and synthetic data, we find our approach to be practically applicable and scalable.
@techreport{DBLP:journals/corr/abs-2509-02413, author = {Marangone, Edoardo and Nemmi, {Eugenio Nerio} and Friolo, Daniele and Ateniese, Giuseppe and Weber, Ingo and {Di Ciccio}, Claudio}, title = {Enabling decision support over confidential data}, journal = {CoRR}, volume = {abs/2509.02413}, year = {2025}, url = {https://doi.org/10.48550/arXiv.2509.02413}, doi = {10.48550/ARXIV.2509.02413}, eprinttype = {arXiv}, eprint = {2509.02413}, timestamp = {Sun, 12 Oct 2025 18:22:42 +0200} } - BPM Forum-25Balancing Confidentiality and Transparency for Blockchain-Based Process-Aware Information SystemsIn Business Process Management Forum 2025
Blockchain enables novel, trustworthy Process-Aware Information Systems (PAISs) by enforcing the security, robustness, and traceability of operations. In particular, transparency ensures that all information exchanges are openly accessible, fostering trust within the system. Although this is a desirable property to enable notarization and auditing activities, it also represents a limitation for such cases where confidentiality is a requirement since interactions involve sensitive data. Current solutions rely on obfuscation techniques or private infrastructures, hindering the enforcement capabilities of smart contracts and the public verifiability of transactions. Against this background, we propose CONFETTY, an architecture for blockchain-based PAISs to preserve confidentiality and transparency. Smart contracts enact, enforce and store public interactions, while attribute-based encryption techniques are adopted to specify access grants to confidential information. We assess the security of our solution through a systematic threat model analysis and evaluate its practical feasibility by gauging the performance of our implemented prototype in different scenarios from the literature.
@inproceedings{confetty, author = {Marcelletti, Alessandro and Marangone, Edoardo and Kryston, Michele and {Di Ciccio}, Claudio}, editor = {Senderovich, Arik and Cabanillas, Cristina and Vanderfeesten, Irene and A. Reijers, Hajo}, title = {Balancing Confidentiality and Transparency for Blockchain-Based Process-Aware Information Systems}, booktitle = {Business Process Management Forum}, year = {2025}, publisher = {Springer Nature Switzerland}, address = {Cham}, pages = {238--255} } - CAiSE Forum-25MARTSIA: A Tool for Confidential Data Exchange via Public BlockchainKryston, Michele, Marangone, Edoardo, Di Ciccio, Claudio, Friolo, Daniele, Nemmi, Eugenio Nerio, Samory, Mattia, Spina, Michele, Venturi, Daniele, and Weber, IngoIn Intelligent Information Systems - CAiSE 2025 Forum and Doctoral Consortium 2025
Blockchain technology streamlines multi-party collaborations in decentralized settings, especially when trust is limited or difficult to establish. While public blockchains enhance transparency and reliability by replicating data across all network nodes, they also conflict with confidentiality. Here, we introduce Multi-Authority Approach to Transaction Systems for Interoperating Applications (MARTSIA) to address this challenge. MARTSIA provides fine-grained read-access control at the message-part level by combining user-defined policies with certifier-declared attributes. The approach guarantees that even though data is replicated across the network to maintain consistency, fault tolerance, and availability, its confidentiality is securely preserved through encryption. To this end, MARTSIA integrates blockchain technologies, Multi-Authority Attribute-Based Encryption, and distributed hash-table file storages. This architecture effectively balances the transparency inherent in public blockchains with the privacy required for sensitive applications. We present the tool and its applicability in a business scenario.
@inproceedings{Kryston2025MARTSIA, author = {Kryston, Michele and Marangone, Edoardo and {Di Ciccio}, Claudio and Friolo, Daniele and Nemmi, {Eugenio Nerio} and Samory, Mattia and Spina, Michele and Venturi, Daniele and Weber, Ingo}, editor = {Pufahl, Luise and Rosenthal, Kristina and Espa{\~{n}}a, Sergio and Nurcan, Selmin}, title = {{MARTSIA:} {A} Tool for Confidential Data Exchange via Public Blockchain}, booktitle = {Intelligent Information Systems - CAiSE 2025 Forum and Doctoral Consortium}, series = {Lecture Notes in Business Information Processing}, volume = {557}, pages = {173--180}, publisher = {Springer}, year = {2025} } - BLINK: Blockchain-Linked Network for Credit Guarantee InstitutionsLeo, Sabrina, Delle Foglie, Andrea, Barbaro, Luca, Marangone, Edoardo, Panetta, Ida Claudia, and Di Ciccio, Claudio2025
Credit Guarantee Institutions (CGIs) provide a fundamental contribution in alleviating the financial constraints faced by a specific group of borrowers. However, critics highlight significant weaknesses, including the limited ability to maintain financial stability and operational effectiveness. This paper presents a framework for leveraging DLTs, specifically blockchain technologies, in CGI processes to enhance. To achieve this, we analyse critical architectural characteristics, considering access level, governance structure, and consensus method, to assess how well they align with CGI processes. This study has the potential to provide valuable guidance to policymakers and stakeholders, encouraging continued innovation in this promising field.
@techreport{Leo.etal/BLINK, year = {2025}, author = {Leo, Sabrina and {Delle Foglie}, Andrea and Barbaro, Luca and Marangone, Edoardo and Panetta, Ida Claudia and {Di Ciccio}, Claudio}, title = {BLINK: Blockchain-Linked Network for Credit Guarantee Institutions}, note = {Accepted for publication at Financial Innovation Journal} }
2024
- LMCSDesigning Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints.2024
In game theory, mechanism design is concerned with the design of incentives so that a desirable outcome will be achieved under the assumption that players act rationally. In this paper, we explore the concept of equilibrium design, where incentives are designed to obtain a desirable equilibrium that satisfies a specific temporal logic property. Our study is based on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players’ goals as mean-payoff objectives. We consider system specifications given by LTL and GR(1) formulae, and show that designing incentives to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game can be achieved in PSPACE for LTL properties and in NP/Σ^P_2 for GR(1) specifications. We also examine the complexity of related decision and optimisation problems, such as optimality and uniqueness of solutions, as well as considering social welfare, and show that the complexities of these problems lie within the polynomial hierarchy. Equilibrium design can be used as an alternative solution to rational synthesis and verification problems for concurrent games with mean-payoff objectives when no solution exists or as a technique to repair concurrent games with undesirable Nash equilibria in an optimal way.
@incollection{J-GNPW24, author = {Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael}, title = {Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints.}, booktitle = {Logical Methods in Computer Science}, year = {2024}, volume = {20}, issue = {4}, note = {To appear}, } - DL-24Optimal Alignment of Temporal Knowledge Bases (Extended Abstract).In 37th International Workshop on Description Logics, DL 2024
Answering temporal CQs over temporalized Description Logic knowledge bases (TKB) is a main technique to realize ontology-based situation recognition. In case the collected data in such a knowledge base is inaccurate, important query answers can be missed. In this paper we introduce the TKB Alignment problem, which computes a variant of the TKB that minimally changes the TKB, but entails the given temporal CQ and is in that sense (cost-)optimal. We investigate this problem for ALC TKBs and conjunctive queries with LTL operators and devise a solution technique to compute (cost-optimal) alignments of TKBs that extends techniques for the alignment problem for propositional LTL over finite traces.
@inproceedings{C-FPPT24, author = {Fernandez-Gil, Oliver and Patrizi, Fabio and Perelli, Giuseppe and Turhan, Anni-Yasmin}, title = {Optimal Alignment of Temporal Knowledge Bases (Extended Abstract).}, booktitle = {37th International Workshop on Description Logics, {DL}}, year = {2024}, volume = {3739}, publisher = {CEUR-WS.org}, } - KR-24Incentive Design for Rational Agents.In 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024
We introduce Incentive Design: a new class of problems for equilibrium verification in multi-agent systems. In our model, agents attempt to maximize their utility functions, which are expressed as formulae in LTL[F], a quantitative extension of Linear Temporal Logic with functions computable in polynomial time. We assume agents are rational, in the sense that they adopt strategies consistent with game theoretic solution concepts such as Nash equilibrium. For each solution concept we consider, we analyze the problems of verifying whether an incentive scheme achieves a societal objective and finding one that does so, whether it be social welfare or any other aggregate measure of collective well-being. We study both static and dynamic incentive schemes, showing that the latter are more powerful than the former. Finally, we solve the incentive verification and synthesis problems for all the solution concepts we consider, and analyze their complexity.
@inproceedings{C-JHNPW24, author = {Hyland, David and Mittelmann, Munyque and Murano, Aniello and Perelli, Giuseppe and Wooldridge, Michael}, title = {Incentive Design for Rational Agents.}, booktitle = {21st International Conference on Principles of Knowledge Representation and Reasoning, {KR}}, year = {2024}, } - ECAI-24Synthesis of Reward Machines for Multi-Agent Equilibrium Design.In 27th European Conference on Artificial Intelligence, ECAI 2024
Mechanism design is a well-established paradigm in game theory, and it is concerned with designing games to achieve desired outcomes. This paper addresses a closely related but distinct concept, equilibrium design. Unlike mechanism design, the designer’s authority in equilibrium design is more constrained; she can only modify the incentive structures in a given game to achieve certain outcomes without the ability to create the game from scratch. We study the problem of equilibrium design using dynamic incentive structures, known as reward machines. We use weighted concurrent game structures for the game model, with goals (for the players and the designer) defined as mean-payoff objectives. We show how reward machines can be used to represent dynamic incentives that allocate rewards in a manner that optimises the designer’s goal. We also introduce the main decision problem within our framework, the payoff improvement problem. This problem essentially asks whether there exists a dynamic incentive (represented by some reward machine) that can improve the designer’s payoff by more than a given threshold value. We present two variants of the problem: strong and weak. We demonstrate that both can be solved in polynomial time using a Turing machine equipped with an NP oracle. Furthermore, we also establish that these variants are either NP-hard or coNP-hard. Finally, we show how to synthesise the corresponding reward machine if it exists.
@inproceedings{C-JHNPW25, author = {Najib, Muhammad and Perelli, Giuseppe}, title = {Synthesis of Reward Machines for Multi-Agent Equilibrium Design.}, booktitle = {27th European Conference on Artificial Intelligence, {ECAI}}, year = {2024}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {392}, pages = {2733--2740}, publisher = {{IOS} Press}, } - ISoLA-24Strategies in Spatio-Temporal Logics for Multi-Agent SystemsIn 12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024
In distributed agent systems, agents with different abilities work autonomously to reach a common task, in the face of challenges posed by their environment. Two types of structures shape the collective behaviour of the system: a temporal one, defined by the progression of states the system goes through, and a spatial one, defined by the various constraints imposed by the environment on agents’ moves. We argue that both structures can be modelled in terms of suitable topologies, giving rise to a common categorical structure, namely that of trees labelled over a well-founded meet-semilattice, which in turn originates specific kinds of propositional and modal logics. As a result, it is immediate to model some sort of temporal logic on the properties of state sequences, with properties expressed as terms of the spatial logic. The same formalisation can be used to define the strategies determining the actual behavior of the agents. The modularity of the approach implies a theoretical simplification and suggests the possibility of a variety of applications.
@inproceedings{C-BLP24, author = {Bottoni, Paolo and Labella, Anna and Perelli, Giuseppe}, title = {{Strategies in Spatio-Temporal Logics for Multi-Agent Systems}}, booktitle = {12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, {ISoLA}}, series = {Lecture Notes in Computer Science}, volume = {15219}, pages = {287--305}, publisher = {Springer}, year = {2024}, } - IJCAI-24Endogenous Energy Reactive Modules Games: Modelling Side Payments Among Resource-Bounded Agents.In 33rd International Joint Conference on Artificial Intelligence, IJCAI 2024
We introduce Energy Reactive Modules Games (ERMGs), an extension of Reactive Modules Games (RMGs) in which actions incur an energy cost (which may be positive or negative), and the choices that players make are restricted by the energy available to them. In ERMGs, each action is associated with an energy level update, which determines how their energy level is affected by the performance of the action. In addition, agents are provided with an initial energy allowance. This allowance plays a crucial role in shaping an agent’s behaviour, as it must be taken into consideration when one is determining their strategy: agents may only perform actions if they have the requisite energy. We begin by studying rational verification for ERMGs, and then introduce Endogenous ERMGs, where agents can choose to transfer their energy to other agents. This exchange may enable equilibria that are impossible to achieve without such transfers. We study the decision problem of whether a stable outcome exists under both the Nash equilibrium and Core solution concepts.
@inproceedings{C-JHNPW26, author = {Gutierrez, Julian and Hyland, David and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael}, title = {Endogenous Energy Reactive Modules Games: Modelling Side Payments Among Resource-Bounded Agents.}, booktitle = {33rd International Joint Conference on Artificial Intelligence, {IJCAI}}, pages = {67--75}, publisher = {ijcai.org}, year = {2024}, } - AAMAS-24Playing Quantitative Games Against an Authority: On the Module Checking Problem.In 23rd International Conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2024
Module checking is a decision problem to formalize the verification of (possibly multi-agent) systems that must adapt their behavior to the input they receive from the environment, also viewed as an authority. So far, module checking has been only considered in the Boolean setting, which does not capture the different levels of quality inherent to complex systems (e.g., systems dealing with quantitative utilities or sensor inputs). In this paper, we address this issue by proposing quantitative module checking. We study the problem in the quantitative and multi-agent setting, which enables the verification of different levels of satisfaction in relation to a specification. We consider specifications given in Quantitative Alternating-time Temporal logics and investigate the complexity and expressivity results.
@inproceedings{C-JMMP24, author = {Jamroga, Wojtek and Mittelmann, Munyque and Murano, Aniello and Perelli, Giuseppe}, title = {Playing Quantitative Games Against an Authority: On the Module Checking Problem.}, booktitle = {23rd International Conference on Autonomous Agents and Multi-Agent Systems, {AAMAS}}, pages = {926--934}, publisher = {{ACM}}, year = {2024}, } - AAAI-24Pure-Past Action Masking.Alechina, Natasha, Dastani, Mehdi, De Giacomo, Giuseppe, Logan, Brian, Perelli, Giuseppe, and Varricchione, GiovanniIn 38th Annual AAAI Conference on Artificial Intelligence, AAAI 2024
We present Pure-Past Action Masking (PPAM), a lightweight approach 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.
@inproceedings{C-ADDLPV24, author = {Alechina, Natasha and Dastani, Mehdi and {De Giacomo}, Giuseppe and Logan, Brian and Perelli, Giuseppe and Varricchione, Giovanni}, title = {Pure-Past Action Masking.}, booktitle = {38th Annual AAAI Conference on Artificial Intelligence, {AAAI}}, pages = {21646--21655}, publisher = {{AAAI} Press}, year = {2024}, }