
Communicating finite-state machine

In computer science, a communicating finite-state machine is a finite state machine labeled with "receive" and "send" operations over some alphabet of channels. They were introduced by Brand and Zafiropulo, and can be used as a model of concurrent processes like Petri nets. Communicating finite state machines are used frequently for modeling a communication protocol since they make it possible to detect major protocol design errors, including boundedness, deadlocks, and unspecified receptions.
The advantage of communicating finite state machines is that they make it possible to decide many properties in communication protocols, beyond the level of just detecting such properties. This advantage rules out the need for human assistance or restriction in generality.
Communicating finite state machines can be more powerful than finite state machines in situations where the propagation delay is not negligible (so that several messages can be in transit at one time) and in situations where it is natural to describe the protocol parties and the communication medium as separate entities.
Communicating Hierarchical State Machine.
Hierarchical state machines are finite state machines whose states themselves can be other machines. Since a communicating finite state machine is characterized by concurrency, the most notable trait in a communicating hierarchical state machine is the coexistence of hierarchy and concurrency. This has been considered highly suitable as it signifies stronger interaction inside the machine.
However, it was proved that the coexistence of hierarchy and concurrency intrinsically costs language inclusion, language equivalence, and all of universality.
Definition.
Protocol.
For an arbitrary positive integer formula_1, a protocol with formula_1 process(es) is a quadruple formula_3 with:
Global state.
A global state is a pair formula_21 where 
The initial global state is a pair formula_29 where
Step.
There are two kinds of steps, steps in which message are received and steps in which messages are sent.
A step in which the formula_14 process receive a message
previously sent by the formula_7-th process is a pair of the form
formula_38 when formula_39, with formula_40. Similarly, a pair in which a message is sent by the formula_7-th process to the formula_14-th one is a pair of the form formula_43 when formula_44
Run.
A run is a sequence of global states such that a step relate a state to the next one, and such that the first state is initial.
It is said that a global state formula_21 is reachable if there exists a run passing through this state.
Problems.
It has been proved with the introduction of the concept itself that when two finite state machines communicate with only one type of messages, boundedness, deadlocks, and unspecified reception state can be decided and identified while such is not the case when the machines communicate with two or more types of messages. Later, it has been further proved that when only one finite state machine communicates with single type of message while the communication of its partner is unconstrained, we can still decide and identify boundedness, deadlocks, and unspecified reception state.
It has been further proved that when the message priority relation is empty, boundedness, deadlocks and unspecified reception state can be decided even under the condition in which there are two or more types of messages in the communication between finite state machines.
Boundedness, deadlocks, and unspecified reception state are all decidable in polynomial time (which means that a particular problem can be solved in tractable, not infinite, amount of time) since the decision problems regarding them are nondeterministic logspace complete.
Extensions.
Some extensions considered are:
Channel system.
A channel system is essentially a version of communicating finite-state machine in which the machine is not divided into distinct process. Thus, there is a single state of state, and there is no restriction relating which system can read/write on any channel.
Formally, given a protocol formula_46, its associated channel system is formula_47, where formula_48 is the set of formula_49 and of formula_50.