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.
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.
@cite_27
2011995167
Designing and analyzing self-organizing systems such as robotic swarms is a challenging task even though we have complete knowledge about the robot’s interior. It is difficult to determine the individual robot’s behavior based on the swarm behavior and vice versa due to the high number of agent–agent interactions. A step towards a solution of this problem is the development of appropriate models which accurately predict the swarm behavior based on a specified control algorithm. Such models would reduce the necessary number of time-consuming simulations and experiments during the design process of an algorithm. In this paper we propose a model with focus on an explicit representation of space because the effectiveness of many swarm robotic scenarios depends on spatial inhomogeneity. We use methods of statistical physics to address spatiality. Starting from a description of a single robot we derive an abstract model of swarm motion. The model is then extended to a generic model framework of communicating robots. In two examples we validate models against simulation results. Our experience shows that qualitative correctness is easily achieved, while quantitative correctness is disproportionately more difficult but still possible.