In this paper we investigate the model-checking problem of pushdown multi-agent systems for ATL* specifications.To this aim, we introduce pushdown game structures over which ATL* formulas are interpreted. We show an algorithm that solves the addressed model-checking problem in 3ExpTime. We also provide a 2ExpSpace lower bound by showing a reduction from the word acceptance problem for deterministic Turing machines with doubly exponential space.

This paper studies the complexity of model checking multiagent systems, in particular systems succinctly described by two practical representations: concurrent representation and symbolic representation. The logics we concern include branching time temporal logics and several variants of alternating time temporal logics.

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.

Multi-Agent Path Finding (MAPF) deals with the problem of finding collision-free paths for a set of agents, where each agent wants to move from its start location to its goal location on a shared graph. The paper addresses the question of how to model MAPF as a classical planning problem, specifically, how to encode various collision constraints. Several models in the PDDL modeling language are proposed and empirically compared.

We consider a setting where an agent-based planner instructs teams of human emergency responders to perform tasks in the real world. Due to uncertainty in the environment and the inability of the planner to consider all human preferences and all attributes of the real-world, humans may reject plans computed by the agent. A naive solution that re-plans given a rejection is inefficient and does not guarantee the new plan will be acceptable. Hence, we propose a new model re-planning problem using a Multi-agent Markov Decision Process that integrates potential rejections as part of the planning process and propose a novel algorithm to efficiently solve this new model. We empirically evaluate our algorithm and show that it outperforms current benchmarks. Our algorithm is also shown to perform better in pilot studies with real humans.

In this paper, we formalize and study the Moving Agents in Formation (MAiF) problem, that combines the tasks of finding short collision-free paths for multiple agents and keeping them in close adherence to a desired formation. Previous work includes controller-based algorithms, swarm-based algorithms, and potential-field-based algorithms. They usually focus on only one or the other of these tasks, solve the problem greedily without systematic search, and thus generate costly solutions or even fail to find solutions in congested environment. In this paper, we develop a two-phase search algorithm, called SWARM-MAPF, whose first phase is inspired by swarm-based algorithms (in open regions) and whose second phase is inspired by multi-agent path-finding (MAPF) algorithms (in congested regions). In the first phase, SWARM-MAPF selects a leader among the agents and finds a path for it that is sufficiently far away from the obstacles so that the other agents can preserve the desired formation around it.

Pricing-based mechanisms have been widely studied and developed for resource allocation in multi-agent systems. One of the main goals in such studies is to avoid envy between the agents, i.e., guarantee fair allocation. However, even the simplest combinatorial cases of this problem is not well understood. Here, we try to fill these gaps and design polynomial revenue maximizing pricing mechanisms to allocate homogeneous resources among buyers in envy-free manner. In particular, we consider envy-free outcomes in which all buyers' utilities are maximized. We also consider pair envy-free outcomes in which all buyers prefer their allocations to the allocations obtained by other agents. For both notions of envy-freeness, we consider item and bundle pricing schemes. Our results clearly demonstrate the limitations and advantages in terms of revenue between these two different notions of envy-freeness.

In the Multi-Agent Meeting (MAM) problem, the task is to find a meeting location for multiple agents, as well as a path for each agent to that location. In this paper, we introduce MM*, a Multi-Directional Search algorithm that finds the optimal meeting location under different cost functions. A number of admissible heuristics are proposed and experiments demonstrate the benefits of MM*.

Interactive dynamic influence diagrams(I-DIDs) are a well recognized decision model that explicitly considers how multiagent interaction affects individual decision making. To predict behavior of other agents, I-DIDs require models of the other agents to be known ahead of time and manually encoded. This becomes a barrier to I-DID applications in a human-agent interaction setting, such as development of intelligent non-player characters(NPCs) in real-time strategy(RTS) games, where models of other agents or human players are often inaccessible to domain experts. In this paper, we use automatic techniques for learning behavior of other agents from replay data in RTS games. We propose a learning algorithm with improvement over existing work by building a full profile of agent behavior. This is the first time that data-driven learning techniques are embedded into the I-DID decision making framework. We evaluate the performance of our approach on two test cases.

Multi-Agent Path Finding (MAPF) is the problem of finding non-colliding paths for multiple agents. The classical problem assumes that all agents are homogeneous, with a fixed size and behavior. However, in reality agents are heterogeneous, with different sizes and behaviors. In this paper, we generalize MAPF to G-MAPF for the case of heterogeneous agents. We then show how two previous settings of large agents and k-robust agents are special cases of G-MAPF.