Multi-Agent Reinforcement Learning with Temporal Logic Specifications

In recent and ongoing work, we have studied the problem of how a group of agents may learn to satisfy temporal logic specifications in unknown, stochastic environments. From a learning perspective these specifications provide a rich formal language with which to capture tasks or objectives, while from a logic and automated verification perspective the introduction of learning capabilities allows for practical applications in large, stochastic, unknown environments. Previous efforts (and in fact all those that consider full linear temporal logic or have correctness guarantees) have focused predominantly on the single-agent, single-objective setting. In contrast, we develop the first multi-agent reinforcement learning technique with convergence and correctness guarantees, even when using function approximators (such as neural networks). Our approach is also novel in its ability to handle lexicographic and linear combinations of specifications alongside standard, scalar utility functions. Based on initial theoretical results, our ongoing work seeks to apply our improved algorithm — Automaton/Logic Multi-Agent (Approximate) Natural Actor-Critic, or ALMA^2NAC — to a range test domains, thoroughly benchmarking it against plausible contenders that range from probabilistic model-checkers to deep multi-agent reinforcement learning algorithms. The proposed presentation will seek to summarise the main results and insights from this line of work, emphasising how learning can be fruitfully applied to settings that combine logic, games, and automata.

Authors

• Lewis Hammond University of Oxford, United Kingdom

Keywords

No keywords are indexed for this paper.