In formal strategic reasoning for Multi-Agent Systems (MAS), agents are typically assumed to (i) employ arbitrarily complex strategies, (ii) execute each move at zero cost, and (iii) operate over fully crisp game structures. These idealized assumptions stand in stark contrast with human decision-making in real-world environments. The natural strategies framework, along with some of its recent variants, partially addresses this gap by restricting strategies to concise rules guarded by regular expressions. Yet, it still overlook both the cost of each action and the uncertainty that often characterizes human perception of facts over the time. In this work, we introduce HumanATLF, a logic that builds upon natural strategies employing both fuzzy semantics and resource‐bound actions: each action carries a real-valued cost drawn from a non‐refillable budget, and atomic conditions and goals have degrees in [0,1]. We give a formal syntax and semantics, and prove that model checking is in P when both the strategy complexity k and resource budget b are fixed, NP-complete if just one strategic operator over Boolean objectives is allowed, and Delta^P_2‐complete when k and b vary. Moreover, we show that recall‐based strategies can be decided in PSPACE. We implement our algorithms in VITAMIN, an open source model-checking tool for MAS and validate them on an adversarial resource-aware drone rescue scenario.

Multi-agent systems often involve multi-level interactions that make strategic reasoning hard to scale. To capture such systems, we introduce hierarchical concurrent game models (HCGMs) that allow embedding of (sub)systems into other systems. We define the semantics of ATL on HCGMs by an unfolding of an HCGM into a standard (flat) concurrent game model. Building on this semantics, we provide a model checking algorithm for ATL interpreted over HCGMs and discuss its complexity.

Trusting software systems, particularly autonomous ones, is challenging. To address this, formal verification techniques can ensure these systems behave as expected. Runtime Verification (RV) is a leading, lightweight method for verifying system behaviour during execution. However, traditional RV assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments where sensors might be faulty. Additionally, traditional RV considers the monitor to be passive, lacking the capability to interpret the system’s information and thus unable to address incomplete data. In this work, we extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally. We outline the necessary engineering steps to update the verification pipeline and demonstrate our implementation in a case study involving robotic systems.

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.

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.

The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them are not always readily avail able. Even when such tools are accessible, they tend to be hard-coded, lacking in compositionality, and challenging to use due to a steep learning curve. In this paper, we introduce a methodology designed for the formal verification of MAS in a modular and versatile manner, along with an initial prototype, that we named VITAMIN. Unlike existing verification methodologies and frameworks for MAS, VITAMIN is constructed for easy extension to accommodate various logics (for specifying the properties to verify) and models (for deter mining on what to verify such properties).

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.

We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a “program epistemic” logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex, including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can “see” only a part of the global space of variables. We verify program-epistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers.

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.

We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are such that it is still decidable to model-check these CGSs against a relevant fragment of ATL. These systems can be thought as a generalization of architectures allowing information forks, that is, cases where strategic abilities lead to certain agents outside a coalition privately sharing information with selected agents inside that coalition. Moreover, in our case, in the initial states of the system, we allow information forks from agents outside a given set \(A\) to agents inside this group \(A\) . For this reason, together with the fact that the communication in our models underpins a specialized form of broadcast, we call our formalism \(A\) -cast systems . To underline, the fragment of ATL for which we show the model-checking problem to be decidable over \(A\) -cast is a large and significant one; it expresses coalitions over agents in any subset of the set \(A\) . Indeed, as we show, our systems and this ATL fragments can encode security problems that are notoriously hard to express faithfully: terrorist-fraud attacks in identity schemes.

International audience

We propose a new approach to the verification of epistemic properties of programmes. First, we introduce the new ``program-epistemic'' logic L_PK, which is strictly richer and more general than similar formalisms appearing in the literature. To solve the verification problem in an efficient way, we introduce a translation from our language L_PK into first-order logic. Then, we show and prove correct a reduction from the model checking problem for program-epistemic formulas to the satisfiability of their first-order translation. Both our logic and our translation can handle richer specification w.r.t. the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (i.e., agents' knowledge before a program is executed as well as after is has been executed). Furthermore, we implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and we use existing SMT-solvers to check satisfaction of L_PK formulas on a benchmark example in the AI/agency field.

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.

International audience

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.

The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results.

Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

International audience

The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic AT L, hence AT L∗ , under perfect recall and imperfect information is known to be undecidable. To tackle this problem, in this paper we investigate a notion of bounded recall under incomplete information. We present a novel three-valued semantics for AT L∗ in this setting and analyse the corresponding model checking problem. We show that the three-valued semantics here introduced is an approximation of the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS, an open-source model checker for AT L and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.

Formal analysis of security is often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the relevant security properties. In real life, this cannot be taken for granted. In particular, security mechanisms that are difficult and costly to use are often ignored by the users, and do not really defend the system against possible attacks. Here, we propose a graded notion of security based on the complexity of the user’s strategic behavior. More precisely, we suggest that the level to which a security property φ is satisfied can be defined in terms of: (a) the complexity of the strategy that the user needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security. We demonstrate how the idea works in a case study based on an electronic voting scenario. To this end, we model the vVote implementation of the Prêt à Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain voter-verifiability, and measure the voter’s effort that they require. We also consider the dual view of graded security, measured by the complexity of the attacker’s strategy to compromise the relevant properties of the election.

The verification of strategic abilities of autonomous agents is a key subject of investigation in the applications of formal methods to the design and certification of multi-agents systems. In this contribution we propose a novel approach to this verification problem. Inspired by recent advances, we introduce a translation from Alternating-time Temporal Logic (ATL) to First-order Logic (FOL). We show that our translation is sound on a fragment of ATL, that we call ATL-live, as it is suitable to express liveness properties in MAS. Further, we show how the universal model checking problem for ATL-live can be reduced to semantic entailment in FOL. Finally, we prove that ATL-live is maximal in the sense that if any other ATL connective is added, non-FOL reasoning techniques would be required. These results are meant to be a first step towards the application of FOL reasoners to model check strategic abilities expressed in ATL.

A major challenge for logics for strategies is represented by their verification in contexts of imperfect information. In this contribution we advance the state of the art by approximating the verification of Alternating-time Temporal Logic (ATL) under imperfect information by using perfect information and a three-valued semantics. In particular, we develop novel automata-theoretic techniques for the linear-time logic LTL, then apply these to finding “failure” states, where the ATL specification to be model checked is undefined. Such failure states can then be fed into a refinement procedure, thus providing a sound, albeit incomplete, verification procedure.

We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accomodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

We investigate the verification of Multi-agent Systems against strategic properties expressed in Alternating-time Temporal Logic under the assumptions of imperfect information and perfect recall. To this end, we develop a three-valued semantics for concurrent game structures upon which we define an abstraction method. We prove that concurrent game structures with imperfect information admit perfect information abstractions that preserve three-valued satisfaction. Further, we present a refinement procedure to deal with cases where the value of a specification is undefined. We illustrate the overall procedure in a variant of the Train Gate Controller scenario under imperfect information and perfect recall.

In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies. Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned.

In game theory, deciding whether a designed player wins a game amounts to check whether he has a winning strategy. However, there are several game settings in which knowing whether he has more than a winning strategy is also important. For example, this is crucial in deciding whether a game admits a unique Nash Equilibrium, or in planning a rescue as this would provide a backup plan. In this paper we study the problem of checking whether, in a two-player reachability game, a designed player has more than a winning strategy. We investigate this question both under perfect and imperfect information about the moves performed by the players. We provide an automata-based solution that results, in the perfect information setting, in a linear-time procedure; in the imperfect information setting, instead, it shows an exponential-time upper bound. In both cases, the results are tight.

We study a class of determined two-player reachability games, played by Player0and Player1under imperfect information. Precisely, we consider the case in which Player0wins the game if Player1cannot prevent him from reaching a target state. We show that the problem of deciding such a game is EXPTIME-COMPLETE.

In game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we introduce Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) with graded quantifiers. SL is a powerful formalism that allows to describe useful game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In GSL, by means of the existential construct 〈〈x ≥ g〉〉φ one can enforce that there exist at least g strategies satisfying φ. Dually, via the universal construct [[x <; g]]φ one can ensure that all but less than g strategies satisfy φ. As different strategies may induce the same outcome, although looking different, they need to be counted as one. While this interpretation is natural, it heavily complicates the definition and thus the reasoning about GSL. In order to accomplish this specific way of counting, we formally introduce a suitable equivalence relation over profiles based on the strategic behavior they induce. To give evidence of GSL usability, we investigate basic questions of one of its vanilla fragment, namely GSL[1G]. In particular, we report on positive results about the determinacy of games and the related model-checking problem, which we show to be PTIME-COMPLETE.