Arenas of Finite State Machines

TL;DR

This paper introduces Arena of Finite State Machines (AFSMs), a new class of non-flat systems that model concurrent interactions in complex systems, enabling efficient bisimulation checks without expansion.

Contribution

The paper proposes AFSMs and a compositional bisimulation method that reduces computational complexity in verifying system equivalence, with an application to gene regulation.

Findings

AFSMs effectively model concurrent finite state systems.

Bisimulation checking is more efficient with the proposed method.

Application demonstrated in gene expression regulation.

Abstract

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.