Analysis of a class of communicating finite state machines (Q1323365)

The reachability, deadlock detection and unboundedness detection problems are considered for the class of cyclic one-type message networks of communicating finite state machines. We show that all the three problems are effectively solvable by (a) constructing canonical execution event sequences which belong to a context-free language, and (b) showing that the reachability sets are semilinear. Our algorithms have polynomial complexity in terms of size of a global structure of a network, called the shuffle-product. The relationships between general Petri nets and the class of communicating finite state machines considered here are also explored.