Arenas of Finite State Machines

Finite state machines are widely used as a sound mathematical formalism that appropriately describes large scale, distributed and complex systems. Multiple interactions of finite state machines in complex systems are well captured by the notion of non-flat systems. Non--flat systems are "finite state machines" where each "state" can be either a basic state or an aggregate of finite state machines. By expanding a non-flat system, a flat system is obtained which is an ordinary finite state machine. In this paper we introduce a novel class of non--flat systems called Arena of Finite State Machines (AFSM). AFSMs are collections of finite state machines that interact concurrently through a communication network. We propose a notion of compositional bisimulation that allows checking bisimulation equivalence of AFSMs by directly exploiting their communication networks and hence, without the need of expanding the AFSMs to finite state machines. Compositional bisimulation allows a computational complexity reduction when checking bisimulation equivalence of AFSMs, as formally quantified in the paper. An application of the proposed framework to the regulation of gene expression in the bacterium Escherichia coli is also presented.