Author name cluster

James Ortiz

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.

3 papers

1 author row

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

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

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