Runtime verification (RV) is a lightweight technique for checking system correctness against formal specifications. Traditional RV assumes full system observability, which rarely holds in distributed and component-based systems where monitors only see partial traces. This leads to inconclusive or incorrect verdicts. To address this, recent work has explored monitors that handle imperfect information and reason about visibility. However, these approaches focus on isolated monitors and overlook coordination in distributed settings. We propose a novel framework for runtime verification with rational multi-monitors, where each monitor is a resource-bounded agent with a local specification. Monitors strategically decide what information to share or request, balancing verification goals with communication costs. We formalise this interaction using multi-agent system techniques and synthesise cooperative strategies through model checking. We implement our approach and evaluate it in a case study, showing that rational coordination improves monitoring conclusiveness over existing approaches.

We introduce First-Order Coalition Logic (FOCL), which combines key intuitions behind Coalition Logic (CL) and Strategy Logic (SL). Specifically, FOCL allows for arbitrary quantification over actions of agents. FOCL is interesting for several reasons. First, we show that FOCL is strictly more expressive than existing coalition logics. Second, we provide a sound and complete axiomatisation of FOCL, which, to the best of our knowledge, is the first axiomatisation of any variant of SL in the literature. Finally, while discussing the satisfiability problem for FOCL, we reopen the question of the recursive axiomatisability of SL.

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.

Multi-Agent Systems (MAS) are essential for modelling strategic interactions between multiple agents, often involving partial information. Managing this partial information is crucial for accurate decision-making and strategy optimization. However, partial information combined with perfect recall strategies renders verifying strategic properties undecidable. Intuitionism, a form of partial information which has not yet been explored in the context of MAS, introduces a novel perspective. In this paper, we propose Intuitionistic Alternating Time Temporal Logic (IATL), an extension of ATL that incorporates intuitionistic logic, providing a specialized representation of imperfect information. We define its syntax, semantics, and key structural properties. Additionally, we propose a PTIME-complete algorithm for IATL model checking, supported by benchmarks demonstrating its efficiency.

In logics for strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall strategies. In this work, we show the combination of two techniques to approximate the verification of Alternating-time Temporal Logic (ATL∗ ) under imperfect information and perfect recall, which is known to be undecidable. Given a model M and a formula φ, we propose a verification procedure that generates sub-models of M in which each sub-model M′ satisfies a sub-formula φ′ of φ and the verification of φ′ in M′ is decidable. Then, we use CTL∗ model checking to provide a verification result of φ on M. In case the previous step does not give a final result, we exploit a runtime verification mechanism to provide some intermediate result. We prove that our procedure is sound and in the same complexity class of ATL∗ model checking under perfect information and perfect recall. Moreover, we present a tool that uses our procedure and provide experimental results.

International audience

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.

An attack graph is a succinct representation of all the paths in an open system that allow an attacker to enter a forbidden state (e.g., a resource), besides any attempt of the system to prevent it.Checking system vulnerability amounts to verifying whether such paths exist.In this paper we reason about attack graphs by means of a game-theoretic approach.Precisely, we introduce a suitable game model to represent the interaction between the system and the attacker and an automata-based solution to show the absence of vulnerability.

Abstract In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.