Search

We introduce a natural variant of weighted voting games, which we refer to as k-Prize Weighted Voting Games. Such games consist of n players with weights, and k prizes, of possibly differing values. The players form coalitions, and the i-th largest coalition (by the sum of weights of its members) wins the i-th largest prize, which is then shared among its members. We present four solution concepts to analyse the games in this class, and characterise the existence of stable outcomes in games with three players and two prizes, and in games with uniform prizes. We then explore the efficiency of stable outcomes in terms of Pareto optimality and utilitarian social welfare. Finally, we study the computational complexity of finding stable outcomes.

Planning under uncertainty requires complex reasoning about future events, and this complexity increases with the addition of multiple agents. One problem faced when considering multi-agent systems under uncertainty is the handling of shared resources. Adding a resource constraint limits the actions that agents can take, forcing collaborative decision making on who gets to use what resources. Prior work has considered different formulations, such as satisfying a resource constraint in expectation or ensuring that a resource constraint is met some percent of the time. However, these formulations of constrained planning ignore important distributional information about resource usage. Namely, they do not consider how bad the worst cases can get. In this paper, we formulate a risk-constrained shared resource problem and aim to limit the risk of excessive use of such resources. We focus on optimising for reward while constraining the Conditional Value-at-Risk (CVaR) of the shared resource. While CVaR is well studied in the single-agent setting, we consider the challenges that arise from the state and action space explosion in the multi-agent setting. In particular, we exploit risk contributions, a measure introduced in finance research which quantifies how much individual agents affect the joint risk. We present an algorithm that uses risk contributions to iteratively update single-agent policies until the joint risk constraint is satisfied. We evaluate our algorithm on two synthetic domains.

Agent-based models (ABMs) are a promising tool to simulate complex environments. Their rapid adoption requires scalable specification, efficient data-driven calibration, and validation through sensitivity analyses. Recent progress in tensorized and differentiable ABM design (GradABM) has enabled fast calibration of million-size populations, however, validation through sensitivity analysis is still computationally prohibitive due to the need for running the model a large number of times. Here, we present a novel methodology that uses automatic differentiation to perform a sensitivity analysis on a calibrated ABM without requiring any further simulations. The key insight is to leverage gradients of a GradABM to compute exact partial derivatives of any model output with respect to an arbitrary combination of parameters. We demonstrate the benefits of this approach on a case study of the first wave of COVID-19 in London, where we investigate the causes of variations in infections by age, socio-economic index, ethnicity, and geography. Finally, we also show that the same methodology allows for the design of optimal policy interventions. The code to reproduce the presented results is made available on GitHub (https://github.com/arnauqb/one_shot_sensitivity).

Causal reasoning and game-theoretic reasoning are fundamental topics in artificial intelligence, among many other disciplines: this paper is concerned with their intersection. Despite their importance, a formal framework that supports both these forms of reasoning has, until now, been lacking. We offer a solution in the form of (structural) causal games, which can be seen as extending Pearl's causal hierarchy to the game-theoretic domain, or as extending Koller and Milch's multi-agent influence diagrams to the causal domain. We then consider three key questions: i) How can the (causal) dependencies in games - either between variables, or between strategies - be modelled in a uniform, principled manner? ii) How may causal queries be computed in causal games, and what assumptions does this require? iii) How do causal games compare to existing formalisms? To address question i), we introduce mechanised games, which encode dependencies between agents' decision rules and the distributions governing the game. In response to question ii), we present definitions of predictions, interventions, and counterfactuals, and discuss the assumptions required for each. Regarding question iii), we describe correspondences between causal games and other formalisms, and explain how causal games can be used to answer queries that other causal or game-theoretic models do not support. Finally, we highlight possible applications of causal games, aided by an extensive open-source Python library., Published in Artificial Intelligence (2023)

Coalitional resource games (CRGs) provide a natural abstract framework with which to model scenarios in which groups of agents cooperate by pooling resources in order to carry out tasks or achieve individual goals. In this work, we introduce a richer and more general framework, called Łukasiewicz resource games (ŁRG), which is based on many-valued Łukasiewicz logics, whose formulae make it possible to specify the class of piecewise linear polynomial functions with integer and rational coefficients on [ 0 , 1 ] n . The use of Łukasiewicz logics provides a new approach to the representation of the scenario/situations modelled by CRGs. In ŁRGs, each agent is endowed with resources that can be allocated over a set of tasks, where the outcome of a task depends on the profile of resources that are allocated to it. We specify task outcomes using formulae of Łukasiewicz logic. In addition, agents have payoff functions over task outcomes, which are also specified by Łukasiewicz formulae. After motivating and introducing ŁRGs, we formalise notions of coalition structures and the core for ŁRGs and investigate the non-emptiness of the core both from a logical and computational perspective. We prove that ŁRGs are a proper generalisation of CRGs by showing how any CRG can be translated into a ŁRG that is strategically equivalent, in the sense that the former has a non-empty core if and only if so does the latter.

Recent work studied Stackelberg security games with multiple defenders, in which heterogeneous defenders allocate security resources to protect a set of targets against a strategic attacker. Equilibrium analysis was conducted to characterize outcomes of these games when defenders act independently. Our starting point is the observation that the use of resources in equilibria may be inefficient due to lack of coordination. We explore the possibility of reducing this inefficiency by coordinating the defenders-specifically, by pooling the defenders' resources and allocating them jointly. The defenders' heterogeneous preferences then give rise to a collective decision-making problem, which calls for a mechanism to generate joint allocation strategies. We seek a mechanism that encourages coordination, produces efficiency gains, and incentivizes the defenders to report their true preferences and to execute the recommended strategies. Our results show that, unfortunately, even these basic properties clash with each other and no mechanism can achieve them simultaneously, which reveals the intrinsic difficulty of achieving meaningful defense coordination in security games. On the positive side, we put forward mechanisms that fulfill some of these properties and we identify special cases of our setting where more of these properties are compatible.

As we saw in the first part of this short series, a mechanism design problem involves engineering the rules of a game so that, if participants then behave rationally in the game (by choosing strategies that maximize their expected utility, for example), then the result will satisfy some desired property. So far, however, we have said nothing about what these desirable properties might be, or what mechanisms might achieve them. Here, we will dig into these two issues in a little more detail.

Stackelberg security games have received much attention in recent years. While most existing work focuses on single-defender settings, there are many real-world scenarios that involve multiple defenders (e.g., multi-national anti-crime actions in international waters, different security agencies patrolling the same area). In this paper, we consider security games with uncoordinated defenders who jointly protect a set of targets, but may have different valuations for these targets; each defender schedules their own resources and selfishly optimizes their own utility. We generalize the standard (single-defender) model of Stackelberg security games to this setting and formulate an equilibrium concept that captures the nature of strategic interaction among the players. We argue that an exact equilibrium may fail to exist, and, in fact, deciding whether it exists is NP-hard. However, under mild assumptions, every multi-defender security game admits an ε-equilibrium for every ε>0$, and the limit points corresponding to ε\to 0$ can be efficiently approximated.

Game theory provides a well-established framework for the analysis and verification of concurrent and multi-agent systems. Typically, the analysis of a multi-agent system involves computing the set of equilibria in the associated multi-player game representing the behaviour of the system. As systems grow larger, it becomes increasingly harder to find equilibria in the game – which represent the rationally stable behaviours of the multi-agent system (the solutions of the game). To address this issue, in this paper, we study the concept of local equilibria, which are defined with respect to (maximal) stable coalitions of agents for which an equilibrium can de found. We focus on the solutions given by the Nash equilibria of Boolean games and iterated Boolean games, two logic-based models for multi-agent systems, in which the players’ goals are given by formulae of propositional logic and LTL, respectively.

Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a setting involves computing the set of (Nash) equilibria in the concurrent game. However, we show that, with respect to the above model of strategies (arguably, the “standard” model in the computer science literature), bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal logic formulae, may nevertheless have fundamentally different properties (solutions) from a game theoretic perspective. Our aim in this paper is to explore the issues raised by this discovery. After illustrating the issue by way of a motivating example, we present three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the computer science literature.

Linear Dynamic Logic on finite traces (LDLF ) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLF. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDLF goals are considered, in the setting we study— iterated Boolean games with goals over finite traces (iBGF )—players’ goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (Nash) equilibria, shows that the set of Nash equilibria in games with LDL F objectives is regular, and provides complexity results for the associated automata constructions.

Rational verification is the problem of understanding what temporal logic properties hold of a multi-agent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. More specifically, rational verification asks whether a given property, expressed as a temporal logic formula, is satisfied in a computation of the system that might be generated if agents within the system choose strategies for selecting actions that form a Nash equilibrium. We show that, when agents are modelled using the Simple Reactive Modules Language, a widely-used system modelling language for concurrent and multi-agent systems, this problem can be reduced to a simpler query: whether some iterated game—in which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulae—has a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the two-player case for various types of LTL goals, present some experimental results, and describe a general technique to implement rational verification using MCMAS, a model checking tool for the verification of concurrent and multi-agent systems.

In Boolean games, agents uniquely control a set of propositional variables, and aim at achieving a goal formula whose realisation might depend on the choices the other agents make with respect to the variables they control. We consider the case in which assigning a value to propositional variables incurs a cost, and moreover, we assume agents to be restricted in their choice of assignments by an initial endowment: they can only make choices with a lower cost than this endowment. We then consider the possibility that endowments can be redistributed among agents. Different redistributions may lead to Nash equilibrium outcomes with very different properties, and so certain redistributions may be considered more attractive than others. In this context we study centralised redistribution schemes, where a system designer is allowed to redistribute the initial energy endowment among the agents in order to achieve desirable systemic properties. We also show how to extend this basic model to a dynamic variant in which an electric Boolean game takes place over a series of rounds.

Rational verification is concerned with establishing whether a given temporal logic formula φ is satisfied in some or all equilibrium computations of a multi-agent system – that is, whether the system will exhibit the behaviour φ under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the framework of rational verification, we present formal models through which rational verification can be studied, and survey the complexity of key decision problems. We give an overview of a prototype software tool for rational verification, and conclude with a discussion and related work.

The coalition structure generation problem is a natural abstraction of one of the most important challenges in multi-agent systems: How can a number of agents divide themselves into groups in order to improve their performance? More precisely, the coalition structure generation problem focuses on partitioning the set of agents into mutually disjoint coalitions so that the total reward from the resulting coalitions is maximized. This problem is computationally challenging, even under quite restrictive assumptions. This has prompted researchers to develop a range of algorithms and heuristic approaches for solving the problem efficiently. This article presents a survey of these approaches. In particular, it surveys the main dynamic-programming approaches and anytime algorithms developed for coalition structure generation, and considers techniques specifically developed for a range of compact representation schemes for coalitional games. It also considers settings where there are constraints on the coalitions that are allowed to form, as well as settings where the formation of one coalition could influence the performance of other co-existing coalitions.

In Boolean games, agents uniquely control a set of propositional variables, and aim at achieving a goal formula whose realisation might depend on the choices the other agents make with respect to the variables they control. We consider the case in which assigning a value to propositional variables incurs a cost, and moreover, we assume agents to be restricted in their choice of assignments by an initial endowment: they can only make choices with a lower cost than this endowment. We then consider the possibility that endowments can be redistributed among agents. Different redistributions may lead to Nash equilibrium outcomes with very different properties, and so certain redistributions may be considered more attractive than others. In this context we study centralised redistribution schemes, where a system designer is allowed to redistribute the initial energy endowment among the agents in order to achieve desirable systemic properties. We also show how to extend this basic model to a dynamic variant in which an electric Boolean game takes place over a series of rounds.

Strategic social behavior may be held in place by highly sophisticated reasoning, but its stability may also result from a simple iterated imitation and reward structure. The same two perspectives can be taken with respect to other aspects of social life, including the origins of morality. We will explore this tension by taking a look at the interface of classical and evolutionary game theory from a logician’s perspective.

Many sequential decision-making problems require an agent to reason about both multiple objectives and uncertainty regarding the environment's state. Such problems can be naturally modelled as multi-objective partially observable Markov decision processes (MOPOMDPs). We propose optimistic linear support with alpha reuse (OLSAR), which computes a bounded approximation of the optimal solution set for all possible weightings of the objectives. The main idea is to solve a series of scalarized single-objective POMDPs, each corresponding to a different weighting of the objectives. A key insight underlying OLSAR is that the policies and value functions produced when solving scalarized POMDPs in earlier iterations can be reused to more quickly solve scalarized POMDPs in later iterations. We show experimentally that OLSAR outperforms, both in terms of runtime and approximation quality, alternative methods and a variant of OLSAR that does not leverage reuse.

This paper presents a range of expressiveness and complexity results for the specification, computation, and verification of Nash equilibria in multi-player non-zero-sum concurrent games in which players have goals expressed as temporal logic formulae. Our results are based on a novel approach to the characterisation of equilibria in such games: a semantic characterisation based on winning strategies and memoryful reasoning. This characterisation allows us to obtain a number of other results relating to the analysis of equilibrium properties in temporal logic. We show that, up to bisimilarity, reasoning about Nash equilibria in multi-player non-zero-sum concurrent games can be done in ATL^* and that constructing equilibrium strategy profiles in such games can be done in 2EXPTIME using finite-memory strategies. We also study two simpler cases, two-player games and sequential games, and show that the specification of equilibria in the latter setting can be obtained in a temporal logic that is weaker than ATL^*. Based on these results, we settle a few open problems, put forward new logical characterisations of equilibria, and provide improved answers and alternative solutions to a number of questions.

In decision-theoretic planning problems, such as (partially observable) Markov decision problems or coordination graphs, agents typically aim to optimize a scalar value function. However, in many real-world problems agents are faced with multiple possibly conflicting objectives. In such multi-objective problems, the value is a vector rather than a scalar, and we need methods that compute a coverage set, i.e., a set of solutions optimal for all possible trade-offs between the objectives. In this project propose new multi-objective planning methods that compute the so-called convex coverage set (CCS): the coverage set for when policies can be stochastic, or the preferences are linear. We show that the CCS has favorable mathematical properties, and is typically much easier to compute that the Pareto front, which is often axiomatically assumed as the solution set for multi-objective decision problems

Nowadays, multiagent planning under uncertainty scales to tens or even hundreds of agents. However, current methods either are restricted to problems with factored value functions, or provide solutions without any guarantees on quality. Methods in the former category typically build on heuristic search using upper bounds on the value function. Unfortunately, no techniques exist to compute such upper bounds for problems with non-factored value functions, which would additionally allow for meaningful benchmarking of methods of the latter category. To mitigate this problem, this paper introduces a family of influence-optimistic upper bounds for factored Dec-POMDPs without factored value functions. We demonstrate how we can achieve firm quality guarantees for problems with hundreds of agents.

Combined approaches have become a successful technique for CQ answering over ontologies. Existing algorithms, however, are restricted to the logics underpinning the OWL 2 profiles. Our goal is to make combined approaches applicable to a wider range of ontologies. We focus on RSA: a class of Horn ontologies that extends the profiles while ensuring tractability of standard reasoning. We show that CQ answering over RSA ontologies without role composition is feasible in NP. Our reasoning procedure generalises the combined approach for ELHO and DL-LiteR using an encoding of CQ answering into fact entailment w.r.t. a logic program with function symbols and stratified negation. Our results have significant practical implications since many out-of-profile Horn ontologies are RSA.

The Adjusted Winner procedure is an important mechanism proposed by Brams and Taylor for fairly allocating goods between two agents. It has been used in practice for divorce settlements and analyzing political disputes. Assuming truthful declaration of the valuations, it computes an allocation that is envy-free, equitable and Pareto optimal. We show that Adjusted Winner admits several elegant characterizations, which further shed light on the outcomes reached with strategic agents. We find that the procedure may not admit pure Nash equilibria in either the discrete or continuous variants, but is guaranteed to have ∈-Nash equilibria for each ∈ > 0. Moreover, under informed tie-breaking, exact pure Nash equilibria always exist, are Pareto optimal, and their social welfare is at least 3/4 of the optimal.

Machine learning (ML) is becoming ubiquitous in real-world applications, spanning from our domestic devices such as vacuum cleaner robots, smart phones, virtual assistants, to industrial applications such as manipulators, warehouse robots, to public services such as medical imaging, surveillance cameras, energy grid, etc. With the growing ubiquity and interconnection of these devices, interactions among them will soon become commonplace. These emerging ML problems and the interactions among agents can be formulated as Multiagent ML Systems. On the one hand, many complex ML tasks require the cooperation among multiple agents carrying distributed resources and capabilities. On the other hand, multiagent solutions often lead to improved efficiency, robustness and scalability. Among the many aspects of multiagent ML systems, an important research problem is payoff allocation. This is because multiagent ML systems typically receive a global payoff for the overall performance of all agents, while a fine-grained evaluation of each agent's contribution is absent. Nevertheless, these agent-specific payoffs not only offer natural incentives for their contribution and cooperation, but also provide crucial feedback signals for interpreting the agent's contributions and improving the their future cooperative policies. In this thesis, we investigate the properties of emerging multiagent ML systems and address new challenges that arise when applying classic payoff allocation methods from cooperative game theory to them. The first part of the thesis investigates payoff allocation in submodular multiagent ML problems. Though convex games are commonly studied in cooperative game theory, many multiagent ML applications naturally exhibit submodular characteristics. Moreover, properties of the ML applications give rise to increased computational burden, as well as a new type of malicious attack (i.e., the replication manipulation). To address these challenges, we present a theoretical analysis on payoff allocation methods (in particular, semivalues) in submodular cooperative games, and characterise their robustness against the replication manipulation. We then extend our theoretical results to an emerging application of ML data markets and discuss related and more complex attack models. Moreover, we present a sampling method for estimating the payoff allocation methods to address the computational issue. Finally, we empirically validate our results on a classic facility location problem and on real-life machine learning datasets. In the second part of the thesis, we investigate the integration of the payoff allocation into the learning process for guiding multiagent reinforcement learning (MARL) updates. To this end, we present a framework of game-theoretic payoff allocation in MARL for robotic control. Though the payoffs to agents provide crucial reward signals for improving their cooperative policy, a new challenge arises when performing the payoff allocations during learning. That is, the characteristic values of coalitions are absent except for the grand coalition, i.e., the global reward. On the one hand, it is impossible to re-run the simulation for all possible coalitions at each step. On the other hand, brute-force inferring the value of the unseen coalitions would suffer from highly inaccurate estimations due to high dimensional continuous state and action spaces in the robotic application. To address this challenge, we further incorporate a model-based RL module into our payoff allocation framework, and use a learned model of the environment to simulate values of the unseen coalitions. We empirically demonstrate that our model-based payoff allocation framework greatly improves the performance and sample-efficiency of the MARL system on (multiagent) MuJoCo robotic locomotion control tasks. In conclusion, the results presented in this thesis pave the way towards the application of game-theoretic payoff allocation methods in emerging multiagent ML systems, and opens up a number of exciting directions for future research in this topic.

This thesis focuses on two aspects of Stackelberg games — decentralized leadership and follower deception — that stem from reasoning about strategic interactions at a higher level in Stackelberg games. In the first part of the thesis, we study decentralized leadership in Stackelberg games. We focus on a variant of Stackelberg security games that involves multiple leaders, in which the leaders allocate their security resources to protect a set of targets against an attacker; the attacker acts as the follower in the game, surveying the leaders’ strategies and responding rationally afterwards. We aim to understand the game under decentralized leadership and explore ways to coordinate the leaders. To this end, firstly, we propose a novel equilibrium concept to describe the outcome of the game, and we analyze the existence of an equilibrium and the complexity of computing it. Then, we take a mechanism design approach to coordinate the leaders, aiming to design a coordination mechanism that satisfies several natural properties concerning efficiency, incentives, strategyproofness, and stability of strategies it generates. We obtain impossibility results showing that certain combinations of these properties cannot be achieved by any mechanism. On top of that we also present mechanisms for property combinations that are not blocked by the impossibility results. The second part of the thesis is motivated by the finding that, in a Stackelberg game, the follower can benefit from changing the leader’s belief about the game. This can typically happen when the follower is able to tamper with the leader’s attempt of information gathering: for instance, when the leader learns the follower’s type by interacting with the follower, the follower can imitate the behavior of a different follower type, pretending that their payoffs are different than the actual ones. A leader who ignores such strategic manipulation will then be misled into playing optimally against the imitated follower type, which may correspond to a highly suboptimal strategy in the original game. We study the strategic interactions resulting from this deceptive behavior, both from the leader’s and the follower’s perspectives. From the leader’s perspective, we propose a policy-based approach to mitigate potential losses due to follower deception and study the associated problem of computing the optimal policy. From the follower’s perspective, we study the problem of computing the optimal strategy to deceive the leader. Our results provide an almost complete picture of the complexity landscape of these problems in various settings. It is shown that the problems facing the leader are hard in general, whereby we derive inapproximability bounds and also design algorithms that achieve matching approximation ratios; whereas the problems facing the follower are tractable, whereby we design polynomial-time algorithms to compute optimal (or near-optimal) deception strategies for the follower. Our work sheds light on strategic interactions that may arise in Stackelberg games but are not captured by existing solution concepts. It provides frameworks to study these interactions and contributes to the understanding of them through the lens of computation.

The overall aim of our research is to develop techniques to reason about the equilibrium properties of multi-agent systems. We model multi-agent systems as concurrent games, in which each player is a process that is assumed to act independently and strategically in pursuit of personal preferences. In this article, we study these games in the context of finite-memory strategies, and we assume players’ preferences are defined by a qualitative and a quantitative objective, which are related by a lexicographic order: a player first prefers to satisfy its qualitative objective (given as a formula of linear temporal logic) and then prefers to minimise costs (given by a mean-payoff function). Our main result is that deciding the existence of a strict ϵ Nash equilibrium in such games is 2ExpTime-complete (and hence decidable), even if players’ deviations are implemented as infinite-memory strategies. © 2020, Springer-Verlag GmbH Germany, part of Springer Nature.

A group of agents controls a common budget or owns some common resources. The agents need to decide how to divide this budget across various projects, or to distribute the resources among themselves. Each agent has their own preferences about the best use of the resources. We study ways in which the agents can make these decisions in a fair manner. By fairness, we will mean that for every group member, a proportional part of the common budget is spent in accordance with the member's interests. We will also be interested to take into account the interests of subgroups, and when appropriate aim to avoid envy between group members. We consider several settings in this thesis, capturing different types of potential uses of the common budget. For example, we distinguish between projects that come with a fixed cost (and can be either fully funded or not at all), and projects that can flexibly scale with the amount of funding received. We also distinguish between uses that potentially benefit several or all group members (public goods) or uses that benefit only one agent (private goods). For each scenario we consider, we formalise what we might mean by a "fair" outcome, and then design decision rules that guarantee fairness. Where possible, we additionally aim for rules that make Pareto-efficient use of the common budget. Unfortunately, many of our rules can be exploited by strategic agents who misreport their preferences. In these cases, we prove impossibility theorems which imply that no fair decision rule can be resistant to such strategic manipulation. These impossibility theorems are proved using a computer-aided technique based on SAT solvers, which allows us to obtain computer-generated but human-readable proofs. Further, we consider the computational complexity of the decision rules we consider. In most cases, they can be evaluated using efficient algorithms. In other cases, there are NP-completeness results, but we can show that efficient algorithms exist that work when preferences are well-behaved, in the sense of exhibiting underlying structure.

The global financial system is a sociotechnological complex network, in which millions of economic agents interact over timescales ranging from months to milliseconds. The decade since the near-collapse of this system has been characterised by the meteoric rise of computerised algorithmic trading. This transition has resulted in markets that are vulnerable to new forms of systemic risk, as exemplified by the Flash Crash of May 2010, and related events. The failure of extant models to predict, or mitigate, either the Global Financial Crisis, or the Flash Crash, has led financial regulators to increasingly engage with academia in search of new approaches through which to understand such systems. Agent-based modelling, rooted in complex systems theory, has emerged as a compelling method. However, there remains a pressing regulatory need to understand how systemic (macro- level) network effects are influenced by (micro-level) algorithmic trading. To address this, we developed and assessed a novel combination of macro- and micro-level agent-based models of financial markets, demonstrating the benefits and applicability of the agent-based methodology. We con- structed quantitatively validated network representations of all liquid as- set portfolios held by investors in US equities, and then simulated the exchange of assets using quantitatively calibrated and validated market mechanisms, incorporating key regulatory interventions such as price limits and circuit breakers. Our microstructure calibration dataset spans a range of assets and dates that far exceeds previous approaches. By subjecting the validated model to counterfactual scenarios, such as price shocks, alternative network topologies, and alternative agent behaviours, we presented the first in-depth analysis of systemic risk over intraday timescales. We assessed the effectiveness of current, and proposed, regulations at mitigating this new form of high-frequency financial distress. We find that the actions of distressed market participants facilitate new propagation channels for intraday systemic risk, and flash crash contagion, across the financial network. We also find that systemic risk has a complex non-linear dependence on network topology. We further identify stable and unstable network and agent-behaviour scenarios. The scope and complexity of the model allows the first quantitative analysis of the systemic effect of price limits and circuit breakers. Our insights include the fact that current regulation is inadequate in certain circumstances, and that its effectiveness strongly depends on fund liquidation behaviour. We perform the first ever quantification of the effectiveness of a novel pol- icy proposed by a major market participant, and find it could potentially reduce systemic risk. Based on our work and results, we argue that a hybrid micro-macro approach offers a powerful new lens, through which regulators can assess novel threats to financial stability in the modern, computerised, market- place.

Rational verification problem is concerned with checking which temporal logic properties will hold in a system composed of multiple agents which are assumed to behave rationally and strategically in pursuit of individual objectives. Unfortunately, the problem is generally hard from computational point of view, and for the purpose of practical implementations, usually requires specialised techniques. This thesis aims to develop algorithms and study computational complexity results for rational verification in multi-agent systems. Firstly, a practically amenable technique which relies on a reduction to the solution of a collection of parity games is proposed. The technique in this thesis uses a model of strategies that is bisimulation invariant—that is, in which individual strategies for system components are valid across all bisimilar systems, and which satisfy the same temporal logic properties in equilibrium. This approach has been implemented in the Equilibrium Verification Environment (EVE) system. Secondly, some cases in which the problem of rational verification is computationally tractable are investigated. In particular, it is shown that the complexity of rational verification can be reduced from 2EXPTIME-complete to fixed-parameter tractable. Furthermore, improved complexity results when considering quantitative goals, namely mean-payoff utility functions, are also studied. In doing so, a concept called equilibrium design is proposed. This concept is concerned with the design of incentives so that a desirable equilibrium is obtained.

Most logic-based machine learning algorithms rely on an Occamist bias where textual complexity of hypotheses is minimised. Within Inductive Logic Programming (ILP), this approach fails to distinguish between the efficiencies of hypothesised programs, such as quick sort (O(n log n)) and bubble sort (O(n2)). This paper addresses this issue by considering techniques to minimise both the textual complexity and resource complexity of hypothesised robot strategies. We develop a general framework for the problem of minimising resource complexity and show that on two robot strategy problems, 1) Postman 2) Sorter (recursively sort letters for delivery), the theoretical resource complexities of optimal strategies vary depending on whether objects can be composed within a strategy. The approach considered is an extension of Meta-Interpretive Learning (MIL), a recently developed paradigm in ILP which supports predicate invention and the learning of recursive logic programs. We introduce a new MIL implementation, MetagolO, and prove its convergence, with increasing numbers of randomly chosen examples to optimal strategies of this kind. Our experiments show that MetagolO learns theoretically optimal robot sorting strategies, which is in agreement with the theoretical predictions showing a clear divergence in resource requirements as the number of objects grows. To the authors’ knowledge this paper is the first demonstration of a learning algorithm able to learn optimal resource complexity robot strategies and algorithms for sorting lists.

Payoff division schemes from cooperative game theory, such as the Shapley value and Banzhaf index, have recently gained popularity as measures of node centrality in networks. The general idea in this line of research is to treat nodes as players in a cooperative game, to treat a group centrality measure as a characteristic function and to apply a division scheme as a centrality measure. While this research direction is promising, the computational problems that surround it are challenging and are mostly open. On the one hand, the current research lacks sufficient breadth to understand the field and its computational intricacy as a whole. Existing literature has focused on combining a single division scheme (or class of division schemes) with a single group measure and computing it. On the other hand, the current game-theoretic measures lack sufficient depth to be applicable to certain complex but often-encountered settings, such as networks with an overlapping community structure. The aim of this thesis is to (1) provide a broad computational analysis of a wide class of game-theoretic measures, (2) develop a new class of measures for networks with overlapping community structures, (3) propose high-performance game-theoretic measures. With respect to the first issue, we present a generic framework for defining game-theoretic measures and prove that all measures that can be expressed in our framework are computable in polynomial time. The framework applies to a broad class of division schemes called semivalues in combination with a very wide range of group centrality measures, which is the first result of its kind to date. Our second focus is on a class of real-life networks that have an overlapping community structure. We develop a new class of solution concepts - configuration semivalues - and use them to propose a class of centrality measures based on closeness. We develop polynomial algorithms for its computation and apply them to the Warsaw public transportation network, where they produce a highly interpretable ranking that is - arguably - better than other measures. Finally, we propose the generalised closeness interaction index for the purposes of link prediction. We develop polynomial-time algorithms for the computation of our measure and find that it achieves the best results when compared to the state-of-the-art link prediction methods in the literature.

Combined approaches have become a successful technique for CQ answering over ontologies. Existing algorithms, however, are restricted to the logics underpinning the OWL 2 profiles. Our goal is to make combined approaches applicable to a wider range of ontologies. We focus on RSA: a class of Horn ontologies that extends the profiles while ensuring tractability of standard reasoning. We show that CQ answering over RSA ontologies without role composition is feasible in NP. Our reasoning procedure generalises the combined approach for ELHO and DL-LiteR using an encoding of CQ answering into fact entailment w.r.t. a logic program with function symbols and stratified negation. Our results have significant practical implications since many out-of-profile Horn ontologies are RSA.

We present a logical setting that incorporates a belief-revision mechanism within Dynamic-Epistemic logic. As the “static” basis for belief revision, we use epistemic plausibility models, together with a modal language based on two epistemic operators: a “knowledge” modality K (the standard S5, fully introspective, notion), and a “safe belief” modality □ (“weak”, non-negatively-introspective, notion, capturing a version of Lehrer’s “indefeasible knowledge”). To deal with “dynamic” belief revision, we introduce action plausibility models, representing various types of “doxastic events”. Action models “act” on state models via a modified update product operation: the “Action-Priority” Update. This is the natural dynamic generalization of AGM revision, giving priority to the incoming information (i.e., to “actions”) over prior beliefs. We completely axiomatize this logic, and show how our update mechanism can “simulate”, in a uniform manner, many different belief-revision policies.

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.

The idea of only knowing is a natural and intuitive notion to precisely capture the beliefs of a knowledge base. However, an extension to the many agent case, as would be needed in many applications, has been shown to be far from straightforward. For example, previous Kripke frame-based accounts appeal to proof-theoretic constructions like canonical models, while more recent works in the area abandoned Kripke semantics entirely. We propose a new account based on Moss' characteristic formulas, formulated for the usual Kripke semantics. This is shown to come with other benefits: the logic admits a group version of only knowing, and an operator for assessing the epistemic entrenchment of what an agent or a group only knows is definable. Finally, the multi-agent only knowing operator is shown to be expressible with the cover modality of classical modal logic, which then allows us to obtain a completeness result for a fragment of the logic. ispartof: pages:2713-2719 ispartof: Proceedings of 24th International Joint Conference on Artificial Intelligence (IJCAI) vol:2015-January pages:2713-2719 ispartof: IJCAI location:ARGENTINA, Buenos Aires date:25 Jul - 31 Jul 2015 status: published

High-level programming languages are an influential control paradigm for building agents that are purposeful in an incompletely known world. GOLOG, for example, allows us to write programs, with loops, whose constructs refer to an explicit world model axiomatized in the expressive language of the situation calculus. Over the years, GOLOG has been extended to deal with many other features, the claim being that these would be useful in robotic applications. Unfortunately, when robots are actually deployed, effectors and sensors are noisy, typically characterized over continuous probability distributions, none of which is supported in GOLOG, its dialects or its cousins. This paper presents ALLEGRO, a belief-based programming language for stochastic domains, that refashions GOLOG to allow for discrete and continuous initial uncertainty and noise. It is fully implemented and experiments demonstrate that ALLEGRO could be the basis for bridging high-level programming and probabilistic robotics technologies in a general way. ispartof: pages:2762-2769 ispartof: International Joint Conference on Artificial Intelligence (IJCAI) vol:2015-January pages:2762-2769 ispartof: IJCAI location:ARGENTINA, Buenos Aires date:25 Jul - 31 Jul 2015 status: published

We study the problem of inducing logic programs in a probabilistic setting, in which both the example descriptions and their classification can be proba- bilistic. The setting is incorporated in the proba- bilistic rule learner ProbFOIL + , which combines principles of the rule learner FOIL with ProbLog, a probabilistic Prolog. We illustrate the approach by applying it to the knowledge base of NELL, the Never-Ending Language Learner. acceptance rate 28.8% ispartof: pages:1835-1842 ispartof: Proceedings of 24th International Joint Conference on Artificial Intelligence (IJCAI) vol:2015-January pages:1835-1842 ispartof: International Joint Conference on Artificial Intelligence (IJCAI) location:Buenos Aires, Argentina date:25 Jul - 31 Jul 2015 status: published

Existing techniques for inference in probabilistic logic programs are sequential: they first compute the relevant propositional formula for the query of interest, then compile it into a tractable target representation and finally, perform weighted model counting on the resulting representation. We propose TP-compilation, a new inference technique based on forward reasoning. TP-compilation proceeds incrementally in that it interleaves the knowledge compilation step for weighted model counting with forward reasoning on the logic program. This leads to a novel anytime algorithm that provides hard bounds on the inferred probabilities. Furthermore, an empirical evaluation shows that TP-compilation effectively handles larger instances of complex real-world problems than current sequential approaches, both for exact and for anytime approximate inference. ispartof: pages:1852-1858 ispartof: Proceedings of 24th International Joint Conference on Artificial Intelligence (IJCAI) vol:2015-January pages:1852-1858 ispartof: International Joint Conference on Artificial Intelligence location:Buenos Aires date:25 Jul - 1 Aug 2015 status: published