Multi-player mean-payoff games are a natural formalism for modelling the behaviour of concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while attempting to maximise a (mean-)payoff function that depends on the play generated. As with all games, the equilibria that could arise may have undesirable properties. However, as system designers, we typically wish to ensure that equilibria in such systems correspond to desirable system behaviours, for example, satisfying certain safety or liveness properties. One natural way to do this would be to specify such desirable properties using temporal logic. Unfortunately, the use of temporal logic specifications causes game theoretic verification problems to have very high computational complexity. To address this issue, we consider ω-regular specifications. These offer a concise and intuitive way of specifying system behaviours with a comparatively low computational overhead. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given ω-regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.
ABSTRACTA robust testing program is necessary for containing the spread of COVID-19 infections before a vaccine becomes available. However, due to an acute shortage of testing kits (especially in low-resource developing countries), designing an optimal testing program/strategy is a challenging problem to solve. Prior literature on testing strategies suffers from two major limitations: (i) it does not account for the trade-off between testing of symptomatic and asymptomatic individuals, and (ii) it primarily focuses on static testing strategies, which leads to significant shortcomings in the testing program’s effectiveness. In this paper, we address these limitations by making five novel contributions. (i) We formally define the optimal testing problem and propose the DOCTOR POMDP model to tackle it. (ii) We solve the DOCTOR POMDP using a scalable Monte Carlo tree search based algorithm. (iii) We provide a rigorous experimental analysis of DOCTOR’s testing strategies against static baselines - our results show that when applied to the city of Santiago in Panama, DOCTOR’s strategies result in ∼40% fewer COVID-19 infections (over one month) as compared to state-of-the-art static baselines. (iv) In addition, we analyze DOCTOR’s testing policy to derive insights about the reasons behind the optimality of DOCTOR’s testing policy. (v) Finally, we characterize conditions (of the real world) under which DOCTOR’s optimization would be of most benefit to government policy makers, and thus requires significant attention from researchers in this area. Our work complements the growing body of research on COVID-19, and serves as a proof-of-concept that illustrates the benefit of having an AI-driven adaptive testing strategy for COVID-19.
Deploying reinforcement learning (RL) involves major concerns around safety. Engineering a reward signal that allows the agent to maximize its performance while remaining safe is not trivial. Safe RL studies how to mitigate such problems. For instance, we can decouple safety from reward using constrained Markov decision processes (CMDPs), where an independent signal models the safety aspects. In this setting, an RL agent can autonomously find tradeoffs between performance and safety. Unfortunately, most RL agents designed for CMDPs only guarantee safety after the learning phase, which might prevent their direct deployment. In this work, we investigate settings where a concise abstract model of the safety aspects is given, a reasonable assumption since a thorough under-standing of safety-related matters is a prerequisite for deploying RL in typical applications. Factored CMDPs provide such compact models when a small subset of features describe the dynamics relevant for the safety constraints. We propose an RL algorithm that uses this abstract model to learn policies for CMDPs safely, that is without violating the constraints. During the training process, this algorithm can seamlessly switch from a conservative policy to a greedy policy without violating the safety constraints. We prove that this algorithm is safe under the given assumptions. Empirically, we show that even if safety and reward signals are contradictory, this algorithm always operates safely and, when they are aligned, this approach also improves the agent’s performance.
In service robot applications, planning is often integrated with task allocation. Linear Temporal Logic (LTL) as an expressive high-level formalism is widely used for task specification, and allows for formalised restrictions on temporal sequences of tasks. In multiagent planning, a Multi-Objective Markov Decision Process extends the standard model with vector rewards capturing possibly conflicting planning objectives. Such objectives include the success rates of accomplishing individual tasks, and the cost budgets for individual agents. In this paper, we consider the problem of concurrently allocating LTL task sequences to a team of agents and calculating optimal task schedulers simultaneously, satisfying cost and probability thresholds. We reduce this problem to multi-objective scheduler synthesis for a team MDP structure, whose size is linear in the number of agents. Our preliminary experiment demonstrates the scalability of our approach.
This paper addresses an epidemiologic inference problem where, given realtime observation of test results, presence of symptoms, and physical contacts, the most likely infected individuals need to be inferred. The inference problem is modeled as a hidden Markov model where infection probabilities are updated at every time step and evolve between time steps. We suggest a unique inference approach that avoids storing the given observations explicitly. Theoretical justification for the proposed model is provided under specific simplifying assumptions. To complement these theoretical results, a comprehensive experimental study is performed using a custom-built agent-based simulator that models inter-agent contacts. The reported results show the effectiveness of the proposed inference model when considering more realistic scenarios – where the simplifying assumptions do not hold. When pairing the proposed inference model with a simple testing and quarantine policy, promising trends are obtained where the epidemic progression is significantly slowed down while quarantining a bounded number of individuals. © 2021 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
