Francesco Belardinelli

AAMAS Conference 2026 Conference Paper

ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems

• Sofia Garcia de Blas Garcia-Alcaide
• Francesco Belardinelli

We present two novel symbolic algorithms for model checking the Alternating-time Temporal Logic ATL∗, over both the infinitetrace and the finite-trace semantics. In particular, for infinite traces we design a novel symbolic reduction to parity games. We implement both methods in the ATL∗AS model checker and evaluate it using synthetic benchmarks as well as a cybersecurity scenario. Our results demonstrate that the symbolic approach significantly outperforms the explicit-state representation and we find that our parity-game-based algorithm offers a more scalable and efficient solution for infinite-trace verification, outperforming previously available tools. Our results also confirm that finite-trace model checking yields substantial performance benefits over infinite-trace verification. As such, we provide a comprehensive toolset for verifying multi-agent systems against specifications in ATL∗.

AAAI Conference 2026 Conference Paper

Behaviour Policy Optimization: Provably Lower Variance Return Estimates for Off-Policy Reinforcement Learning

• Alex W. Goodall
• Edwin Hamel-de le Court
• Francesco Belardinelli

Many reinforcement learning algorithms, particularly those that rely on return estimates for policy improvement, can suffer from poor sample efficiency and training instability due to high-variance return estimates. In this paper we leverage new results from off-policy evaluation; it has recently been shown that well-designed behaviour policies can be used to collect off-policy data for provably lower variance return estimates. This result is surprising as it means collecting data on-policy is not variance optimal. We extend this key insight to the online reinforcement learning setting, where both policy evaluation and improvement are interleaved to learn optimal policies. Off-policy RL has been well studied (e.g., IMPALA), with correct and truncated importance weighted samples for de-biasing and managing variance appropriately. Generally these approaches are concerned with reconciling data collected from multiple workers in parallel, while the policy is updated asynchronously, mismatch between the workers and policy is corrected in a mathematically sound way. Here we consider only one worker - the behaviour policy, which is used to collect data for policy improvement, with provably lower variance return estimates. In our experiments we extend two policy-gradient methods with this regime, demonstrating better sample efficiency and performance over a diverse set of environments.

AAAI Conference 2026 Conference Paper

Expressive Temporal Specifications for Reward Monitoring

• Omar Adalat
• Francesco Belardinelli

Specifying informative and dense reward functions remains a pivotal challenge in Reinforcement Learning, as it directly affects the efficiency of agent training. In this work, we harness the expressive power of quantitative Linear Temporal Logic on finite traces to synthesize reward monitors that generate a dense stream of rewards for runtime-observable state trajectories. By providing nuanced feedback during training, these monitors guide agents toward optimal behaviour and help mitigate the well-known issue of sparse rewards under long-horizon decision making, which arises under the Boolean semantics dominating the current literature. Our framework is algorithm-agnostic and only relies on a state labelling function, and naturally accommodates specifying non-Markovian properties. Empirical results show that our quantitative monitors consistently subsume and, depending on the environment, outperform Boolean monitors in maximizing a quantitative measure of task completion and in reducing convergence time.

AAMAS Conference 2026 Conference Paper

ProSh: Probabilistic Shielding for Model-free Reinforcement Learning

• Edwin Hamel-de le Court
• Gaspard Ohlmann
• Francesco Belardinelli

Safety is a major concern in reinforcement learning (RL): we aim at developing RL systems that not only perform optimally, but are also safe to deploy by providing formal guarantees about their safety. To this end, we introduce Probabilistic Shielding via Risk Augmentation (ProSh), a model-free algorithm for safe reinforcement learning under cost constraints. ProSh augments the Constrained MDP state space with a risk budget and enforces safety by applying a shield to the agent’s policy distribution using a learned cost critic. The shield ensures that all sampled actions remain safe in expectation. We also show that optimality is preserved when the environment is deterministic. Since ProSh is model-free, safety during training depends on the knowledge we have acquired about the environment. We provide a tight upper-bound on the cost in expectation, depending only on the backup-critic accuracy, that is always satisfied during training. Under mild, practically achievable assumptions, ProSh guarantees safety even at training time, as shown in the experiments.

AAMAS Conference 2026 Conference Paper

Safe Reinforcement Learning via Recovery-based Shielding with Gaussian Process Dynamics Models

• Alexander W. Goodall
• Francesco Belardinelli

Reinforcement learning (RL) is a powerful framework for optimal decision-making and control but often lacks provable guarantees for safety-critical applications. In this paper, we introduce a novel recovery-based shielding framework that enables safe RL with a provable safety lower bound for unknown and non-linear continuous dynamicalsystems. The proposed approach integratesa backup policy (shield) with the RL agent, leveraging Gaussian process (GP) based uncertainty quantification to predict potential violations of safety constraints, dynamically recovering to safe trajectories only when necessary. Experience gathered by the ‘shielded’ agent is used to construct the GP models, with policy optimization via internal model-based sampling – enabling unrestricted exploration and sample efficient learning, without compromising safety. Empirically our approach demonstrates strong performance and strict safety-compliance on a suite of continuous control environments. 1

AAMAS Conference 2026 Conference Paper

Synthesis of Safety Specifications for Probabilistic Systems

• Gaspard Ohlmann
• Edwin Hamel-de le Court
• Francesco Belardinelli

Ensuring that agents satisfy safety specifications can be crucial in safety-critical environments. While methods exist for controller synthesis with safe temporal specifications, most existing methods restrict safe temporal specifications to probabilistic-avoidance constraints. Formal methods typically offer more expressive ways to expresssafetyinprobabilisticsystems, suchasProbabilisticComputation Tree Logic (PCTL) formulas. Thus, in this paper, we develop a new approach that supports more general temporal properties expressed in PCTL. Our contribution is twofold. First, we develop a theoretical framework for the Synthesis of safe-PCTL specifications. We show how the reducing global specification satisfaction to local constraints, and define CPCTL, a fragment of safe-PCTL. We demonstrate how the expressiveness of CPCTL makes it a relevant fragment for the Synthesis Problem. Second, we leverage these results and propose a new Value Iteration-based algorithm to solve the synthesis problem for these more general temporal properties, and we prove the soundness and completeness of our method.

AAMAS Conference 2025 Conference Paper

LUNAR: A Runtime Verification Tool for Anomaly Detection in Gas Networks

• Julius Gasson
• Francesco Belardinelli

We introduce LUNAR, a framework to detect and classify network anomalies. The tool is designed to (1) synthesize safety constraints expressed in Signal Temporal Logic (STL) based on network data; (2) detect anomalies in new samples wrt the STL constraints; (3) learn to classify anomaly types based on user labels of prior anomalies.

AAAI Conference 2025 Conference Paper

Probabilistic Shielding for Safe Reinforcement Learning

• Edwin Hamel-de le Court
• Francesco Belardinelli
• Alexander W. Goodall

In real-life scenarios, a Reinforcement Learning (RL) agent aiming to maximize their reward, must often also behave in a safe manner, including at training time. Thus, much attention in recent years has been given to Safe RL, where an agent aims to learn an optimal policy among all policies that satisfy a given safety constraint. However, strict safety guarantees are often provided through approaches based on linear programming, and thus have limited scaling. In this paper we present a new, scalable method, which enjoys strict formal guarantees for Safe RL, in the case where the safety dynamics of the Markov Decision Process (MDP) are known, and safety is defined as an undiscounted probabilistic avoidance property. Our approach is based on state-augmentation of the MDP, and on the design of a shield that restricts the actions available to the agent. We show that our approach provides a strict formal safety guarantee that the agent stays safe at training and test time. Furthermore, we demonstrate that our approach is viable in practice through experimental evaluation.

AAMAS Conference 2024 Conference Paper

Leveraging Approximate Model-based Shielding for Probabilistic Safety Guarantees in Continuous Environments

• Alexander W. Goodall
• Francesco Belardinelli

Shielding is a popular technique for achieving safe reinforcement learning (RL). However, classical shielding approaches come with quite restrictive assumptions making them difficult to deploy in complex environments, particularly those with continuous state or action spaces. In this paper we extend the more versatile approximate model-based shielding (AMBS) framework to the continuous setting. In particular we use Safety Gym as our test-bed, allowing for a more direct comparison of AMBS with popular constrained RL algorithms. We also provide strong probabilistic safety guarantees for the continuous setting. In addition, we propose two novel penalty techniques that directly modify the policy gradient, which empirically provide more stable convergence in our experiments.

NeurIPS Conference 2024 Conference Paper

Measuring Goal-Directedness

• Matt MacDermott
• James Fox
• Francesco Belardinelli
• Tom Everitt

We define maximum entropy goal-directedness (MEG), a formal measure of goal-directedness in causal models and Markov decision processes, and give algorithmsfor computing it. Measuring goal-directedness is important, as it is a criticalelement of many concerns about harm from AI. It is also of philosophical interest, as goal-directedness is a key aspect of agency. MEG is based on an adaptation ofthe maximum causal entropy framework used in inverse reinforcement learning. Itcan measure goal-directedness with respect to a known utility function, a hypothesisclass of utility functions, or a set of random variables. We prove that MEG satisfiesseveral desiderata and demonstrate our algorithms with small-scale experiments.

AAMAS Conference 2024 Conference Paper

On the Stability of Learning in Network Games with Many Players

• Aamal Hussain
• Dan Leonte
• Francesco Belardinelli
• Georgios Piliouras

Multi-agent learning algorithms have been shown to display complex, unstable behaviours in a wide array of games. In fact, previous works indicate that convergent behaviours are less likely to occur as the total number of agents increases. This seemingly prohibits convergence to stable strategies, such as Nash Equilibria, in games with many players. To make progress towards addressing this challenge we study the Q-Learning Dynamics, a classical model for exploration and exploitation in multi-agent learning. In particular, we study the behaviour of Q-Learning on games where interactions between agents are constrained by a network. We determine a number of su�cient conditions, depending on the game and network structure, which guarantee that agent strategies converge to a unique stable strategy, called the Quantal Response Equilibrium (QRE). Crucially, these su�cient conditions are independent of the total number of agents, allowing for provable convergence in arbitrarily large games. Next, we compare the learned QRE to the underlying NE of the game, by showing that any QRE is an n-approximate Nash Equilibrium. We� rst provide tight bounds on n and show how these bounds lead naturally to a centralised scheme for choosing exploration rates, which enables independent learners to learn stable approximate Nash Equilibrium strategies. We validate the method through experiments and demonstrate its e�ectiveness even in the presence of numerous agents and actions. Through these results, we show that independent learning dynamics may converge to approximate Nash Equilibria, even in the presence of many agents.

AAAI Conference 2024 Conference Paper

Stability of Multi-Agent Learning in Competitive Networks: Delaying the Onset of Chaos

• Aamal Hussain
• Francesco Belardinelli

The behaviour of multi agent learning in competitive network games is often studied within the context of zero sum games, in which convergence guarantees may be obtained. However, outside of this class the behaviour of learning is known to display complex behaviours and convergence cannot be always guaranteed. Nonetheless, in order to develop a complete picture of the behaviour of multi agent learning in competitive settings, the zero sum assumption must be lifted. Motivated by this we study the Q Learning dynamics, a popular model of exploration and exploitation in multi agent learning, in competitive network games. We determine how the degree of competition, exploration rate and network connectivity impact the convergence of Q Learning. To study generic competitive games, we parameterise network games in terms of correlations between agent payoffs and study the average behaviour of the Q Learning dynamics across all games drawn from a choice of this parameter. This statistical approach establishes choices of parameters for which Q Learning dynamics converge to a stable fixed point. Differently to previous works, we find that the stability of Q Learning is explicitly dependent only on the network connectivity rather than the total number of agents. Our experiments validate these findings and show that, under certain network structures, the total number of agents can be increased without increasing the likelihood of unstable or chaotic behaviours.

AAMAS Conference 2024 Conference Paper

The Reasons that Agents Act: Intention and Instrumental Goals

• Francis Rhys Ward
• Matt MacDermott
• Francesco Belardinelli
• Francesca Toni
• Tom Everitt

Intention is an important and challenging concept in AI. It is important because it underlies many other concepts we care about, such as agency, manipulation, legal responsibility, and blame. However, ascribing intent to AI systems is contentious, and there is no universally accepted theory of intention applicable to AI agents. We operationalise the intention with which an agent acts, relating to the reasons it chooses its decision. We introduce a formal definition of intention in structural causal influence models, grounded in the philosophy literature on intent and applicable to real-world machine learning systems. Through a number of examples and results, we show that our definition captures the intuitive notion of intent and satisfies desiderata set-out by past work. In addition, we show how our definition relates to past concepts, including actual causality, and the notion of instrumental goals, which is a core idea in the literature on safe AI agents. Finally, we demonstrate how our definition can be used to infer the intentions of reinforcement learning agents and language models from their behaviour.

AAMAS Conference 2024 Conference Paper

Verification of Stochastic Multi-Agent Systems with Forgetful Strategies

• Francesco Belardinelli
• Wojtek Jamroga
• Munyque Mittelmann
• Aniello Murano

Intelligent autonomous agents need to reason about different kinds of uncertainty in a Multi-Agent System (MAS): first, due to the occurrence of randomization and, second, their inability to completely observe the state of the system. In this paper, we investigate the verification of system specifications in probabilistic variants of the logics ATL and ATL∗ under imperfect information (II). The resulting setting combines these two sources of uncertainty and captures the situation in which agents have qualitative uncertainty about the local state as well as quantitative uncertainty about the occurrence of future events. Since the model-checking problem is undecidable when considered in the context of strategies with perfect recall, we focus on memoryless (positional) strategies. As the main result, we show that, in stochastic MAS under II, model-checking Probabilistic ATL is in EXPTIME when agents play probabilistic strategies. Filling the gap in recent work, we also show that model-checking Probabilistic ATL∗ is PSPACE-complete when the proponent coalition is restricted to deterministic strategies.

AIJ Journal 2023 Journal Article

An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information

• Francesco Belardinelli
• Angelo Ferrando
• Vadim Malvone

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. Furthermore, to deal with cases in which the value of a specification is undefined, we develop a novel automata-theoretic technique for the linear-time logic (LTL), then apply it to finding “failure” states. The latter can then be fed into a refinement procedure, thus providing a sound, albeit incomplete, verification method. We illustrate the overall procedure in a variant of the Train Gate Controller scenario and a simple voting protocol under imperfect information and perfect recall. We also present an implementation of our procedure and provide preliminary experimental results.

ECAI Conference 2023 Conference Paper

Approximate Model-Based Shielding for Safe Reinforcement Learning

• Alexander W. Goodall
• Francesco Belardinelli

Reinforcement learning (RL) has shown great potential for solving complex tasks in a variety of domains. However, applying RL to safety-critical systems in the real-world is not easy as many algorithms are sample-inefficient and maximising the standard RL objective comes with no guarantees on worst-case performance. In this paper we propose approximate model-based shielding (AMBS), a principled look-ahead shielding algorithm for verifying the performance of learned RL policies w. r. t. a set of given safety constraints. Our algorithm differs from other shielding approaches in that it does not require prior knowledge of the safety-relevant dynamics of the system. We provide a strong theoretical justification for AMBS and demonstrate superior performance to other safety-aware approaches on a set of Atari games with state-dependent safety-labels.

AAMAS Conference 2023 Conference Paper

Asymptotic Convergence and Performance of Multi-Agent Q-learning Dynamics

• Aamal Abbas Hussain
• Francesco Belardinelli
• Georgios Piliouras

Achieving convergence of multiple learning agents in general 𝑁player games is imperative for the development of safe and reliable machine learning (ML) algorithms and their application to autonomous systems. Yet it is known that, outside the bounds of simple two-player games, convergence cannot be taken for granted. To make progress in resolving this problem, we study the dynamics of smooth Q-Learning, a popular reinforcement learning algorithm which quantifies the tendency for learning agents to explore their state space or exploit their payoffs. We show a sufficient condition on the rate of exploration such that the Q-Learning dynamics Is guaranteed to converge to a unique equilibrium in any game. We connect this result to games for which Q-Learning is known to converge with arbitrary exploration rates, including weighted Potential games and weighted zero sum polymatrix games. Finally, we examine the performance of the Q-Learning dynamic as measured by the Time Averaged Social Welfare, and comparing this with the Social Welfare achieved by the equilibrium. We provide a sufficient condition whereby the Q-Learning dynamic will outperform the equilibrium even if the dynamics do not converge.

AAAI Conference 2023 Conference Paper

Automatically Verifying Expressive Epistemic Properties of Programs

• Francesco Belardinelli
• Ioana Boureanu
• Vadim Malvone
• Fortunat Rajaona

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.

IJCAI Conference 2023 Conference Paper

Beyond Strict Competition: Approximate Convergence of Multi-agent Q-Learning Dynamics

• Aamal Hussain
• Francesco Belardinelli
• Georgios Piliouras

The behaviour of multi-agent learning in competitive settings is often considered under the restrictive assumption of a zero-sum game. Only under this strict requirement is the behaviour of learning well understood; beyond this, learning dynamics can often display non-convergent behaviours which prevent fixed-point analysis. Nonetheless, many relevant competitive games do not satisfy the zero-sum assumption. Motivated by this, we study a smooth variant of Q-Learning, a popular reinforcement learning dynamics which balances the agents' tendency to maximise their payoffs with their propensity to explore the state space. We examine this dynamic in games which are `close' to network zero-sum games and find that Q-Learning converges to a neighbourhood around a unique equilibrium. The size of the neighbourhood is determined by the `distance' to the zero-sum game, as well as the exploration rates of the agents. We complement these results by providing a method whereby, given an arbitrary network game, the `nearest' network zero-sum game can be found efficiently. Importantly, our theoretical guarantees are widely applicable in different game settings, regardless of whether the dynamics ultimately reach an equilibrium, or remain non convergent.

AAMAS Conference 2023 Conference Paper

Defining Deception in Structural Causal Games

• Francis Rhys Ward
• Francesca Toni
• Francesco Belardinelli

Deceptive agents are a challenge for the safety, trustworthiness, and cooperation of AI systems. We focus on the problem that agents might deceive in order to achieve their goals. There are a number of existing definitions of deception in the literature on game theory and symbolic AI, but there is no overarching theory of deception for learning agents in games. We introduce a functional definition of deception in structural causal games, grounded in the philosophical literature. We present several examples to establish that our formal definition captures philosophical desiderata for deception.

NeurIPS Conference 2023 Conference Paper

Honesty Is the Best Policy: Defining and Mitigating AI Deception

• Francis Ward
• Francesca Toni
• Francesco Belardinelli
• Tom Everitt

Deceptive agents are a challenge for the safety, trustworthiness, and cooperation of AI systems. We focus on the problem that agents might deceive in order to achieve their goals (for instance, in our experiments with language models, the goal of being evaluated as truthful). There are a number of existing definitions of deception in the literature on game theory and symbolic AI, but there is no overarching theory of deception for learning agents in games. We introduce a formaldefinition of deception in structural causal games, grounded in the philosophyliterature, and applicable to real-world machine learning systems. Several examples and results illustrate that our formal definition aligns with the philosophical and commonsense meaning of deception. Our main technical result is to provide graphical criteria for deception. We show, experimentally, that these results can be used to mitigate deception in reinforcement learning agents and language models.

IJCAI Conference 2023 Conference Paper

Scalable Verification of Strategy Logic through Three-Valued Abstraction

• Francesco Belardinelli
• Angelo Ferrando
• Wojciech Jamroga
• Vadim Malvone
• Aniello Murano

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.

KR Conference 2023 Conference Paper

Strategic Abilities of Forgetful Agents in Stochastic Environments

• Francesco Belardinelli
• Wojciech Jamroga
• Munyque Mittelmann
• Aniello Murano

In this paper, we investigate the probabilistic variants of the strategy logics ATL and ATL* under imperfect information. Specifically, we present novel decidability and complexity results when both the model transitions and the strategies played by agents are stochastic. That is, the semantics of the logics are based on multi-agent, stochastic transition systems with imperfect information, which combine two sources of uncertainty, namely, the partial observability agents have on the environment, and the likelihood of transitions to occur from a system state. Since the model checking problem is undecidable in general in this setting, we restrict our attention to agents with memoryless (positional) strategies. The resulting setting captures the situation in which agents have qualitative uncertainty of the local state and quantitative uncertainty about the occurrence of future events. We illustrate the usefulness of this setting with meaningful examples.

ICML Conference 2023 Conference Paper

The Impact of Exploration on Convergence and Performance of Multi-Agent Q-Learning Dynamics

• Aamal Abbas Hussain
• Francesco Belardinelli
• Dario Paccagnan

Understanding the impact of exploration on the behaviour of multi-agent learning has, so far, benefited from the restriction to potential, or network zero-sum games in which convergence to an equilibrium can be shown. Outside of these classes, learning dynamics rarely converge and little is known about the effect of exploration in the face of non-convergence. To progress this front, we study the smooth Q- Learning dynamics. We show that, in any network game, exploration by agents results in the convergence of Q-Learning to a neighbourhood of an equilibrium. This holds independently of whether the dynamics reach the equilibrium or display complex behaviours. We show that increasing the exploration rate decreases the size of this neighbourhood and also decreases the ability of all agents to improve their payoffs. Furthermore, in a broad class of games, the payoff performance of Q-Learning dynamics, measured by Social Welfare, decreases when the exploration rate increases. Our experiments show this to be a general phenomenon, namely that exploration leads to improved convergence of Q-Learning, at the cost of payoff performance.

JAIR Journal 2022 Journal Article

Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications

• Francesco Belardinelli
• Alessio Lomuscio
• Vadim Malvone
• Emily Yu

The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic ATL, hence ATL∗, 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 ATL∗ 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 ATL and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.

ICLR Conference 2022 Conference Paper

In a Nutshell, the Human Asked for This: Latent Goals for Following Temporal Specifications

• Borja G. León
• Murray Shanahan
• Francesco Belardinelli

We address the problem of building agents whose goal is to learn to execute out-of distribution (OOD) multi-task instructions expressed in temporal logic (TL) by using deep reinforcement learning (DRL). Recent works provided evidence that the agent's neural architecture is a key feature when DRL agents are learning to solve OOD tasks in TL. Yet, the studies on this topic are still in their infancy. In this work, we propose a new deep learning configuration with inductive biases that lead agents to generate latent representations of their current goal, yielding a stronger generalization performance. We use these latent-goal networks within a neuro-symbolic framework that executes multi-task formally-defined instructions and contrast the performance of the proposed neural networks against employing different state-of-the-art (SOTA) architectures when generalizing to unseen instructions in OOD environments.

EWRL Workshop 2022 Workshop Paper

In a Nutshell, the Human Asked for This: Latent Goals for Following Temporal Specifications

• Borja G. León
• Murray Shanahan
• Francesco Belardinelli

We address the problem of building agents whose goal is to learn to execute out-of distribution (OOD) multi-task instructions expressed in temporal logic (TL) by using deep reinforcement learning (DRL). Recent works provided evidence that the agent’s neural architecture is a key feature when DRL agents are learning to solve OOD tasks in TL. Yet, the studies on this topic are still in their infancy. In this work, we propose a new deep learning configuration with inductive biases that lead agents to generate latent representations of their current goal, yielding a stronger generalization performance. We use these latent-goal networks within a neuro-symbolic framework that executes multi-task formallydefined instructions and contrast the performance of the proposed neural networks against employing different state-ofthe-art (SOTA) architectures when generalizing to unseen instructions in OOD environments.

AAMAS Conference 2022 Conference Paper

On Agent Incentives to Manipulate Human Feedback in Multi-Agent Reward Learning Scenarios

• Francis Rhys Ward
• Francesca Toni
• Francesco Belardinelli

In settings without well-defined goals, methods for reward learning allow reinforcement learning agents to infer goals from human feedback. Existing work has discussed the problem that such agents may manipulate humans, or the reward learning process, in order to gain higher reward. We introduce the neglected problem that, in multi-agent settings, agents may have incentives to manipulate one another’s reward functions in order to change each other’s behavioral policies. We focus on the setting with humans acting alongside assistive (artificial) agents who must learn the reward function by interacting with these humans. We propose a possible solution to manipulation of human feedback in this setting: the Shared Value Prior (SVP). The SVP equips agents with an assumption that the reward functions of all humans are similar. Given this assumption, the actions of any human provide information to an agent about its reward, and so the agent is incentivised to observe these actions rather than to manipulate them. We present an expository example in which the SVP prevents manipulation.

AAMAS Conference 2022 Conference Paper

Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions

• Francesco Belardinelli
• Wojtek Jamroga
• Vadim Malvone
• Munyque Mittelmann
• Aniello Murano
• Laurent Perrussel

In online advertising, search engines sell ad placements for keywords continuously through auctions. This problem can be seen as an infinitely repeated game since the auction is executed whenever a user performs a query with the keyword. As advertisers may frequently change their bids, the game will have a large set of equilibria with potentially complex strategies. In this paper, we propose the use of natural strategies for reasoning in such setting as they are processable by artificial agents with limited memory and/or computational power as well as understandable by human users. To reach this goal, we introduce a quantitative version of Strategy Logic with natural strategies in the setting of imperfect information. In a first step, we show how to model strategies for repeated keyword auctions and take advantage of the model for proving properties evaluating this game. In a second step, we study the logic in relation to the distinguishing power, expressivity, and model-checking complexity for strategies with and without recall.

LAMAS&SR Workshop 2021 Workshop Paper

A Hennessy-Milner Theorem for ATL with Imperfect Information

• Francesco Belardinelli
• Catalin Dima
• Vadim Malvone
• Ferucio Laurentiu Tiplea

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.

AAMAS Conference 2021 Conference Paper

Aggregating Bipolar Opinions

• Stefan Lauren
• Francesco Belardinelli
• Francesca Toni

We introduce a novel method to aggregate Bipolar Argumentation (BA) Frameworks expressing opinions by different parties in debates. We use Bipolar Assumption-based Argumentation (ABA) as an all-encompassing formalism for BA under different semantics. By leveraging on recent results on judgement aggregation in Social Choice Theory, we prove several preservation results, both positive and negative, for relevant properties of Bipolar ABA.

AAMAS Conference 2021 Conference Paper

An Abstraction-based Method to Check Multi-Agent Deep Reinforcement-Learning Behaviors

• Pierre El Mqirmi
• Francesco Belardinelli
• Borja G. León

Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents, and therefore it is generally not adapted to safety-critical applications. To address this issue, we present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints both in training and testing. The approach we propose expresses the constraints to verify in Probabilistic Computation Tree Logic (PCTL) and builds an abstract representation of the system to reduce the complexity of the verification step. This abstract model allows for model checking techniques to identify a set of abstract policies that meet the safety constraints expressed in PCTL. Then, the agents’ behaviours are restricted according to these safe abstract policies. We provide formal guarantees that by using this method, the actions of the agents always meet the safety constraints, and provide a procedure to generate an abstract model automatically. We empirically evaluate and show the effectiveness of our method in a multi-agent environment.

I&C Journal 2021 Journal Article

Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol

• Francesco Belardinelli
• Rodica Condurache
• Cătălin Dima
• Wojciech Jamroga
• Michal Knapik

We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL⁎ for both the objective and subjective variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL⁎ properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model.

IJCAI Conference 2021 Conference Paper

Reasoning About Agents That May Know Other Agents’ Strategies

• Francesco Belardinelli
• Sophia Knight
• Alessio Lomuscio
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study the semantics of knowledge in strategic reasoning. Most existing works either implicitly assume that agents do not know one another’s strategies, or that all strategies are known to all; and some works present inconsistent mixes of both features. We put forward a novel semantics for Strategy Logic with Knowledge that cleanly models whose strategies each agent knows. We study how adopting this semantics impacts agents’ knowledge and strategic ability, as well as the complexity of the model-checking problem.

AIJ Journal 2021 Journal Article

Strategic reasoning with a bounded number of resources: The quest for tractability

• Francesco Belardinelli
• Stéphane Demri

The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2exptime-complete (the same as its proper extension RB±ATL ⁎) and fragments have been identified to lower the complexity. In this work, we consider the variant RB±ATL + that allows for Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL + restricted to a single agent and a single resource is Δ 2 P -complete, hence the same as for the standard branching-time temporal logic CTL +. In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to ptime, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL + can be solved in exptime using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).

KR Conference 2020 Conference Paper

A Three-valued Approach to Strategic Abilities under Imperfect Information

• Francesco Belardinelli
• Vadim Malvone

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.

ECAI Conference 2020 Conference Paper

Extended Markov Games to Learn Multiple Tasks in Multi-Agent Reinforcement Learning

• Borja G. León
• Francesco Belardinelli

The combination of Formal Methods with Reinforcement Learning (RL) has recently attracted interest as a way for single-agent RL to learn multiple-task specifications. In this paper we extend this convergence to multi-agent settings and formally define Extended Markov Games as a general mathematical model that allows multiple RL agents to concurrently learn various non-Markovian specifications. To introduce this new model we provide formal definitions and proofs as well as empirical tests of RL algorithms running on this framework. Specifically, we use our model to train two different logic-based multi-agent RL algorithms to solve diverse settings of non-Markovian co-safe LTL specifications.

AAAI Conference 2020 Conference Paper

Model Checking Temporal Epistemic Logic under Bounded Recall

• Francesco Belardinelli
• Alessio Lomuscio
• Emily Yu

We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporalepistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

ECAI Conference 2020 Conference Paper

Reasoning with a Bounded Number of Resources in ATL+

• Francesco Belardinelli
• Stéphane Demri

The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2EXPTIME-complete (the same as its proper extension RB±ATL*). Several fragments have been identified to lower the complexity. In this work, we consider the variant RB±ATL + which permits Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL + restricted to a single agent and a single resource is Δ p 2 -complete, hence the same as for CTL +. In this case reasoning about resources comes at no extra computational cost. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the problem can be solved in EXPTIME using a Turing reduction to the parity game problem for alternating vector addition systems with states.

AIJ Journal 2020 Journal Article

Verification of multi-agent systems with public actions against strategy logic

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

Model checking multi-agent systems, in which agents are distributed and thus may have different observations of the world, against strategic behaviours is known to be a complex problem in a number of settings. There are traditionally two ways of ameliorating this complexity: imposing a hierarchy on the observations of the agents, or restricting agent actions so that they are observable by all agents. We study systems of the latter kind, since they are more suitable for modelling rational agents. In particular, we define multi-agent systems in which all actions are public and study the model checking problem of such systems against Strategy Logic with equality, a very rich strategic logic that can express relevant concepts such as Nash equilibria, Pareto optimality, and due to the novel addition of equality, also evolutionary stable strategies. The main result is that the corresponding model checking problem is decidable.

ECAI Conference 2020 Conference Paper

Verifying Strategic Abilities in Multi-Agent Systems via First-Order Entailment

• Francesco Belardinelli
• Vadim Malvone

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.

AAMAS Conference 2019 Conference Paper

A Social Choice Theoretic Perspective on Database Aggregation

• Francesco Belardinelli
• Umberto Grandi

AAAI Conference 2019 Conference Paper

An Abstraction-Based Method for Verifying Strategic Properties in Multi-Agent Systems with Imperfect Information

• Francesco Belardinelli
• Alessio Lomuscio
• Vadim Malvone

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.

AAMAS Conference 2019 Conference Paper

Resource-bounded ATL: the Quest for Tractable Fragments

• Francesco Belardinelli
• Stéphane Demri

Resource-aware logics to represent strategic abilities in multi-agent systems are notoriously hard to handle as they combine strategic reasoning with reasoning about resources. In this work, we begin by providing a general overview of the model-checking results currently available for the Resource-bounded Alternating-time Temporal Logic RB±ATL. This allows us to identify several open problems in the literature, as well as to establish relationships with RBTL-like logics, when RB±ATL is restricted to a single agent. Then, we tackle one such open problem that we deem highly significant: we show that model checking RB±ATL is ptime-complete when restricted to a single agent and a single resource. To do so, we make a valuable detour on vector addition systems with states, by proving new complexity results for their state-reachability and nontermination problems, when restricted to a single counter. Thus, reasoning about resources comes at no computational extra cost in the single-resource, single-agent case.

TARK Conference 2019 Conference Paper

Social Choice Methods for Database Aggregation

• Francesco Belardinelli
• Umberto Grandi

Knowledge can be represented compactly in multiple ways, from a set of propositional formulas, to a Kripke model, to a database. In this paper we study the aggregation of information coming from multiple sources, each source submitting a database modelled as a first-order relational structure. In the presence of integrity constraints, we identify classes of aggregators that respect them in the aggregated database, provided these are satisfied in all individual databases. We also characterise languages for first-order queries on which the answer to a query on the aggregated database coincides with the aggregation of the answers to the query obtained on each individual database. This contribution is meant to be a first step on the application of techniques from social choice theory to knowledge representation in databases.

IJCAI Conference 2019 Conference Paper

Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

• Francesco Belardinelli
• Wojciech Jamroga
• Damian Kurpiewski
• Vadim Malvone
• Aniello Murano

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.

AAMAS Conference 2019 Conference Paper

Verifying Strategic Abilities in Multi-agent Systems with Private Data-Sharing

• Francesco Belardinelli
• Ioana Boureanu
• Catalin Dima
• Vadim Malvone

IJCAI Conference 2018 Conference Paper

Alternating-time Temporal Logic on Finite Traces

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We develop a logic-based technique to analyse finite interactions in multi-agent systems. We introduce a semantics for Alternating-time Temporal Logic (for both perfect and imperfect recall) and its branching-time fragments in which paths are finite instead of infinite. We study validities of these logics and present optimal algorithms for their model-checking problems in the perfect recall case.

KR Conference 2018 Conference Paper

Approximating Perfect Recall when Model Checking Strategic Abilities

• Francesco Belardinelli
• Alessio Lomuscio
• Vadim Malvone

We investigate the notion of bounded recall in the context of model checking ATL∗ and ATL specifications in multiagent systems with imperfect information. We present a novel three-valued semantics for ATL∗, respectively ATL, under bounded recall and imperfect information, and study the corresponding model checking problems. Most importantly, we show that the three-valued semantics constitutes an approximation with respect to the traditional two-valued semantics. In the light of this we construct a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall.

KR Conference 2018 Conference Paper

Bisimulations for Logics of Strategies: A Study in Expressiveness and Verification

• Francesco Belardinelli
• Catalin Dima
• Aniello Murano

In this paper we advance the state of the art on the subject of bisimulations for logics of strategies. Bisimulations are a key notion to study the expressive power of a modal language, as well as for applications to system verification. In this contribution we present novel notions of bisimulation for several significant fragments of Strategy Logic (SL), and prove that they preserve the interpretation of formulas in the corresponding fragments. In selected cases we are able to prove that such bisimulations enjoy the Hennessy-Milner property. Finally, we make use of bisimulations to study the expressiveness of the various fragment of SL, including the complexity of their model checking problems.

AAMAS Conference 2018 Conference Paper

Decidable Verification of Multi-agent Systems with Bounded Private Actions

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

AIJ Journal 2018 Journal Article

Second-order propositional modal logic: Expressiveness and completeness results

• Francesco Belardinelli
• Wiebe van der Hoek
• Louwe B. Kuijer

In this paper we advance the state-of-the-art on the application of second-order propositional modal logic (SOPML) in the representation of individual and group knowledge, as well as temporal and spatial reasoning. The main theoretical contributions of the paper can be summarised as follows. Firstly, we introduce the language of (multi-modal) SOPML and interpret it on a variety of different classes of Kripke frames according to the features of the accessibility relations and of the algebraic structure of the quantification domain of propositions. We provide axiomatisations for some of these classes, and show that SOPML is unaxiomatisable on the remaining classes. Secondly, we introduce novel notions of (bi)simulations and prove that they indeed preserve the interpretation of formulas in (the universal fragment of) SOPML. Then, we apply this formal machinery to study the expressiveness of Second-order Propositional Epistemic Logic (SOPEL) in representing higher-order knowledge, i. e. , the knowledge agents have about other agents' knowledge, as well as graph-theoretic notions (e. g. , 3-colorability, Hamiltonian paths, etc.). The final outcome is a rich formalism to represent and reason about relevant concepts in artificial intelligence, while still having a model checking problem that is no more computationally expensive than that of the less expressive quantified boolean logic.

TARK Conference 2017 Conference Paper

A Logic for Global and Local Announcements

• Francesco Belardinelli
• Hans van Ditmarsch
• Wiebe van der Hoek

In this paper we introduce {\em global and local announcement logic} (GLAL), a dynamic epistemic logic with two distinct announcement operators -- $[\phi]^+_A$ and $[\phi]^-_A$ indexed to a subset $A$ of the set $Ag$ of all agents -- for global and local announcements respectively. The boundary case $[\phi]^+_{Ag}$ corresponds to the public announcement of $\phi$, as known from the literature. Unlike standard public announcements, which are {\em model transformers}, the global and local announcements are {\em pointed model transformers}. In particular, the update induced by the announcement may be different in different states of the model. Therefore, the resulting computations are trees of models, rather than the typical sequences. A consequence of our semantics is that modally bisimilar states may be distinguished in our logic. Then, we provide a stronger notion of bisimilarity and we show that it preserves modal equivalence in GLAL. Additionally, we show that GLAL is strictly more expressive than public announcement logic with common knowledge. We prove a wide range of validities for GLAL involving the interaction between dynamics and knowledge, and show that the satisfiability problem for GLAL is decidable. We illustrate the formal machinery by means of detailed epistemic scenarios.

AAMAS Conference 2017 Conference Paper

Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information

• Francesco Belardinelli
• Alessio Lomuscio

AAMAS Conference 2017 Conference Paper

Bisimulations for Verifying Strategic Abilities with an Application to ThreeBallot

• Francesco Belardinelli
• Rodica Condurache
• Catalin Dima
• Wojciech Jamroga
• Andrew V. Jones

IJCAI Conference 2017 Conference Paper

Dynamic Logic for Data-aware Systems: Decidability Results

• Francesco Belardinelli
• Andreas Herzig

We introduce a first-order extension of dynamic logic (FO-DL), suitable to represent and reason about the behaviour of Data-aware Systems (DaS), which are systems whose data content is explicitly exhibited in the system’s description. We illustrate the expressivity of the formal framework by modelling English auctions as DaS, and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for DaS against FO-DL is actually decidable, provided some mild assumptions on the interpretationdomain.

IJCAI Conference 2017 Conference Paper

Parameterised Verification of Data-aware Multi-Agent Systems

• Francesco Belardinelli
• Panagiotis Kouvaros
• Alessio Lomuscio

We introduce parameterised data-aware multi-agent systems, a formalism to reason about the temporal-epistemic properties of arbitrarily large collections of homogeneous agents, each operating on an infinite data domain. We show that their parameterised verification problem is semi-decidable for classes of interest. This is demonstrated by separately addressing the unboundedness of the number of agents and the the data domain. In doing so we reduce the parameterised model checking problem for these systems to that of parameterised verification for interleaved interpreted systems. We illustrate the expressivity of the formal model by modelling English auctions with an unbounded number of bidders on unbouded data and show how the technique here introduced can be used to give formal guarantees on the resulting system behaviour.

TARK Conference 2017 Conference Paper

Relaxing Exclusive Control in Boolean Games

• Francesco Belardinelli
• Umberto Grandi
• Andreas Herzig
• Dominique Longin
• Emiliano Lorini
• Arianna Novaro
• Laurent Perrussel

In the typical framework for boolean games (BG) each player can change the truth value of some propositional atoms, while attempting to make her goal true. In standard BG goals are propositional formulas, whereas in iterated BG goals are formulas of Linear Temporal Logic. Both notions of BG are characterised by the fact that agents have exclusive control over their set of atoms, meaning that no two agents can control the same atom. In the present contribution we drop the exclusivity assumption and explore structures where an atom can be controlled by multiple agents. We introduce Concurrent Game Structures with Shared Propositional Control (CGS-SPC) and show that they ac- count for several classes of repeated games, including iterated boolean games, influence games, and aggregation games. Our main result shows that, as far as verification is concerned, CGS-SPC can be reduced to concurrent game structures with exclusive control. This result provides a polynomial reduction for the model checking problem of specifications in Alternating-time Temporal Logic on CGS-SPC.

IJCAI Conference 2017 Conference Paper

Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We study a class of synchronous, perfect-recall multi-agent systemswith imperfect information and broadcasting (i. e. , fully observableactions). We define an epistemic extension of strategy logic withincomplete information and the assumption of uniform and coherentstrategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is decidable with non-elementarycomplexity. We exemplify the applicability of the framework on arational secret-sharing scenario.

Highlights Conference 2017 Conference Abstract

Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

• Francesco Belardinelli

Abstract available in PDF.

AAMAS Conference 2017 Conference Paper

Verification of Multi-agent Systems with Imperfect Information and Public Actions

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

AAAI Conference 2016 Conference Paper

A Semantical Analysis of Second-Order Propositional Modal Logic

• Francesco Belardinelli
• Wiebe van der Hoek

This paper is aimed as a contribution to the use of formal modal languages in Artificial Intelligence. We introduce a multi-modal version of Second-order Propositional Modal Logic (SOPML), an extension of modal logic with propositional quantification, and illustrate its usefulness as a specification language for knowledge representation as well as temporal and spatial reasoning. Then, we define novel notions of (bi)simulation and prove that these preserve the interpretation of SOPML formulas. Finally, we apply these results to assess the expressive power of SOPML.

JELIA Conference 2016 Conference Paper

A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems

• Francesco Belardinelli
• Alessio Lomuscio

Abstract We put forward an abstraction technique, based on a three-value semantics, for the verification of epistemic properties of agents participating in a multi-agent system. First we introduce a three-value interpretation of epistemic logic, based on a notion of order defined on the information content of the local states of each agent. Then, we use the three-value semantics to introduce an abstraction technique to verify epistemic properties of agents in infinite-state multi-agent systems.

ECAI Conference 2016 Conference Paper

Abstraction-Based Verification of Infinite-State Reactive Modules

• Francesco Belardinelli
• Alessio Lomuscio

We introduce the formalism of infinite-state reactive modules to reason about the strategic behaviour of autonomous agents in a setting where data are explicitly exhibited in the systems description and in the specification language. Technically, we endow reactive modules with an infinite domain of interpretation for individual variables, and introduce FO-ATL, a first-order version of alternating time temporal logic, for the specification of properties of interest. We show that their verification is decidable for classes of data types of interest. This result is proved by defining a first-order version of alternating bisimulations and finite bisimilar abstractions. We illustrate the formal machinery by applying it to English and sealed bid auctions. In particular, we show that strategic properties of agents in auctions, including manipulability and collusion, can be expressed and verified in this framework.

ECAI Conference 2016 Conference Paper

Agent-Based Refinement for Predicate Abstraction of Multi-Agent Systems

• Francesco Belardinelli
• Alessio Lomuscio
• Jakub Michaliszyn

We put forward an agent-based refinement methodology for the verification of infinite-state Multi-Agent Systems by predicate abstraction. We use specifications defined in a three-valued variant of the temporal epistemic logic ATLK. We define "failure states" as candidates for refinement, and provide a sound automatic procedure for their identification. Further, we introduce a methodology based on Craig's interpolants for the refinement of the agent-specific predicates upon which the abstraction is built. We illustrate the refinement technique on an infinite-state auction scenario, and show that specifications of interest, that could not be checked by plain abstraction, can now be verified on the refined models.

IJCAI Conference 2016 Conference Paper

On Logics of Strategic Ability Based on Propositional Control

• Francesco Belardinelli
• Andreas Herzig

Recently logics for strategic ability have gained pre-eminence in the modelisation and analysis of game-theoretic scenarios. In this paper we provide a contribution to the comparison of two popular frameworks: Concurrent Game Structures (CGS) and Coalition Logic of Propositional Control (CLPC). Specifically, we ground the abstract abilities of agents in CGS on Propositional Control, thus obtaining a class of CGS that has the same expressive power as CL-PC. We study the computational properties of this setting. Further, we relax some of the assumptions of CL-PC so as to introduce a wider class of computationally-grounded CGS.

AAMAS Conference 2016 Conference Paper

Second-order Propositional Announcement Logic

• Francesco Belardinelli
• Hans van Ditmarsch
• Wiebe van der Hoek

IJCAI Conference 2015 Conference Paper

Epistemic Quantified Boolean Logic: Expressiveness and Completeness Results

• Francesco Belardinelli
• Wiebe van der Hoek

We introduce epistemic quantified boolean logic (EQBL), an extension of propositional epistemic logic with quantification over propositions. We show that EQBL can express relevant properties about agents’ knowledge in multi-agent contexts, such as “agent a knows as much as agent b”. We analyse the expressiveness of EQBL through a translation into monadic second-order logic, and provide completeness results w. r. t. various classes of Kripke frames. Finally, we prove that model checking EQBL is PSPACE-complete. Thus, the complexity of model checking EQBL is no harder than for (non-modal) quantified boolean logic.

IJCAI Conference 2015 Conference Paper

Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems

• Francesco Belardinelli
• Davide Grossi
• Alessio Lomuscio

We develop a methodology to model and verify open multi-agent systems (OMAS), where agents may join in or leave at run time. Further, we specify properties of interest on OMAS in a variant of firstorder temporal-epistemic logic, whose characterising features include epistemic modalities indexed to individual terms, interpreted on agents appearing at a given state. This formalism notably allows to express group knowledge dynamically. We study the verification problem of these systems and show that, under specific conditions, finite bisimilar abstractions can be obtained.

IJCAI Conference 2015 Conference Paper

Formal Analysis of Dialogues on Infinite Argumentation Frameworks

• Francesco Belardinelli
• Davide Grossi
• Nicolas Maudet

The paper analyses multi-agent strategic dialogues on possibly infinite argumentation frameworks. We develop a formal model for representing such dialogues, and introduce FOA-ATL, a first-order extension of alternating-time logic, for expressing the interplay of strategic and argumentation-theoretic properties. This setting is investigated with respect to the model checking problem, by means of a suitable notion of bisimulation. This notion of bisimulation is also used to shed light on how static properties of argumentation frameworks influence their dynamic behaviour.

ECAI Conference 2014 Conference Paper

Model Checking Auctions as Artifact Systems: Decidability via Finite Abstraction

• Francesco Belardinelli

The formal verification of auctions has recently received considerable attention in the AI and logic community. We tackle this problem by adopting methodologies and techniques originally developed for Artifact Systems, a novel paradigm in Service Oriented Computing. Specifically, we introduce a typed version of artifactcentric multi-agent systems (AC-MAS), a multi-agent setting for Artifact Systems, and consider the model checking problem against typed first-order temporal epistemic specifications. Notably, this formal framework is expressive enough to capture a relevant class of auctions: parallel English (ascending bid) auctions. We prove decidability of the model checking problem for AC-MAS via finite abstraction. In particular, we put forward a methodology to formally verify interesting properties of auctions.

KR Conference 2014 Conference Paper

Satisfiability of Alternating-time Temporal Epistemic Logic through Tableaux

• Francesco Belardinelli

theoretical computer science (D’Agostino et al. 1999). Recently, a stream of papers has appeared on tableau methods for various flavours of temporal logics as well as multiagent epistemic logics (Goranko and Shkatov 2009a; 2009b; 2009c; Ajspur, Goranko, and Shkatov 2013). While we explicitly acknowledge the influence of these works and make use of part of their formal machinery, we substantially extend the object of investigation. Specifically, our work differs from the contributions above in three ways. Firstly, we adopt an agent-based perspective and consider agents as the basic components of our epistemic concurrent game models. This means that the decision procedure returns not just a model satisfying the formula if successful, instead a system of agents is provided. Secondly, we follow the paradigm of Interpreted Systems (Fagin et al. 1995) and consider forms of interaction between the temporal and epistemic dimensions. In particular, we introduce epistemic concurrent game models which are synchronous or have a unique initial state. Thirdly, we analyse two different notions of satisfiability, namely satisfiability in some initial state, as opposed to satisfiability in any state. We maintain that the former notion is typical in the modelling and verification of concurrent systems (Baier and Katoen 2008), while the latter has traditionally been studied in mathematical logic (Blackburn, de Rijke, and Venema 2001). We will see that all these choices do have an impact on tableaux construction. The motivation for the present work comes also from the fact that, besides the theoretical interest of algorithmic decision techniques, tableaux for ATEL can in principle be used to synthesize agent systems capable of enforcing behaviours specified as ATEL formulas. Thus, the investigations carried out hereafter can be seen as a preliminary contribution to bridge the gap between knowledge representation and model synthesis. Related Work. This contribution builds on a series of papers on tableaux for multi-agent modal logics. Specifically, (Goranko and Shkatov 2009a) puts forward incremental tableaux for (non-epistemic) ATL; while in (Ajspur, Goranko, and Shkatov 2013) an epistemic logic with group knowledge is considered. In (Goranko and Shkatov 2009b; 2009c) the linear- and branching-time temporal epistemic logics LTLK and CTLK are given tableau-based decision procedures. However, we extend the object of investigation as detailed above. In (Walther 2005) tableaux for ATEL are In this paper we present a tableau-based method to decide the satisfiability of formulas in ATEL, an extension of the alternating-time temporal logic ATL including epistemic modalities for individual knowledge. Specifically, we analyse satisfiability of ATEL formulas under a number of conditions. We evaluate the assumptions of synchronicity and of a unique initial state, which have been proposed in the context of Interpreted Systems. Also, we consider satisfiability at an initial state as opposed to any state in the system. We introduce a tableau-based decision procedure for each of these combinations. Moreover, we adopt an agent-based approach to satisfiability, namely, the decision procedure returns a set of agents inducing a concurrent game structure that satisfies the relevant specification.

IJCAI Conference 2013 Conference Paper

Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems

• Francesco Belardinelli
• Alessio Lomuscio

Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, nonuniform artifact-centric systems is undecidable. We provide a partial model checking procedure for artifact-centric systems against the universal fragment of a first-order version of the logic CTL. We obtain this result by introducing a counterpart semantics and developing an abstraction methodology operating on these structures. This enables us to generate finite abstractions of infinite artifactcentric systems, hence perform verification on abstract models.

Highlights Conference 2013 Conference Abstract

Model checking Temporal-Epistemic Logic using alternating tree automata

• Francesco Belardinelli
• Andrew Vaughan Jones
• Alessio Lomuscio

We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal epistemic logic CTLK. We show that model check- ing a memory-less interpreted system against a CTLK prop- erty can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.

KR Conference 2012 Conference Paper

An Abstraction Technique for the Verification of Artifact-Centric Systems

• Francesco Belardinelli
• Alessio Lomuscio
• Fabio Patrizi

on which services operate. This emphasis on data makes the automata-based formalisms commonly used to model services generally insufficient: one really requires to account for the evolution of the first-order schemas representing the underlying databases. While this makes the resulting verification problem for artifact systems undecidable, partial solutions have been put forward (Deutsch et al. 2009; Belardinelli, Lomuscio, and Patrizi 2011b; 2011a). These techniques enable the verification of basic temporal properties of the artifact system when analysed under a number of conditions. While these results are valuable, they concern the verification of properties of the artifact system per se and do not address the need of modelling and verifying the actions and information properties of the services acting on or through the artifact system. But if artifact systems are to be deployed in a range of information services as their proponents recommend, it is paramount we can model what actions specific participants are allowed and not allowed to make, what knowledge they can and cannot derive in a system run, what system state they can achieve in coordination with their peers, etc. In other words, we need to verify the epistemic properties of a multi-agent system in which artifacts are present, and not just the evolution of the artifacts themselves. In this paper we set about to explore the verification problem for artifact-centric multi-agent systems, i. e., systems of agents interacting through artifact systems, by means of a knowledge-based perspective. We operate in a first-order setting with knowledge and branching time (FO-CTLK). We first remark that the general problem is undecidable and then proceed to give abstraction results that enable us, in a large class of cases of practical interest, to be able to analyse the model checking of finite approximations rather than the plain infinite model with unbounded database schemas. We stress the fact that all results are obtained for the full firstorder temporal epistemic logic FO-CTLK with identity. So, we assume no restriction on the specification language. The rest of the paper is as follows. In Section 2 we identify the problem, give a general semantics for artifact-centric multi-agent systems (AC-MAS), as well as comment on the undecidability of the model checking problem in the general case. In Section 3 we explore abstraction results that enable us to translate the problem to the model checking of finite We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporalepistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is decidable. We give an upper bound on the complexity of the model checking problem.

IJCAI Conference 2011 Conference Paper

A Computationally-Grounded Semantics for Artifact-Centric Systems and Abstraction Results

• Francesco Belardinelli
• Alessio Lomuscio
• Fabio Patrizi

We present a formal investigation of artifact-based systems, a relatively novel framework in service oriented computing, aimed at laying the foundations for verifying these systems through model checking. We present an infinite-state, computationally grounded semantics for these systems that allows us to reason about temporal-epistemic specifications. We present abstraction techniques for the semantics that guarantee transfer of satisfaction from the abstract system to the concrete one.

KR Conference 2010 Conference Paper

The Interaction of Time and Knowledge in a First-order Logic for Multi-Agent Systems

• Francesco Belardinelli
• Alessio Lomuscio

We investigate a class of first-order temporal epistemic logics for the specification of multi-agent systems. We consider well-known properties of multi-agent systems including perfect recall, synchronicity, no learning, unique initial state, and define natural correspondences between these and quantified interpreted systems. Our findings identify several monodic fragments of first-order temporal epistemic logic that we prove to be both sound and complete with respect to the corresponding classes of quantified interpreted systems. The results show that interaction axioms for propositional temporal epistemic logic can be lifted to the monodic fragment.

KR Conference 2008 Conference Paper

A Complete First-Order Logic of Knowledge and Time

• Francesco Belardinelli
• Alessio Lomuscio

We introduce and investigate quantified interpreted systems, a semantics to reason about knowledge and time in a firstorder setting. We provide an axiomatisation, which we show to be sound and complete. We utilise the formalism to study message passing systems (Lamport 1978; Fagin et al 1995) in a first-order setting, and compare the results obtained to those available for the propositional case.