Author name cluster

Jean Leneutre

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

AAMAS Conference 2026 Conference Paper

A Verification Framework for Obstruction, Probability, and Time

Wissal Dahani
Jean Leneutre
Vadim Malvone
James Ortiz
Axel Oscar

Verifying strategic behaviour in real-time multi-agent systems under uncertainty is vital for safety- and security-critical domains. Existing obstruction logics treat either adversarial timing (TOL) or probabilistic risk (POTL), but real scenarios require both. We introduceProbabilisticTimedObstructionTemporalLogic (PTOTL), which unifies dense time, probabilities, and cost-bounded obstruction for real-time security games. Interpreted over Weighted Probabilistic Timed Automaton (WPTA), PTOTL models attacker–defender interactions where discrete actions evolve and time elapses, and the defender may disable transitions under a per-step budget. We give syntax and semantics and a symbolic model-checking procedure on a probabilistic zone graph. Despite the added strategic and probabilistic features, verification remains PSPACE, not higher than PTCTL or PTATL, while offering greater temporal expressiveness. An automotive Moving Target Defense (MTD) case study demonstrates practicality as a specification and verification language.

PDF

AAMAS Conference 2025 Conference Paper

Alternating-time Temporal Logic with Stochastic Abilities

Gabriel Ballot
Vadim Malvone
Jean Leneutre
Jingxuan Ma
Mourad Leslous

Multi-agent systems strategic verification is a branch of formal methods to model, reason about, and verify strategic behavior in complex environments. The notion of agent capacity was introduced alongside the strategic logic CapATL to model multi-agent systems in which each player may exhibit diverse abilities or profiles. These capacities can represent various aspects, such as an agent’s experience level, personality traits, type, or version. In realworld applications, domain knowledge or prior statistical analyses may provide a probability distribution over the possible profiles of each agent. This leads to the concept of stochastic abilities, where capacities are assigned probabilistically, yet remain private to other agents. In this context, we introduce a novel probabilistic strategic logic, called ATL-SA, that allows the expression of properties concerning the likelihood that agents or coalitions can achieve specific temporal objectives under uncertainty about their capacities. We study the upper and lower complexity bounds of ATL-SA model checking and demonstrate its practical applicability through a use case in cybersecurity, showcasing its potential for analysing systems with probabilistic agent profiles.

PDF

IJCAI Conference 2025 Conference Paper

Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason About Demon Coalitions

Davide Catta
Jean Leneutre
Vadim Malvone
James Ortiz

In multi-agent systems, especially in cybersecurity, the dynamic interplay between attackers and defenders is crucial to the security and resilience of the system. Traditional methods often assume static game models and fail to account for the strategic adaptation of the environment to the actions of the players. This paper presents Coalition Obstruction Temporal Logic (COTL), a formal framework for analyzing defender coalitions in dynamic game scenarios. Within this framework, defenders, conceptualized as demons, can actively obstruct attackers by selectively disabling certain actions in response to perceived threats. We establish the formal semantics of COTL and propose a model checking algorithm to verify complex security properties in systems with evolving adversarial dynamics. The utility of the framework is demonstrated through its application to a coalition of defenders that collaboratively defend a system against coordinated attacks.

PDF Details DOI

ECAI Conference 2025 Conference Paper

Strategic Reasoning with Capacity-Constrained Agents and Imperfect Information

Gabriel Ballot
Vadim Malvone
Jean Leneutre
Jingxuan Ma

Multi-Agent System (MAS) verification comprises formal techniques to model distributed systems, express system properties, and verify them. Capacity Alternating-time Temporal Logic (CapATL) was recently introduced to reason about MASs where agents can have different profiles, called capacities. However, CapATL assumes agents know the global system state throughout the interaction, which is a strong constraint. This paper extends the concept of agent capacities to systems with imperfect information, enabling the formalisation of a wide range of systems which were previously out of reach. Our contributions are: (i) an extension with imperfect information of CapATL, called Capacity Alternating-time Temporal Epistemic Logic (CapATEL), (ii) the analysis and comparison of different semantics, (iii) a completeness result for the CapATEL model-checking problem when agents have bounded recall, and (iv) a cybersecurity illustration that showcases CapATEL’s applicability.

Details

AAMAS Conference 2025 Conference Paper

Timed Obstruction Logic: A Timed Approach to Dynamic Game Reasoning

Jean Leneutre
Vadim Malvone
James Ortiz

Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. Recently, a growing literature has recognized Timed Game Theory as a sound theoretical foundation for modeling strategic interactions between attackers and defenders. This paper proposes Timed Obstruction Logic (TOL), a formalism for verifying specific timed games with real-time objectives unfolding in dynamic models. These timed games involve players whose discrete and continuous actions can impact the underlying timed game model. We show that TOL can be used to describe important timed properties of real-time cybersecurity games. Finally, we provide a verification procedure for TOL and show that its complexity is PSPACE-complete, meaning that it is not higher than that of classical timed temporal logics like TCTL. Thus, we increase the expressiveness of properties without incurring any additional complexity.

PDF

AAMAS Conference 2024 Conference Paper

Obstruction Alternating-time Temporal Logic: A Strategic Logic to Reason about Dynamic Models

Davide Catta
Jean Leneutre
Vadim Malvone
Aniello Murano

Multi-Agent Systems (MAS) operating within dynamic models have been extensively studied in various domains, including cybersecurity and planning. In this paper, we introduce a dedicated logic for analyzing a specific category of MAS that involve strategic objectives within dynamic models. Within these MAS, there exists an agent known as the “Demon”, which possesses the capability to modify the MAS model itself, while other agents operate as traditional MAS entities. We demonstrate that the model-checking problem for our logic is solvable in polynomial time. Furthermore, we showcase how this logic can be effectively employed to articulate significant properties within the realm of cybersecurity.

PDF

AAMAS Conference 2024 Conference Paper

Strategic Reasoning under Capacity-constrained Agents

Gabriel Ballot
Vadim Malvone
Jean Leneutre
Youssef Laarouchi

Personality traits, experience level, or physical characteristics can affect the capacity (or profile) of an agent. For instance, a basketball player may be right-handed or left-handed, and these two versions cannot do the same actions. Dribbling past the player may require, first, understanding its handedness and, accordingly, execute a trick. Generally, capacities apply to systems where multiple entities can play the same role in the system, such as different client versions in protocol analysis, different robots in heterogeneous fleets, different personality traits in social structure modeling, or different attacker profiles in cybersecurity. With the capacity of other agents being unknown at the system’s initialization, the hardness of imperfect information arises. Our contributions are: (i) introducing Capacity Alternating-time Temporal Logic (CapATL) to reason about concurrent game structure where agents are bounded to capacities, (ii) a model-checking algorithm for CapATL, and (iii) a case study of adaptive honeypot design for cyber deception.

PDF

ECAI Conference 2023 Conference Paper

Obstruction Logic: A Strategic Temporal Logic to Reason About Dynamic Game Models

Davide Catta
Jean Leneutre
Vadim Malvone

Games that are played in a dynamic model have been studied in several contexts, such as cybersecurity and planning. In this paper, we introduce a logic for reasoning about a particular class of games with temporal goals played in a dynamic model. In such games, the actions of a player can modify the game model itself. We show that the model-checking problem for our logic is decidable in polynomial-time. Then, using this logic, we show how to express interesting properties of cybersecurity games defined on attack graphs.

Details