Journals
2025
[12] A Formal Approach to Attack Graphs
Annals of Mathematics and Artificial Intelligence
Joint work with Davide Catta, Jean Leneutre, and Aniello Murano
[11] Reasoning about Decidability of Strategic Logics with Imperfect Information and Perfect Recall Strategies
Journal of Artificial Intelligence Research
Joint work with Davide Catta and Angelo Ferrando
[10] An SMT-Based Approach to the Verification of Knowledge-Based Programs
Formal Aspects of Computing
Joint work with Francesco Belardinelli, Ioana Boureanu, and Fortunat Rajaona
[9] Model Checking Strategic Abilities in Information-sharing Systems
ACM Transactions on Computational Logic
Joint work with Francesco Belardinelli, Ioana Boureanu, and Catalin Dima
2023
[8] Attack Graphs & Subset Sabotage Games
Intelligenza Artificiale
Joint work with Davide Catta and Jean Leneutre
[7] An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
Journal of Artificial Intelligence
Joint work with Francesco Belardinelli and Angelo Ferrando
2022
[6] Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
Journal of Artificial Intelligence Research
Joint work with Francesco Belardinelli, Alessio Lomuscio, and Emily Yu
[5] How to measure usable security: Natural strategies in voting protocols
Journal of Computer Security
Joint work with Wojtek Jamroga and Damian Kurpiewski
2019
[4] Natural Strategic Ability
Journal of Artificial Intelligence
Joint work with Wojtek Jamroga and Aniello Murano
2018
[3] Additional Winning Strategies in Reachability Games
Fundamenta Informaticae
Joint work with Aniello Murano and Loredana Sorrentino
[2] Graded Modalities in Strategy Logic
Information and Computation
Joint work with Benjamin Aminof, Aniello Murano, and Sasha Rubin
[1] Reasoning about Graded Strategy Quantifiers
Information and Computation
Joint work with Fabio Mogavero, Aniello Murano, and Loredana Sorrentino
Conferences
2025
[64] Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason about Demon Coalitions
34th International Joint Conference on Artificial Intelligence, IJCAI 2025
Joint work with Davide Catta, Jean Leneutre, and James Ortiz
[63] Agreement Games in Multi-Agent Systems
24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Joint work with Davide Catta and Angelo Ferrando
[62] FindMe: A prototype videogame AI based on CTL with an Optimized Synthesis Algorithm
24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Joint work with Marco Aruta, Aniello Murano, Vincenzo Pio Palma and Salvatore Romano
[61] VITAMIN: VerIficaTion of A MultI ageNt system
24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Joint work with Angelo Ferrando
[60] Timed Obstruction Logic: A Timed Approach to Dynamic Game Reasoning
24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Joint work with Jean Leneutre and James Ortiz
[59] Alternating-time Temporal Logic with Stochastic Abilities
24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025
Joint work with Gabriel Ballot, Jean Leneutre, Jingxuan Ma, and Mourad Leslous
[58] VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems
17th International Conference on Agents and Artificial Intelligence, ICAART 2025
Joint work with Angelo Ferrando
2024
[57] Solvent: Liquidity Verification of Smart Contracts
19th International Conference on Integrated Formal Methods, iFM 2024
Joint work with Massimo Bartoletti, Angelo Ferrando, and Enrico Lipparini
[56] Reasoning about Real-Time and Probability on Obstruction Logic
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2024
Joint work with Jean Leneutre and James Ortiz
[55] Development of Natural Strategies in Strategic Logics
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2024
Joint work with Marco Aruta and Aniello Murano
[54] Towards a Compositional and User-friendly Tool for Multi-Agent Systems Verification
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2024
Joint work with Angelo Ferrando
[53] Theory and Practice of Quantitative ATL
The 25th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2024
Joint work with Angelo Ferrando, Giulia Luongo, and Aniello Murano
[52] Resource Action-Based Bounded ATL: A New Logic for MAS to Express a Cost Over the Actions
The 25th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2024
Joint work with Davide Catta and Angelo Ferrando
[51] Obstruction Alternating-time Temporal Logic: A Strategic Logic to Reason about Dynamic Models
23th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024
Joint work with Davide Catta, Jean Leneutre, and Aniello Murano
[50] Strategic Reasoning under Capacity-constrained Agents
23th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024
Joint work with Gabriel Ballot, Jean Leneutre, and Youssef Laarouchi
[49] A Formal Verification Approach to Handle Attack Graphs
16th International Conference on Agents and Artificial Intelligence, ICAART 2024
Joint work with Davide Catta, Jean Leneutre, Antonina Mijatovic, and Johanna Ulin
[48] Hands-on VITAMIN: A Compositional Tool for Model Checking of Multi-Agent Systems
25nd Workshop "From Objects to Agents", WOA 2024
Joint work with Angelo Ferrando
2023
[47] RMLGym: a Formal Reward Machine Framework for Reinforcement Learning
24nd Workshop "From Objects to Agents", WOA 2023
Joint work with Francesco Belardinelli, Angelo Ferrando, and Hisham Unniyankal
[46] HYASM: A Tool to Verify Hierarchical Systems
IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023
Joint work with Angelo Ferrando, Aniello Murano, and Silvia Stranieri
[45] Reasoning about Intuitionistic Computation Tree Logic
Third Workshop on Agents and Robots for reliable Engineered Autonomy, AREA 2023
Joint work with Davide Catta and Aniello Murano
[44] The Impact of Strategies and Information in Model Checking for Multi-Agent Systems
Third Workshop on Agents and Robots for reliable Engineered Autonomy, AREA 2023
[43] 3vLTL: A Tool to Generate Automata for Three-valued LTL
Fifth International Workshop on Formal Methods for Autonomous Systems, FMAS 2023
Francesco Belardinelli and Angelo Ferrando
[42] Coalition Alternating-Time Temporal Logic: A Logic to Find Good Coalitions to Achieve Strategic Objectives
Agents and Artificial Intelligence - 15th International Conference, ICAART 2023, Revised Selected Papers
Joint work with Davide Catta and Angelo Ferrando
[41] Reasoning About Dynamic Game Models Using Obstruction Logic
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2023
Joint work with Davide Catta and Jean Leneutre
[40] Obstruction Logic: a Strategic Temporal Logic to Reason about Dynamic Game Models
26th European Conference on Artificial Intelligence, ECAI 2023
Joint work with Davide Catta and Jean Leneutre
[39] Scalable Verification of Strategy Logic through Three-Valued Abstraction
32th International Joint Conference on Artificial Intelligence, IJCAI 2023
Joint work with Francesco Belardinelli, Angelo Ferrando, Wojtek Jamroga, and Aniello Murano
[38] Towards the Verification of Strategic Properties in Multi-Agent System with Imperfect Information
22th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2023
Joint work with Angelo Ferrando
[37] Automatically Verifying Expressive Epistemic Properties of Programs
The Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023
Joint work with Francesco Belardinelli, Ioana Boureanu, and Fortunat Rajaona
[36] Program Semantics and Verification Technique for AI-Centred Programs
Formal Methods - 25th International Symposium, FM 2023 (BEST PAPER AWARD)
Joint work with Francesco Belardinelli, Ioana Boureanu, and Fortunat Rajaona
[35] How to Find Good Coalitions to Achieve Strategic Objectives
15th International Conference on Agents and Artificial Intelligence, ICAART 2023
Joint work with Angelo Ferrando
[34] A Game Theoretic Approach to Attack Graphs
15th International Conference on Agents and Artificial Intelligence, ICAART 2023
Joint work with Davide Catta, Antonio Di Stasio, Jean Leneutre, and Aniello Murano
2022
[33] Give Me a Hand: How to Use Model Checking for Multi-Agent Systems to Help Runtime Verification and Vice Versa
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2022
Joint work with Angelo Ferrando
[32] Towards a Formal Verification of Attack Graphs
Workshop on Strategies, Prediction, Interaction, and Reasoning, SPIRIT 2022
Joint work with Davide Catta and Jean Leneutre
[31] Reasoning about MTD in Attack Modeling Formalisms
9th ACM Workshop on Moving Target Defense, MTD 2022
Joint work with Gabriel Ballot, Jean Leneutre, and Etienne Borde
[30] Runtime Verification with Imperfect Information through Indistinguishability Relations
20th International Conference on Software Engineering and Formal Methods, SEFM 2022
Joint work with Angelo Ferrando
[29] Subset Sabotage Games & Attack Graphs
23nd Workshop "From Objects to Agents", WOA 2022
Joint work with Davide Catta and Jean Leneutre
[28] Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
20th International Conference of Practical Applications of Agents and Multi-Agent Systems, PAAMS 2022
Joint work with Angelo Ferrando
[27] Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions
21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022
Joint work with F. Belardinelli, W. Jamroga, M. Mittelmann , A. Murano, and L. Perrussel
[26] Enabling Markovian Representations under Imperfect Information
14th International Conference on Agents and Artificial Intelligence, ICAART 2022
Joint work with Francesco Belardinelli and Borja G. Leon
2021
[25] Combine Model Checking and Runtime Verification in Multi-Agent Systems
22nd Italian Conference on Theoretical Computer Science, ICTCS 2021
Joint work with Angelo Ferrando
[24] Towards a Model Checking Tool for Strategy Logic with Simple Goals
22nd Italian Conference on Theoretical Computer Science, ICTCS 2021
Joint work with Silvia Stranieri
[23] Strategy RV: A Tool to Approximate ATL Model Checking under Imperfect Information and Perfect Recall
20th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2021
Joint work with Angelo Ferrando
2020
[22] Natural Strategic Abilities in Voting Protocols
10th International Workshop on Socio-Technical Aspects in Security, STAST 2020
Joint work with Wojtek Jamroga and Damian Kurpiewski
[21] A Three-valued Approach to Strategic Abilities under Imperfect Information
17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020
Joint work with Francesco Belardinelli
[20] Verifying Strategic Abilities in Multi-agent Systems via First-order Entailment
24th European Conference on Artificial Intelligence, ECAI 2020
Joint work with Francesco Belardinelli
[19] A Hennessy-Milner Theorem for ATL with Imperfect Information
Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
July 8-11 2020, Saarbrücken, Germany
Joint work with Francesco Belardinelli, Catalin Dima, and Ferucio Tiplea
2019
[18] Decidable Verification of Agent-Based Data-Aware Systems
22nd International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2019
Joint work with Francesco Belardinelli
[17] Strategy Logic with Simple Goals: Tractable Reasoning about Strategies
28th International Joint Conference on Artificial Intelligence, IJCAI 2019
Joint work with Francesco Belardinelli, Wojtek Jamroga, Damian Kurpiewski, and Aniello Murano
[16] Natural Strategic Ability under Imperfect Information
18th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2019
Joint work with Wojtek Jamroga and Aniello Murano
[15] Verifying Strategic Abilities in Multi-agent Systems
with Private-Data Sharing
18th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2019
Joint work with Francesco Belardinelli, Ioana Boureanu, and Catalin Dima
[14] An Abstraction-based Method for Verifying Strategic Properties
in Multi-agent Systems with Imperfect Information
Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019
Joint work with Francesco Belardinelli and Alessio Lomuscio
2018
[13] Approximating Perfect Recall when Model Checking Strategic Abilities
16th International Conference on Principles of Knowledge Representation and Reasoning, KR 2018
Joint work with Francesco Belardinelli and Alessio Lomuscio
[12] Dynamic Escape Game
17th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2018
Joint work with Antonio Di Stasio, Paolo Domenico Lambiase, and Aniello Murano
2017
[11] Reasoning about Additional Winning Strategies in Two-Player Games
15th European Conference on Multi-Agent Systems, EUMAS 2017
Joint work with Aniello Murano
[10] Hiding Actions in Multi-Player Games
16th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2017
Joint work with Aniello Murano and Loredana Sorrentino
[9] Reasoning about Natural Strategic Ability
16th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2017
Joint work with Wojtek Jamroga and Aniello Murano
2016
[8] Additional Winning Strategies in Two-Player Games
17th Italian Conference on Theoretical Computer Science, ICTCS 2016
Joint work with Aniello Murano
[7] Hiding Actions in Concurrent Games
22nd European Conference on Artificial Intelligence, ECAI 2016
Joint work with Aniello Murano and Loredana Sorrentino
[6] Extended Graded Modalities in Strategy Logic
4th International Workshop on Strategic Reasoning, SR 2016
Joint work with Benjamin Aminof, Aniello Murano, and Sasha Rubin
[5] NWin: A Tool for Counting Winning Strategies
15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016
Joint work with Aniello Murano and Marco Tafuto
[4] Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria
15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016
Joint work with Benjamin Aminof, Aniello Murano, and Sasha Rubin
[3] Concurrent Multi-Player Parity Games
15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016
Joint work with Aniello Murano and Loredana Sorrentino
2015
[2] On the Counting of Strategies
22nd International Symposium on Temporal Representation and Reasoning, TIME15
Joint work with Fabio Mogavero, Aniello Murano, and Loredana Sorrentino
[1] Games with Additional Winning Strategies
XXX Convegno Italiano di Logica Computazionale, CILC15
Joint work with Aniello Murano and Loredana Sorrentino
Theses
2024
[4] Formal Modeling, Specification, and Verification of Multi-Agent Systems
HDR in Computer Science, Data, and AI. Institut Polytechnique de Paris, France, June 2024.
2018
[3] Strategic Reasoning in Game Theory
PhD in Mathematics and Computer Science. Universita' degli Studi di Napoli "Federico II", Italy, February 2018.
2014
[2] Graded modalities in strategic reasoning
Master degree in Computer Science. Universita' degli Studi di Napoli "Federico II", Italy, July 2014.
2010
[1] Implementazione di un algoritmo di verifica formale per programmi gerarchici nel tool Yasm
Bachelor degree in Computer Science. Universita' degli Studi di Napoli "Federico II", Italy, December 2010.