5 papers
Execution-Time Opacity Logic: A Logic for Ensuring ET-Opacity in Timed Systems
Jean Leneutre, Dylan Marinho, Vadim Malvone +1
Ensuring confidentiality in Cyber-Physical Systems is critical, especially when attackers exploit execution times to infer sensitiveinformation. Traditional opacity models are inad…
A Timed Obstruction Logic for Dynamic Game Models
David Cortes, Jean Leneutre, Vadim Malvone +1
Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. Many of these reactive real-time applica…
Probabilistic Obstruction Temporal Logic: a Probabilistic Logic to Reason about Dynamic Models
Jean Leneutre, Vadim Malvone, James Ortiz
In this paper, we propose a novel formalism called Probabilistic Obstruction Temporal Logic (POTL), which extends Obstruction Logic (OL) by incorporating probabilistic elements. PO…
Capacity ATL
Gabriel Ballot, Vadim Malvone, Jean Leneutre +1
Model checking strategic abilities was successfully developed and applied since the early 2000s to ensure properties in Multi-Agent System. In this paper, we introduce the notion o…
Reasoning about Moving Target Defense in Attack Modeling Formalisms
Gabriel Ballot, Vadim Malvone, Jean Leneutre +1
Since 2009, Moving Target Defense (MTD) has become a new paradigm of defensive mechanism that frequently changes the state of the target system to confuse the attacker. This freque…