We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems. Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic, where one can specify properties of the type a coalition of (at least) n controllable agents can ensure against (at most) m uncontrollable agents that any possible evolution of the system satisfies a given objective ., where is specified again as a formula of that language and each of n and m is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic L HDMAS and define normal form of its formulae. We then prove that every formula in L HDMAS is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

We study dynamic multi-agent systems (dmass). These are multi-agent systems with explicitly dynamic features, where agents can join and leave the system during the evolution. We propose a general conceptual framework for modelling such dmass and argue that it can adequately capture a variety of important and representative cases. We then present a concrete modelling framework for a large class of dmass, composed in a modular way from agents specified by means of automata-based representations. We develop generic algorithms implementing the dynamic behaviour, namely addition and removal of agents in such systems. Lastly, we state and discuss several formal verification tasks that are specific for dmass and propose general algorithmic solutions for the class of automata representable dmass.

We consider a new generalisation of the Dining Philosophers problem with a set of agents and a set of resource units which can be accessed by them according to a fixed graph of accessibility between agents and resources. Each agent needs to accumulate a certain (fixed for the agent) number of accessible resource units to accomplish its task, and once it is accomplished the agent releases all resources and starts accumulating them again. All this happens in succession of discrete ‘rounds’ and yields a concurrent game model of ‘dynamic resource allocation’. We use the Alternating time Temporal Logic (ATL) to specify important properties, such as goal achievability, fairness, deadlock, starvation, etc. These can be formally verified using the efficient model checking algorithm for ATL. However, the sizes of the resulting explicit concurrent game models are generally exponential both in the number of resources and the number of agents, which makes the ATL model checking procedure generally intractable on such models, especially when the number of resources is large. That is why we also develop an abstract representation of the dynamic resource allocation models and develop a symbolic version of the model checking procedure for ATL. That symbolic procedure reduces the time complexity of model checking to polynomial in the number of resources, though it can take a worst-case double exponential time in the number of agents.