A Compositional Approach to Bisimulation of Arenas of Finite State Machines

Finite state machines are widely used as a sound mathematical formalism which appropriately describes large scale distributed and complex systems, arising in many technological domains of interest. One of the key issues in the modeling and analysis of such systems is to derive formal methods that cope with their inherent complexity. In this paper we introduce a novel class of non-flat systems that we term arenas of finite state machines. Arenas of finite state machines are collections of finite state machines that interact concurrently through a communication network. By expanding the arena, a flat system is obtained which is an ordinary finite state machine. For this class of non-flat systems we propose a notion of compositional bisimulation, which allows one to check bisimulation equivalence of arenas by directly exploiting their communication networks, without the need of expanding them to the corresponding finite state machines. Computational complexity analysis of the proposed approach is discussed and an illustrative example is included in the paper.