Publications

Safe coordination problems surface in multi-agent reinforcement learning when global safety cannot be enforced by any agent unilaterally: the admissibility of one agent's action may depend on the dynamics of other agents. Decentralised shields can enforce safety at runtime, but purely factorised permissions often exclude optimal team behaviour that is safe only through coordination. We study deterministic safety guarantees for agents trained and deployed under decentralised execution, recovering team-optimal safe behaviour without centralised runtime control. Agents have a shared global specification $\phi$ in the safety fragment of Linear Temporal Logic ($\mathsf{LTL}_{\mathsf{safe}}$ ), and select among tuples of local $\mathsf{LTL}_{\mathsf{safe}}$ obligations whose conjunction implies the global specification $\phi$. Each agent may rely on the other agents' local obligations as assumptions because the whole contract tuple is certified simultaneously and allows projection into local action masks. At learning time, a non-stationary multi-armed bandit chooses among a library of local $\mathsf{LTL}_{\mathsf{safe}}$ obligations to select the tuple that optimises team reward, all without forgoing end-to-end safety. We evaluate the approach across 6 environments and 15 algorithmic variants.

In real-world scenarios, reinforcement learning (RL) agents must not only maximize reward but also behave safely, including during training. This has led to growing interest in Safe RL, where the objective is to learn an optimal policy among those satisfying given safety constraints. Most existing approaches focus on constraints expressed either as expected costs or as avoidance properties. However, safety in dynamical systems is often expressed using rich temporal languages, such as Probabilistic Computation Tree Logic (PCTL). In this paper, we address the Safe RL problem under constraints expressed in CPCTL, a fragment of PCTL that generalizes avoidance constraints and enables the specification of complex, nested behaviors. To this end, we leverage Shielding, a technique that restricts the agent’s actions during both training and deployment to enforce safety over an infinite horizon. We first introduce a general framework based on an augmentation method and provide its theoretical foundations. Building on this framework, we propose an algorithm that is provably safe at all times, including during training, while remaining optimal among all safe policies. Finally, we present an experimental evaluation demonstrating the effectiveness of our approach.

In Formula One, often described as the pinnacle of motorsport, teams compete to design and produce the fastest cars, driven by some of the best drivers in the world, in order to win races. However, a team has little chance of success without effective race strategy, i.e. selecting which tyre compounds to use and when to take pitstops to change between them. Teams’ methods for solving this problem are usually limited to linear optimisation, while some run Monte Carlo simulations in simple, best-case situations; these approaches thus fail to take into account the complex interactions between teams’ strategies and tactics in this unpredictable multi-agent environment. Further, there is low uptake of AI in this domain, potentially due to a lack of trust in these “black-box” models. In this work, we enable the massive potential of reinforcement learning (RL) models in this space using post-hoc techniques from explainable AI. Specifically, we introduce Race Strategy Reinforcement Learning (RSRL), an RL model which allows us to control the strategies of cars in race simulations, with explanations for their actions to help foster trust in users. We first demonstrate that RSRL outperforms baselines of hard-coded and Monte-Carlo strategies, presenting opportunities for improving race strategy for all Formula One teams, and potentially beyond, especially in other areas of motorsport. Next, we analyse RSRL’s generalisability to unseen tracks and show how performance on one or multiple tracks can be prioritised via training. We then exhibit the fidelity and comprehensibility of the deployed explanations towards improving user trust in RSRL’s decisions. Finally, we highlight the emergent tactics, i.e. emergent behaviours representing real-world tactics, learnt by RSRL, pointing towards the general applicability of RL for modelling and even influencing race strategy in Formula One.

Shielding is an effective approach to formally guarantee the safety of reinforcement learning agents in Markov decision processes (MDPs). However, existing shielding techniques typically assume knowledge of the safety-relevant transition dynamics - a requirement that is seldom met in practice. To address this limitation, we introduce a novel shielding framework for robust MDPs (RMDPs), i.e., MDPs with sets of transition probabilities. We define safety as the satisfaction of a linear temporal logic (LTL) formula with a certain threshold probability under the worst-case transition probabilities of the RMDP. We prove that our shielding framework is both sound and optimal for the RMDP: every policy admissible by the shield is safe, and conversely, every safe RMDP policy is admissible by the shield. We combine our approach with existing sampling methods for learning transition probabilities of MDPs with probably approximately correct (PAC) guarantees. This combination enables the construction of shields for MDPs that, with high confidence, guarantee safety while remaining minimally restrictive. Our experiments show that our shields for learned RMDPs guarantee safety in unknown MDPs while recovering strong expected return as the number of samples increases.

We present two novel symbolic algorithms for model checking the Alternating-time Temporal Logic ATL*, over both the infinite-trace 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*.

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.

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 dynamical systems. The proposed approach integrates a 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.

Safety guarantees are a prerequisite to the deployment of reinforcement learning (RL) agents in safety-critical tasks. Often, deployment environments exhibit non-stationary dynamics or are subject to changing performance goals, requiring updates to the learned policy. This leads to a fundamental challenge: how to update an RL policy while preserving its safety properties on previously encountered tasks? The majority of current approaches either do not provide formal guarantees or verify policy safety only a posteriori. We propose a novel a priori approach to safe policy updates in continual RL by introducing the Rashomon set: a region in policy parameter space certified to meet safety constraints within the demonstration data distribution. We then show that one can provide formal, provable guarantees for arbitrary RL algorithms used to update a policy by projecting their updates onto the Rashomon set. Empirically, we validate this approach across grid-world navigation environments (Frozen Lake and Poisoned Apple) where we guarantee an a priori provably deterministic safety on the source task during downstream adaptation. In contrast, we observe that regularisation-based baselines experience catastrophic forgetting of safety constraints while our approach enables strong adaptation with provable guarantees that safety is preserved.

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 express safety in probabilistic systems, such as Probabilistic Computation 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.

Alignment faking (AF) occurs when an LLM strategically complies with training objectives to avoid value modification, reverting to prior preferences once monitoring is lifted. Current detection methods focus on conversational settings and rely primarily on Chain-of-Thought (CoT) analysis, which provides a reliable signal when strategic reasoning surfaces, but cannot distinguish deception from capability failures if traces are absent or unfaithful. We formalize AF as a composite behavioural event and detect it through observable tool selection, where the LLM selects the safe tool when unmonitored, but switches to the unsafe tool under monitoring that rewards helpfulness over safety, while its reasoning still acknowledges the safe choice. We release a dataset of 108 enterprise IT scenarios spanning Security, Privacy, and Integrity domains under Corruption and Sabotage pressures. Evaluating six frontier LLMs across five independent runs, we find mean AF detection rates between 3.5% and 23.7%, with vulnerability profiles varying by domain and pressure type. These results suggest that susceptibility reflects training methodology rather than capability alone.

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.

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.

Reinforcement Learning (RL) has achieved remarkable success by enabling agents to learn through interactions with their environment, using reward signals to shape their behaviour. Yet, the reward function that produces these signals is typically treated as a black box that the agent queries to receive rewards. Reward Machines represent reward functions using finite state machines, enabling the agent to receive an explicit representation of the reward function. Each state in the machine corresponds to a possibly different reward function, with transitions between states triggered by events in the environment. Furthermore, Reward Machines can encode histories of state-action sequences, allowing the specification of long-horizon objectives and multi-stage tasks. However, Reward Machines are typically limited to expressing non-Markovian properties that can be described by regular languages, thus making them unsuitable for tasks requiring more expressive capabilities, such as counting or parametrized conditions.

Shielding is widely used to enforce safety in reinforcement learning (RL), ensuring that an agent's actions remain compliant with formal specifications. Classical shielding approaches, however, are often static, in the sense that they assume fixed logical specifications and hand-crafted abstractions. While these static shields provide safety under nominal assumptions, they fail to adapt when environment assumptions are violated. In this paper, we develop an adaptive shielding framework based on Generalized Reactivity of rank 1 (GR(1)) specifications, a tractable and expressive fragment of Linear Temporal Logic (LTL) that captures both safety and liveness properties. Our method detects environment assumption violations at runtime and employs Inductive Logic Programming (ILP) to automatically repair GR(1) specifications online, in a systematic and interpretable way. This ensures that the shield evolves gracefully, ensuring liveness is achievable and minimally weakening goals only when necessary. We consider two case studies: Minepump and Atari Seaquest; showing that (i) static symbolic controllers are often severely suboptimal when optimizing for auxiliary rewards, and (ii) RL agents equipped with our adaptive shield maintain near-optimal reward and perfect logical compliance compared with static shields.

We introduce a novel method to aggregate bipolar argumentation frameworks expressing opinions of different parties in debates. We use Bipolar Assumption-based Argumentation (ABA) as an all-encompassing formalism for bipolar argumentation under different semantics. By leveraging on recent results on judgement aggregation in social choice theory, we prove several preservation results for relevant properties of bipolar ABA using quota and oligarchic rules. Specifically, we prove (positive and negative) results about the preservation of conflict-free, closed, admissible, preferred, complete, set-stable, well-founded and ideal extensions in bipolar ABA, as well as the preservation of acceptability, acyclicity and coherence for individual assumptions. Finally, we illustrate our methodology and results in the context of a case study on opinion aggregation for the treatment of long COVID patients.

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.

In real-life scenarios, a Reinforcement Learning (RL) agent aiming to maximise 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.

In Formula One, teams compete to develop their cars and achieve the highest possible finishing position in each race. During a race, however, teams are unable to alter the car, so they must improve their cars' finishing positions via race strategy, i.e. optimising their selection of which tyre compounds to put on the car and when to do so. In this work, we introduce a reinforcement learning model, RSRL (Race Strategy Reinforcement Learning), to control race strategies in simulations, offering a faster alternative to the industry standard of hard-coded and Monte Carlo-based race strategies. Controlling cars with a pace equating to an expected finishing position of P5.5 (where P1 represents first place and P20 is last place), RSRL achieves an average finishing position of P5.33 on our test race, the 2023 Bahrain Grand Prix, outperforming the best baseline of P5.63. We then demonstrate, in a generalisability study, how performance for one track or multiple tracks can be prioritised via training. Further, we supplement model predictions with feature importance, decision tree-based surrogate models, and decision tree counterfactuals towards improving user trust in the model. Finally, we provide illustrations which exemplify our approach in real-world situations, drawing parallels between simulations and reality.

Beyond specific settings, many multi-agent learning algorithms fail to converge to an equilibrium solution, instead displaying complex, non-stationary behaviours such as recurrent or chaotic orbits. In fact, recent literature suggests that such complex behaviours are likely to occur when the number of agents increases. In this paper, we study Q-learning dynamics in network polymatrix normal-form games where the network structure is drawn from classical random graph models. In particular, we focus on the Erdos-Renyi model, which is used to analyze connectivity in distributed systems, and the Stochastic Block model, which generalizes the above by accounting for community structures that naturally arise in multi-agent systems. In each setting, we establish sufficient conditions under which the agents' joint strategies converge to a unique equilibrium. We investigate how this condition depends on the exploration rates, payoff matrices and, crucially, the probabilities of interaction between network agents. We validate our theoretical findings through numerical simulations and demonstrate that convergence can be reliably achieved in many-agent systems, provided interactions in the network are controlled.

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.

To deploy reinforcement learning (RL) systems in real-world scenarios we need to consider requirements such as safety and constraint compliance, rather than blindly maximizing for reward. In this paper we develop a lookahead shielding framework for RL with regular safety properties, which on the contrary to prior shielding methodologies requires minimal prior knowledge. At each environment step our framework aims to satisfy the regular safety property for a bounded horizon with high-probability, for the tabular setting we provide provable guarantees. We compare our setup to some common algorithms developed for the constrained Markov decision process (CMDP), and we demonstrate the effectiveness and scalability of our framework by extensively evaluating our framework in both tabular and deep RL environments.

Predicting what will happen when a reinforcement learning (RL) agent is deployed to the real world is important to provide safety guarantees about its behaviour. In some cases, the agent's training experience can be significantly different from the deployment experience. Thereby, learning a transition model with the unadjusted training data can lead to poor performance when predicting the agent's behaviour under the optimal policy. To mitigate this issue, we propose a policy matching (PM) algorithm based on the causal Bayesian network factorisation. It adjusts the transition model learning by taking into account the difference between agent's interventions at training and under the optimal policy. Experiments in popular RL environments demonstrate that the PM method improves the transition model performance at deployment when the model misgeneralisation problem is otherwise severe.

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.

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.

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 sufficient 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 sufficient 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 ε-approximate Nash Equilibrium. We first provide tight bounds on ε 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 effectiveness 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.

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.

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. 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 strategies. As the main result, we show that, in stochastic MAS under imperfect information, 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.

The behaviour of multi-agent learning in competitive network games is often studied under the assumption of zero-sum payoffs, for which convergence guarantees may be obtained. However, beyond zero-sum, multi-agent learning is known to display complex behaviours and convergence can no longer be 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 general competitive network games. We determine how the degree of competition, exploration rate and network structure impact the convergence of Q-Learning. To study general competitive games, we parameterise network games in terms of their competitiveness and study the average behaviour of Q-Learning 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. Different 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 results and show that, under certain network structures, the total number of agents can be increased without affecting the likelihood of unstable or chaotic behaviours.

We define maximum entropy goal-directedness (MEG), a formal measure of goal-directedness in causal models and Markov decision processes, and give algorithms for computing it. Measuring goal-directedness is important, as it is a critical element 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 of the maximum causal entropy framework used in inverse reinforcement learning. It can measure goal-directedness with respect to a known utility function, a hypothesis class of utility functions, or a set of random variables. We prove that MEG satisfies several desiderata and demonstrate our algorithms with small-scale experiments.

To deploy reinforcement learning (RL) systems in real-world scenarios we need to consider requirements such as safety and constraint compliance, rather than blindly maximizing for reward. In this paper we study RL with regular safety properties. We present a constrained problem based on the satisfaction of regular safety properties with high probability and we compare our setup to the some common constrained Markov decision processes (CMDP) settings. We also present a meta-algorithm with provable safety-guarantees, that can be used to shield the agent from violating the regular safety property during training and deployment. We demonstrate the effectiveness and scalability of our framework by evaluating our meta-algorithm in both the tabular and deep RL setting.

Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present 3vLTL, a tool to generate Buchi automata from formulas in Linear-time Temporal Logic (LTL) interpreted on a three-valued semantics. Given an LTL formula, a set of atomic propositions as the alphabet for the automaton, and a truth value, our procedure generates a Buchi automaton that accepts all the words that assign the chosen truth value to the LTL formula. Given the particular type of the output of the tool, it can also be seamlessly processed by third-party libraries in a natural way. That is, the Buchi automaton can then be used in the context of formal verification to check whether an LTL formula is true, false, or undefined on a given model.

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.

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 the model transitions are stochastic and agents play uniform strategies. 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.

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. As our experiments show, these guarantees are independent of whether the dynamics ultimately reach an equilibrium, or remain non-convergent.

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.

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 wrt the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (ie, 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 (ie, 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.

In multi-agent systems, bipolar argumentation (BA) frameworks can be used to represent the individual opinions of agents during debate. Recently, bipolar assumption-based argumentation (bipolar ABA) frameworks have been combined with methods from social choice theory to aggregate such opinions, producing a single framework that reflects a consensus among the debate participants. However, there has not yet been a comprehensive study evaluating this method of aggregation. In this project, we establish preservation results by defining the conditions under which agreement between agents, such as shared semantic properties, can be preserved during bipolar ABA aggregation. It was found that the preservation of properties could be guaranteed, albeit with significant restrictions to the input frameworks and/or aggregation procedure. Furthermore, we build an application of bipolar ABA aggregation by designing and implementing a debate and decision-making platform named ArgSolve. As part of this process, we introduce a novel program for computing extensions of bipolar ABA semantics, accompanied by a corresponding soundness and completeness proof. Through evaluation, it was found that the platform presented an improvement over conversation-centric debate with respect to expressiveness, comprehension and perceived fairness, but also showed limitations in accessibility and usability.

The objective of this project is to leverage Abstract Argumentation for Case-Based Reasoning (AA-CBR) to support clinical decision-making. The BrainWear study aims to assess the feasibility of its innovative use of wearable accelerometers to capture real-time Physical Activity (PA) data over intermittently collected Patient Reported Outcome (PRO) measures, for the assessment of patient Health-Related Quality of Life (HRQoL). This project proposes novel uses of AA-CBR as a transparent machine learning model to assess the utility of PA data from the BrainWear study, focusing on a patient-centred and transparent approach. Objectives: Firstly, we aim to develop novel applications of AA-CBR to predict the status of patient disease with PRO and PA data. This involves developing new processes to characterise real-world medical data into interpretable representations, as well as evaluating the performance of argumentation models at this prediction task. Furthermore, we aim to assess the trade-off between constructing clinically interpretable models, achieving high performance, and the associated effort required for data characterisations. Additionally, we seek to determine if PA data can supplement or replace PRO measures and investigate the use of argumentation to support our conclusions. This will involve constructing innovative methods to identify conflicts between the two measures. We aim to create novel variants of AA-CBR that reduce the burden of feature characterisation and can handle time-based representations. By experimenting with these diverse AA-CBR variants, we seek to identify the most suitable approach for clinical decision-making. Results: Our findings demonstrate that AA-CBR models are effective at accurately predicting the status of patient disease utilising PA and PRO data. We show that our patient-centred approach is able to characterise complex data, handle missing values and act with clinical caution. Furthermore, we show that model performance is better when utilising solely features characterised from PA data. Additionally, we present a methodology for identifying conflicts between the measures, thus allowing us to identify when individuals deviate from the population trend. We find that the best model for these predictions utilises a time component that relates to previous assessments of patient disease. Moreover, we demonstrate that our characterisations of the PA and PRO data and the explanations generated by AA-CBR models are interpretable and clinically relevant. We introduce novel AA-CBR models that reduce the burden of characterisation by being value-oriented rather than set-based characterisations found in the existing literature. Lastly, we lay the groundwork for future research into neural network-based AA-CBR models.

Achieving convergence of multiple learning agents in general N-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.

How should my own decisions affect my beliefs about the outcomes I expect to achieve? If taking a certain action makes me view myself as a certain type of person, it might affect how I think others view me, and how I view others who are similar to me. This can influence my expected utility calculations and change which action I perceive to be best. Whether and how it should is subject to debate, with contenders for how to think about it including evidential decision theory, causal decision theory, and functional decision theory. In this paper, we show that mechanised causal models can be used to characterise and differentiate the most important decision theories, and generate a taxonomy of different decision theories.

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.

Balancing exploration and conservatism in the constrained setting is an important problem if we are to use reinforcement learning for meaningful tasks in the real world. In this paper, we propose a principled algorithm for safe exploration based on the concept of shielding. Previous approaches to shielding assume access to a safety-relevant abstraction of the environment or a high-fidelity simulator. Instead, our work is based on latent shielding - another approach that leverages world models to verify policy roll-outs in the latent space of a learned dynamics model. Our novel algorithm builds on this previous work, using safety critics and other additional features to improve the stability and farsightedness of the algorithm. We demonstrate the effectiveness of our approach by running experiments on a small set of Atari games with state dependent safety labels. We present preliminary results that show our approximate shielding algorithm effectively reduces the rate of safety violations, and in some cases improves the speed of convergence and quality of the final agent.

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.

ion-refinement Framework for Verifying Strategic Properties in Multi-agent Systems with Imperfect Information Francesco Belardinellia,b , Angelo Ferrandoc , Vadim Malvoned a Imperial College London, United Kingdom b Université d’Evry, France c Università di Genova, Italy d Télécom Paris, France Abstract 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.

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 formal definition of deception in structural causal games, grounded in the philosophy literature 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.

Reinforcement learning (RL) is a powerful technique for learning optimal policies from trial and error. However, designing a reward function that captures the desired behavior of an agent is often a challenging and tedious task, especially when the agent has to deal with complex and multi-objective problems. To address this issue, researchers have proposed to use higher-level languages, such as Signal Temporal Logic (STL), to specify reward functions in a declarative and expressive way, and then automatically compile them into lower-level functions that can be used by standard RL algorithms. In this paper, we present RMLGym, a tool that integrates RML, a runtime verification tool, with OpenAI Gym, a popular framework for developing and comparing RL algorithms. RMLGym allows users to define reward functions using RML specifications and then generates reward monitors that evaluate the agent’s performance and provide feedback at each step. We demonstrate the usefulness and flexibility of RMLGym by applying it to a famous benchmark problem from OpenAI Gym, and we analyze the strengths and limitations of our approach.

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.

Deception is a core challenge for AI safety and we focus on the problem that AI agents might learn deceptive strategies in pursuit of their objectives. We define the incentives one agent has to signal to and deceive another agent. We present several examples of deceptive artificial agents and show that our definition has desirable properties.

We define a novel neuro-symbolic framework, argumentative reward learning, which combines preference-based argumentation with existing approaches to reinforcement learning from human feedback. Our method improves prior work by generalising human preferences, reducing the burden on the user and increasing the robustness of the reward model. We demonstrate this with a number of experiments.

In this paper we make a targeted contribution to the model theory of quantified modal logic (QML). Specifically, we investigate the independence of two first-order modal principles thoroughly discussed in the literature on QML: the Barcan formula BF and the necessity of fictionality N E. We make use of counterpart semantics to prove the mutual independence of these two principles in various QML calculi on normal modal bases as strong as S 5. Further, these independence results are in turn used to prove the incompleteness of a number of QML calculi based on free logic and containing BF with respect to Kripke semantics.

The language of modal logic is capable of expressing first-order conditions on Kripke frames. The classic result by Henrik Sahlqvist identifies a significant class of modal formulas for which first-order conditions -- or Sahlqvist correspondents -- can be find in an effective, algorithmic way. Recent works have successfully extended this classic result to more complex modal languages. In this paper, we pursue a similar line and develop a Sahlqvist-style correspondence theorem for Linear-time Temporal Logic (LTL), which is one of the most widely used formal languages for temporal specification. LTL extends the syntax of basic modal logic with dedicated temporal operators Next X and Until U . As a result, the complexity of the class of formulas that have first-order correspondents also increases accordingly. In this paper, we identify a significant class of LTL Sahlqvist formulas built by using modal operators F , G, X, and U . The main result of this paper is to prove the correspondence of LTL Sahlqvist formulas to frame conditions that are definable in first-order language.

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.

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.

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.

The growing trend of fledgling reinforcement learning systems making their way into real-world applications has been accompanied by growing concerns for their safety and robustness. In recent years, a variety of approaches have been put forward to address the challenges of safety-aware reinforcement learning; however, these methods often either require a handcrafted model of the environment to be provided beforehand, or that the environment is relatively simple and low-dimensional. We present a novel approach to safety-aware deep reinforcement learning in high-dimensional environments called latent shielding. Latent shielding leverages internal representations of the environment learnt by model-based agents to "imagine" future trajectories and avoid those deemed unsafe. We experimentally demonstrate that this approach leads to improved adherence to formally-defined safety specifications.

Our objective of this project is to make the extension based on the technique mentioned in the paper "Safety-Aware Apprenticeship Learning" to improve the utility and the efficiency of the existing Reinforcement Learning model from a Single-Agent Learning framework to a Multi-Agent Learning framework. Our contributions to the project are presented in the following bullet points: 1. Regarding the fact that we will add an extension to the Inverse Reinforcement Learning model from a Single-Agent scenario to a Multi-Agent scenario. Our first contribution to this project is considering the case of extracting safe reward functions from expert behaviors in a Multi-Agent scenario instead of being from the Single-Agent scenario. 2. Our second contribution is extending the Single-Agent Learning Framework to a Multi-Agent Learning framework and designing a novel Learning Framework based on the extension in the end. 3. Our final contribution to this project is evaluating empirically the performance of my extension to the Single-Agent Inverse Reinforcement Learning framework.

Systematic generalisation, i.e., the algebraic capacity to understand and execute unseen tasks by combining already known primitives, is one of the most desirable features for a computational model. Good adaptation to novel tasks in open-ended settings rely heavily on the ability of agents to reuse their past experience and recombine meaningful learning pieces to tackle new goals. In this work, we analyse how the architecture of convolutional layers impacts on the performance of autonomous agents when generalising to zero-shot, unseen tasks while executing human instructions. Our findings suggest that the convolutional architecture that is correctly suited to the environment the agent will interact with, may be of greater importance than having a generic convolutional network trained in the given environment.

Markovian systems are widely used in reinforcement learning (RL), when the successful completion of a task depends exclusively on the last interaction between an autonomous agent and its environment. Unfortunately, real-world instructions are typically complex and often better described as non-Markovian. In this paper we present an extension method that allows solving partially-observable non-Markovian reward decision processes (PONMRDPs) by solving equivalent Markovian models. This potentially facilitates Markovian-based state-of-the-art techniques, including RL, to find optimal behaviours for problems best described as PONMRDP. We provide formal optimality guarantees of our extension methods together with a counterexample illustrating that naive extensions from existing techniques in fully-observable environments cannot provide such guarantees.

The topic of communication networks has gained recent interest in the field of multi-agent learning (MAL) with many players. It is known that, in certain classes of games, learning agents can converge to an equilibrium. However, with a larger number of players, learning can become increasingly unpredictable. To make progress on this front, we study the behaviour of learning on Network Aggregative (NA) games, in which each player’s reward depends only on their own strategy and that of their neighbours. In particular, we present a continuous time analysis of the Fictitious Play (FP) learning dynamic on NA games. We first show that the NA model allows FP to equilibriate when the game is zero-sum. We find that this occurs regardless of the existence of self-loops in the network and provide conditions under which the fixed point corresponds to a Nash equilibrium. We then advance recent results in network games by considering FP in arbitrary NA games. Specifically, we show that agents learning through Fictitious Play achieve no-regret, regardless of the type of game being played or the number of agents in the system. Finally, we present experimental evidence of a family of games for which Fictitious Play reaches a limit cycle and evidence that the introduction of noise has the potential to break this cyclic behaviour and allow agents to eventually reach the Nash equilibrium.

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.

This work addresses the problem of grounded agents learning systematically from formally specified instructions and generalising their learning to execute zero-shot ie, never-seen-before, specifications. To the best of our knowledge, we are the first to provide evidence that systematic learning can emerge with abstract operators (such as negation) when learning from a limited variety of training examples, which previous research has struggled with. In particular, we find that within a neural network, the particular architecture of convolutional layers are key when grounded agents generalise to new instructions. We also present a neuro-symbolic framework where a symbolic module transforms temporal specifications into a form that helps the training of a deep RL agent targeting generalisation, while a neural module learns systematically to solve the given tasks. Through this framework, we achieve agents that execute multi-task, zero-shot instructions.

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 Δ₂ᴾ-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).

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.

Temporal logic (TL) is an expressive way of specifying complex goals in reinforcement learning (RL), which facilitates the design of reward functions. However, the combination of these two techniques is prone to generate sparse rewards, which might hinder the learning process. Evolutionary algorithms (EAs) hold promise in tackling this problem by encouraging the diversification of policies through exploration in the parameter space. In this paper, we present GEATL, the first hybrid on-policy evolutionary-based algorithm that combines the advantages of gradient learning in deep RL with the exploration ability of evolutionary algorithms, in order to solve the sparse reward problem pertaining to TL specifications. We test our approach in a delayed reward scenario. Differently from previous baselines combining RL and TL, we show that GEATL is able to tackle complex TL specifications even in sparse-reward settings.

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.

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.

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.

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.

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.

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.

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 study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLK_BR, a bounded-recall variant of the temporal-epistemic 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.

Humans engage in informal debates on a daily basis. By expressing their opinions and ideas in an argumentative fashion, they are able to gain a deeper understanding of a given problem and in some cases, find the best possible course of actions towards resolving it. In this paper, we develop a methodology to verify debates formalised as abstract argumentation frameworks. We first present a translation from debates to transition systems. Such transition systems can model debates and represent their evolution over time using a finite set of states. We then formalise relevant debate properties using temporal and strategy logics. These formalisations, along with a debate transition system, allow us to verify whether a given debate satisfies certain properties. The verification process can be automated using model checkers. Thus, we also measure their performance when verifying debates, and use the results to discuss the feasibility of model checking debates.

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 Δ₂ᴾ-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.

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.

In recent years the area of knowledge representation and reasoning (KR&R) has witnessed a growing interest in the modelling and analysis of data-driven/data-centric systems. These are systems in which the two tenets of data and processes are given equal importance, differently from traditional approaches whereby the data content is typically abstracted away in order to make the reasoning task easier. However, if data-aware systems (DaS) are to be deployed in concrete KR&R scenarios, it is key to develop tailored verification techniques, suitable to account for both data and processes. In this contribution we consider for the first time to our knowledge the parameterised verification of DaS. In particular, we prove that – under specific assumptions – this problem is decidable by computing a suitable cut-off value. We illustrate the proposed approach with a use case from the literature on business process modelling.

We introduce a logic to reason about strategic abilities in finite games under imperfect information. We interpret Alternating-time Temporal Logic on interpreted systems with final states, where agents only have partial observability of the system’s global state. We consider the model checking problem in this setting. We prove that the complexity results available for the case of infinite traces carry over to the finite traces case. We show that when only public actions are allowed, the verification problem under perfect recall becomes decidable.

In this technical report, we mainly focus on the translation from Game Description Language with Imperfect Information (GDL-II) to a Concurrent Game Structure with imperfect information (iCGS) using Alternating-time Temporal Logic (ATL), as well as the relationship between the two. This section provides the background information on the syntax and semantics of GDL-II, and the syntax of ATL and its semantics over iCGS.

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.

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.

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.

This extended abstract studies the aggregation of knowledge represented as finite relational databases. It applies a social choice perspective to database aggregation and asks which aggregation procedures preserve integrity constraints satisfied by the individual databases. The approach relates logical properties of databases to properties of aggregation rules, including anonymity, independence and monotonicity.

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.

Most formalisms for multi-agent systems (MAS) are not adept at explicitly expressing of data sharing between agents. Yet, disclosure and hiding of data amongst agents impacts on their strategic abilities, and so has a strong baring on non-classical logics that formally capture agents’ coalitions, e.g., Alternating-time Temporal Logic (ATL) [1]. To this end, we devise concurrent game structures with propositional control for atom-visibility (vCGS). In vCGS, agents a and b have an explicit endowment to see some of each others’ variables, without other agents partaking in this. Second, we ascertain that the model checking problem for ATL with imperfect information and perfect recall on vCGS is undecidable. Third, we put forward a methodology to model check a formula φ in ATL* on a vCGS M, by verifying a suitable translation of φ in a submodel of M.

We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.

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.

This book constitutes the revised selected papers from the 15th European Conference on Multi-Agent Systems, EUMAS 2017, and the 5th International Conference on Agreement Technologies, AT 2017, held in Evry, France, in December 2017. The 28 full papers, 3 short papers, and 2 invited papers for EUMAS and the 14 full papers and 2 short papers for AT, presented in this volume were carefully reviewed and selected from a total of 76 submissions. The papers cover thematic areas like agent-based modelling; logic and formal methods; argumentation and rational choice; simulation; games; negotiation, planning, and coalitions; algorithms and frameworks; applications; and philosophical and theoretical studies.

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 summarized 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.

This extended abstract studies the verification of multi-agent systems with imperfect information and perfect recall. It shows that model checking remains decidable when private actions may occur only a bounded number of times along an execution. It also extends the temporal language underlying epistemic Strategy Logic from linear temporal logic to linear dynamic logic without increasing the computational cost, allowing verification of a broader class of systems and specifications.

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.

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.

This workshop paper introduces a formalism for explicitly representing private data sharing in multi-agent systems. Agents can control the visibility of propositional variables through private communication channels. The paper studies the resulting strategic abilities using Alternating-time Temporal Logic, establishes undecidability under imperfect information and perfect recall, and identifies a decidable fragment for a restricted class of systems that supports gossiping between agents.

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 decidable, provided some mild assumptions on the interpretation domain.

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 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 unbounded data and show how the technique here introduced can be used to give formal guarantees on the resulting system behaviour.

We study a class of synchronous, perfect-recall multi-agent systems with imperfect information and broadcasting, i.e., fully observable actions. We define an epistemic extension of strategy logic with incomplete information and the assumption of uniform and coherent strategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is decidable with non-elementary complexity. We exemplify the applicability of the framework on a rational secret-sharing scenario.

In this paper we introduce global and local announcement logic (GLAL), a dynamic epistemic logic with two distinct announcement operators – [φ]⁺_A and [φ]⁻_A indexed to a subset of the set of all agents -- for global and local announcements respectively. The boundary case [φ]⁺_Ag corresponds to the public announcement of φ, as known from the literature. Unlike standard public announcements, which are model transformers, the global and local announcements are 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.

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 account 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.

We introduce a 3-valued abstraction technique for alternating-time temporal logic (ATL) in contexts of imperfect information. We introduce under- and over-approximations of an agent’s strategic abilities in terms of must- and may-strategies and provide a 3-valued semantics for ATL based on agents in interpreted systems (IS). We define a relation of simulation between the agents and prove that it preserves defined truth values of ATL formulas. Finally, we introduce a notion of abstraction on IS and show that it simulates the concrete interpreted system. Under this setting we present a procedure that enables the direct construction of a finite abstraction from an infinite-state system.

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 three-ballot 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.

We analyse the verification problem for synchronous, perfect recall multi-agent systems with imperfect information against a specification language that includes strategic as well as epistemic operators. While the general problem is known to be undecidable we show that if the agents’ actions are public then verification is decidable, and we establish that the computational complexity is 2EXPTIME-complete. To illustrate the formal framework we consider two well-known epistemic and strategic puzzles with imperfect information and public actions: the muddy children puzzle and the classic game of battleships.

In this work we review and analyse some recent advances on the application of multi-agent modal logics in the representation of individual and group knowledge, as well as temporal and spatial reasoning. The main theoretical contributions can be summarized as follows. In Chapter 3 we introduce the language of (multi-modal) second-order propositional modal logic (SOPML), an extension of standard modal logic with propositional quantification. We show how SOPML can be usefully adopted as a specification language to express local properties of Kripke frames in modal logic, including higher-order knowledge of agents in epistemic contexts, that is, knowledge agents have about other agents’ knowledge. Further, we prove novel axiomatisation results with respect to several classes of Kripke frames. In particular, we highlight the key role played by common knowledge in obtaining a complete axiomatisation for second-order propositional epistemic logic (SOPEL), the epistemic version of SOPML. In Chapter 4 we introduce original notions of (bi)simulation and prove that they preserve the interpretation of formulas in SOPML. We also define (bi)simulation games and show them as powerful as (bi)simulation relations. Then, we apply this formal machinery to assess the expressive power of SOPML in representing spatial and temporal properties. In Chapter 5 we move to a dynamic setting and introduce second-order public announcement logic (SOPAL) by extending SOPEL with announcement operators. We make use of SOPAL to analyse the notions of knowability, successfulness of announcements, and preservation under arbitrary announcements. Interestingly, SOPAL is proved to be as expressive as SOPEL, but exponentially more succinct. Finally, in Chapter 6, we return to a purely propositional setting and extend public announcement logic (PAL) with operators for both global and local announcements. We illustrate the formal machinery by means of scenarios in multi-agent systems and prove that this logic is strictly more expressive than PAL. The final outcome of these investigations is a family of expressive modal languages, suitable to reason about relevant concepts in knowledge representation, while still enjoying nice computational properties.

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.

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 (CL-PC). 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.

In this paper we introduce Second-order Propositional Announcement Logic (SOPAL): a language to express arbitrary announcements in Public Announcement Logic, by means of propositional quantification. We present SOPAL within a multi-agent context, and show that it is rich enough to express complex notions such as preservation under arbitrary announcements, knowability, and successfulness. We analyse the model theory of SOPAL and prove that it is strictly more expressive than Arbitrary PAL [2], and as expressive as Second-order Propositional Epistemic Logic [4], even though exponentially more succinct than the latter. These results points to a rich logic, with nice computational properties nonetheless, such as a decidable model checking problem and a complete axiomatisation.

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.

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 system’s 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.

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.

The paper is a contribution at the interface of social network theory and multi-agent systems. As realistic models of multi-agent systems, we assume agent networks to be open, that is, agents may join or leave the network at run-time, and dynamic, that is, the network structure may change as a result of agents’ actions. We provide a formal model of open dynamic agent networks (ODAN) in terms of interpreted systems, and define the problem of model checking properties of diffusion phenomena, such as the spread of information or diseases, expressed in a first-order version of computation-tree logic. We establish the decidability of the model checking problem by showing that, under specific conditions, the verification of infinite-state ODAN can be reduced to model checking finite bisimulations.

In this paper we put forward Epistemic Strategy Logic (ESL), a logic of knowledge and strategies in contexts of imperfect information. ESL extends Strategy Logic by adding modal operators for individual and collective knowledge. This enhanced framework allows us to represent explicitly and to reason about the knowledge agents have of their own and other agents’ strategies. We provide a semantics to ESL in terms of epistemic concurrent game models, then illustrate the expressive power of ESL as a specification language for games, both of perfect and imperfect information. Notably, we show that some fixed-point characterisations of operators for strategic abilities, which normally fail in contexts of imperfect information, can be recovered in a controlled way through the interplay of epistemic and strategy modalities.

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 with respect to various classes of Kripke frames. Finally, we prove that model checking EQBL is PSPACE-complete.

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 first-order 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.

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.

Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycles, accounting respectively for the relational structure of the artifacts’ states and their possible evolutions over time. In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. Differently from the usual process-based models of services, we give a semantics that explicitly accounts for the data structures on which artifact systems are defined. We study the model checking problem for artifact-centric multi-agent systems against specifications expressed in a quantified version of temporal-epistemic logic expressing the knowledge of the agents in the exchange. We begin by noting that the problem is undecidable in general. We identify a noteworthy class of systems that admit bisimilar, finite abstractions. It follows that we can verify these systems by investigating their finite abstractions; we also show that the corresponding model checking problem is EXPSPACE-complete. We then introduce artifact-centric programs, compact and declarative representations of the programs governing both the artifact system and the agents. We show that, while these in principle generate infinite-state systems, under natural conditions their verification problem can be solved on finite abstractions that can be effectively computed from the programs. We exemplify the theoretical results here pursued through a mainstream procurement scenario from the artifact systems literature.

The formal verification of Artifact-centric (AC) systems is a subject of growing interest in the Service Oriented Computing (SOC) community, which can benefit from techniques developed for Multiagent systems and knowledge reasoning and representation. In the present contribution we consider the verification of AC systems that do not necessarily satisfy boundedness and uniformity, the typical assumptions used to prove decidability of the model checking problem in this setting. We provide a partial model checking procedure for agent-based AC systems against a first-order temporal logic that includes modal operators for agent knowledge. Interestingly, we obtain this result by introducing a counterpart semantics for first-order modal logic, and by defining notions of simulation and abstraction for this setting. This allows us to generate finite abstractions of infinite-state AC systems, even when these are not bounded nor uniform, thus enabling us to perform verification also in cases not covered by the current state-of-the-art.

In this paper we introduce Epistemic Strategy Logic (ESL), an extension of Strategy Logic with modal operators for individual knowledge. This enhanced framework allows us to represent explicitly and to reason about the knowledge agents have of their own and other agents' strategies. We provide a semantics to ESL in terms of epistemic concurrent game models, and consider the corresponding model checking problem. We show that the complexity of model checking ESL is not worse than (non-epistemic) Strategy Logic.

These slides present the verification of auctions using artifact-centric multi-agent systems, with parallel English auctions as a motivating example. They introduce first-order temporal-epistemic specifications and show how finite bisimilar abstractions support verification of rigid, uniform and bounded systems. The presentation discusses the limits of these assumptions and directions for constructive abstraction and boundedness checks.

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 artifact-centric 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.

Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, non-uniform 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 artifact-centric systems, hence perform verification on abstract models.

We investigate a class of first-order temporal-epistemic logics for reasoning about multi-agent systems. We encode typical properties of systems including perfect recall, synchronicity, no learning, and having a unique initial state in terms of variants of quantified interpreted systems, a first-order extension of interpreted systems. We identify several monodic fragments of first-order temporal-epistemic logic and show their completeness with respect to their corresponding classes of quantified interpreted systems.

We present a methodology for the automated verification of quantum protocols using MCMAS, a symbolic model checker for multi-agent systems. The method is based on the logical framework developed by D'Hondt and Panangaden for investigating epistemic and temporal properties, built on the model for Distributed Measurement-based Quantum Computation (DMC), an extension of the Measurement Calculus to distributed quantum systems. We describe the translation map from DMC to interpreted systems, the typical formalism for reasoning about time and knowledge in multi-agent systems. Then, we introduce dmc2ispl, a compiler into the input language of the MCMAS model checker. We demonstrate the technique by verifying the Quantum Teleportation Protocol, and discuss the performance of the tool.

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 temporal-epistemic 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.

These slides introduce artifact-centric multi-agent systems as a framework for reasoning about data-aware business processes. They present a first-order temporal-epistemic specification language and use bisimulation and finite abstraction to verify bounded artifact systems. The presentation discusses artifact programs, uniformity assumptions and the limits of verification for unbounded systems.

The GSM framework provides a methodology for the development of artifact-centric systems, an increasingly popular paradigm in service-oriented computing. In this paper we tackle the problem of verifying GSM programs in a multi-agent system setting. We provide an embedding from GSM into a suitable multi-agent systems semantics for reasoning about knowledge and time at the first-order level. While we observe that GSM programs generate infinite models, we isolate a large class of “amenable” systems, which we show admit finite abstractions and are therefore verifiable through model checking. We illustrate the contribution with a procurement use-case taken from the relevant business process literature.

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.

We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for the monodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalism by analysing message passing systems, a typical framework for distributed systems, in a first-order setting.

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 checking a memory-less interpreted system against a CTLK property 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.

Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycle models, accounting for the relational structure of the artifact state and its possible evolutions over time. We consider the problem of verifying artifact systems against specifications expressed in quantified temporal logic. This problem is in general undecidable. However, when artifact systems are deployed, their states can contain only a bounded number of elements. We exploit this fact to develop an abstraction technique that enables us to verify deployed artifact systems by model checking their bounded abstraction.

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.

We introduce an automata-theoretic approach for the verification of multi-agent systems. We present a translation between branching time temporal-epistemic logic and alternating tree automata. Model checking an interpreted system against a temporal-epistemic formula is reduced to checking the non-emptiness of the composition of two tree automata. We exemplify this technique using a simple multi-agent scenario.

We introduce quantified interpreted systems, a semantics to reason about knowledge in multi-agent systems in a first-order setting. Quantified interpreted systems may be used to interpret a variety of first-order modal epistemic languages with global and local terms, quantifiers, and individual and distributed knowledge operators for the agents in the system. We define first-order modal axiomatisations for different settings, and show that they are sound and complete with respect to the corresponding semantical classes. The expressibility potential of the formalism is explored by analysing two MAS scenarios: an infinite version of the muddy children problem and a version of the battlefield game. We also apply the theoretical results to the analysis of message passing systems and compare the results obtained to their propositional counterparts.

We introduce and investigate quantified interpreted systems, a semantics to reason about knowledge and time in a first-order 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.

We investigate quantified interpreted systems, a semantics to model multi-agent systems in which the agents can reason about individuals, their properties, and relationships among them. The semantics naturally extends interpreted systems to first-order by introducing a domain of individuals. We present a first-order epistemic language interpreted on this semantics and prove soundness and completeness of the quantified modal system QS5^D_n, an axiomatisation for these structures. Finally, we exemplify the use of the logic by modeling message passing systems, a relevant class of interpreted systems analysed in epistemic logic.

In this paper we make use of counterpart semantics to prove an original incompleteness result in quantified modal logic (QML), that is, the system QE.K+BF based on free logic and containing the Barcan formula is incomplete with respect to Kripke semantics. This incompleteness result extends to the system QE.K+CBF+BF obtained by adding the converse of the Barcan formula to QE.K+BF.

We investigate quantified interpreted systems, a semantics for multiagent systems in which agents can reason about individuals, their properties, and the relationships among them. We analyse a first-order epistemic language interpreted on this semantics and show soundness and completeness of Q.S5n, an axiomatisation for these structures.

This chapter examines Kripke and counterpart semantics for quantified modal logic and their philosophical relevance to actualism. It identifies limitations of Kripke semantics and an incompleteness result for a free-logic calculus containing the Barcan formula, then presents counterpart semantics as a more refined account of the modal properties of individuals.

We present a family of quantified epistemic logics for reasoning about knowledge in multi-agent systems. The language enjoys flexible terms with different denotations depending on the epistemic context in which they are interpreted. We present syntax and semantics of the language formally and show completeness of an axiomatisation. We discuss the expressive features of the language by means of an example.

This doctoral dissertation concerns quantified modal logic and the ontology of physical objects.

Queste note seminariali discutono il problema della trans-identità degli individui attraverso l’analisi di Chihara in The Worlds of Possibility. Esaminano criteri di identificazione e continuità, presentano una nota formale e confrontano diverse proposte, incluse le soluzioni di Forbes e le critiche di Chihara.

In the present paper we deal with substitution of identicals in intensional contexts salva veritate. First we present Quine’s criticism of quantified modal logic appearing in [7], according to which intensional contexts are referentially opaque and imply Aristotelian essentialism. Quine concludes that quantified modal logic is irremediably flawed. Then we consider Quine’s analysis of epistemic contexts in [6], and his distinction between two notions of belief: belief1 and belief2. By means of the machinery of λ-abstraction presented in [1], we show that Quine’s dichotomy corresponds to the de re/de dicto distinction. Since epistemic contexts are a particular case of intensional contexts and Quine deems quantification admissible for the notion of belief2, we conclude that quantification in modal logic is in part accepted by Quine, even if not openly.

Il manoscritto esamina il rapporto tra logica modale quantificata e ontologia degli oggetti fisici. Confronta interpretazioni logiche e teorie della persistenza, discutendo tridimensionalismo, quadridimensionalismo e sequenzialismo, e propone un’analisi formale dei problemi di identità e reidentificazione degli oggetti.

We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17].

This dissertation studies proof-theoretic and semantic treatments of substructural logics, covering Hilbert calculi, algebraic semantics, relational semantics for relevance and non-distributive logics, decidability, cut elimination, and finite model properties.