On conditions to verify progress and finiteness for cyclic communicating machines

Systems of communicating finite state machines model abstract processes which communicate exclusively by exchanging messages through FIFO channels. They can be used to study protocols and distributed computing. This paper discusses a methodology to validate cyclic communicating systems. The communication is assumed asynchronous between processes which exchange exclusively messages over two FIFO channels. A well known reachability analysis is based on the perturbation algorithm. It is designed to explore all reachable global states from the initial states of each process to the final directed graph. This graph is used to verify some suitable properties of the communication. It has been shown earlier that the problem of finiteness of the graph is undecidable in general. We first describe conditions in which the communication progresses between the processes without blocking states. After this, we clarify some sufficient conditions used to decide whether the reachability graph for a given system is finite or infinite. The proposed technique works on particular global states defined as milestones and some potential executed sequences in each process. It guided by cracking the content of channels at each step