Multiplayer computer games play a big role in the ever-growing entertainment industry. Being competitive in this industry means releasing the best possible software, and reliability is a key feature to win the market. Computer games are also actively used to simulate different robotic systems where reliability is even more important, and potentially critical. Traditional software testing approaches can check a subset of all the possible program executions, and they can never guarantee complete absence of errors in the source code. On the other hand, during more than twenty years, Model Checking has demonstrated to be a powerful instrument for formal verification of large hardware and software components. In this paper, we contribute with a novel approach to formally verify computer games. We propose a method of model construction that starts from a computer game description and utilizes Model Checking technique. We apply the method on a case study: the game Penguin Clash. Finally, an approach to game model reduction (and its implementation) is introduced in order to address the state explosion problem.
@cite_27: The field of multi-agent dynamic systems is an inter-disciplinary research field that has become very popular in the recent years in parallel with the significant interest in the practical applications of such systems in various areas including robotics. In this article we give a relatively short review of this field from the system dynamics and control perspective. We first focus on mathematical modelling of multi-agent systems paying particular attention on the agent dynamics models available in the literature. Then we present a number of problems on coordination and control of multi-agent systems which have gained significant attention recently and various approaches to these problems. Relevant to these problems and approaches, we summarize some of the recent results on stability, robustness, and performance of multi-agent dynamic systems which appeared in the literature. The article is concluded with some remarks on the implementation and application side of the control designs developed for multi-agent systems.
Model Checking approach can be also a valuable tool for formal simulation and verification in swarms and swarm robotics, where multi-agent dynamic system behavior is frequently described by directed and undirected graphs and their geometric representations in a particular motion space @cite_27 . These graphs @math typically take into account the communication, information flow and interaction scenarios between agents @math in a swarm @math by a weighted graph representation @math , where @math is a vertex (node) set of agents @math with @math , @math is an edge set, which describes an information link @math between a pair @math of agents, and a weighting set @math defines the desired weights @math that represent a control goal or a critical parameter (e.g., a distance between @math ). The structure and properties of @math strictly depend on the hardware and software features of the swarm agents.