Channel system (computer science)

In computer science, a channel system is a finite state machine similar to communicating finite-state machine in which there is a single system communicating with itself instead of many systems communicating with each other. A channel system is similar to a pushdown automaton where a queue is used instead of a stack. Those queues are called channels. Intuitively, each channel represents a sequence a message to be sent, and to be read in the order in which they are sent.
Definition.
Channel system.
Formally, a channel system (or perfect channel system) formula_1 is defined as a tuple formula_2 with:
Depending of the author, a channel system may have no initial state and may have an empty alphabet.
Configuration.
A configuration or global state of the channel system is a formula_12 tuple belonging to formula_13. Intuitively, a configuration formula_14 represents that a run is in state formula_15 and that its formula_16-th channel contains the word formula_17.
The initial configuration is formula_18, with formula_19 the empty word.
Step.
Intuitively, a transition formula_20 means that the system may goes to control state formula_15 to formula_22 by writing an formula_23 to the end of the channel formula_24. Similarly formula_25 means that the system may goes to control state formula_15 to formula_22 by removing a formula_23 starting the word formula_24.
Formally, given a configuration formula_30, and a transition formula_31, there is a perfect step formula_32, where the step adds a letter formula_23 to the end of the formula_16-th word. Similarly, given a transition formula_35, there is a perfect step formula_36 where the first letter of the formula_16-th word is formula_23 and has been removed during the step.
Run.
A perfect run is a sequence of perfect step, of the form formula_39. We let formula_40 denote that there is a perfect run starting at formula_41 and ending at formula_42.
Languages.
Given a perfect or a lossy channel system formula_1, multiple languages may be defined.
A word over formula_44 is accepted by formula_1 if it is the concatenation of the labels of a run of formula_1. The language defined by formula_1 is the set of words accepted by formula_1.
The set of reachable configuration of formula_1, denoted formula_50 is defined as the set of configuration formula_41 reachable from the initial state. I.e. as the set of configurations formula_42 such that formula_53.
Given a channel formula_54, the channel of formula_54 is the set of tuples formula_56 such that formula_57.
Channel system and Turing machine.
Most problem related to perfect channel system are undecidable. This is due to the fact that such a machine may simulates the run of a Turing machine. This simulation is now sketched.
Given a Turing machine formula_58, there exists a perfect channel system formula_1 such that any run of formula_58 of length formula_61 can be simulated by a run of formula_1 of length formula_63. Intuitively, this simulation consists simply in having the entire tape of the simulated Turing machine in a channel. The content channel is then entirely read and immediately rewritten in the channel, with one exception, the part of the content representing the head of the Turing machine is changed, to simulate a step of the Turing machine computation.
Variants.
Multiple variants of channel systems have been introduced. The two variants introduced below does not allow to simulate a Turing machine and thus allows multiple problem of interest to be decidable.
One channel machine.
A one-channel machine is a channel system using a single channel. The same definition also applies for all variants of channel system.
Counter machine.
When the alphabet of a channel system contains a single message, then each channel is essentially a counter. It follows that those systems are essentially Minsky machines. We call such systems counter machines. This same definition applies for all variants of channel system.
Completely specified protocol.
A completely specified protocol (CSP) is defined exactly as a channel system. However, the notion of step and of run are defined differently.
A CSP admits two kinds of steps. Perfect steps, as defined above, and a message loss transition step. We denote a message loss transition step by formula_64.
Looseness.
A lossy channel system or machine capable of lossiness error is an extension of completely specified protocol in which letters may disappear anywhere.
A lossy channel system admits two kinds of steps. Perfect steps, as defined above, and lossy step. We denote a lossy step, formula_65.
A run in which channel are emptied as soon as messages are sent into them is a valid run according to this definition. For this reason, some fairness conditions may be introduced to those systems.
Channel fairness.
Given a message a channel formula_54, a run is said to be channel fair with respect to formula_54 if, assuming there are infinitely many steps in which a letter is sent to formula_54 then there are infinitely many steps in which a letter is read from formula_54. 
A computation is said to be channel fair if it is channel fair with respect to each channel formula_54.
Impartiality.
The impartiality condition is a restriction to the channel fairness condition in which both the channel and the letter are considered.
Given a message formula_71 and a channel formula_54, a run is said to be impartial with respect to formula_54 and formula_71 if, assuming there are infinitely many steps in which formula_71 is sent to formula_54 then there are infinitely many steps in which formula_71 is read from formula_54. 
A computation is said to be impartial with respect to a channel formula_54 if it is impartial with respect to formula_54 and a messages formula_71. It is said to be impartial if it is impartial with respect to every channels formula_54.
Message fairness.
The message fairness property is similar to impartiality, but the condition only have to hold if there is an infinite number of step at which formula_71 may be read. Formally, a run is said to be message faire with respect to formula_54 and formula_71 if, assuming there are infinitely many steps in which formula_71 is sent to formula_54, and infinitely many step formula_16 which occurs in a state formula_15 such that there exists a transition formula_90, then there are infinitely many steps in which formula_71 is read from formula_54. 
Boundedness.
The run is said to have bounded lossiness if the number of letter removed between two perfect steps is bounded.
Insertion of errors.
A machine capable of insertion of error is an extension of channel system in which letters may appear anywhere.
A machine capable of insertion of error admits two kinds of steps. Perfect steps, as defined above, and insertion steps. We denote an insertion step by formula_93.
Duplication errors.
A machine capable of duplication error is an extension of machine capable of insertion of error in which the inserted letter is a copy of the previous letter.
A machine capable of insertion of error admits two kinds of steps. Perfect steps, as defined above, and duplication steps. We denote an insertion step by formula_94.
A non-duplicate machine capable of duplication error is a machine which ensures that in each channel, the letters alternate between a special new letter #, and a regular letter from the alphabet of message. If it is not the caes, it means a duplication occurred and the run rejects. This process allow to encode any channel system into a machine capable of duplication error, while forcing it not to have errors. Since channel systems can simulate machines, it follows that machines capable of duplication error can simulate Turing machine.
Properties.
The set of reachable configurations is recognizable for lossy channel machines and machines capable of insertions of errors. It is recursively enumerable for machine capable of duplication error.
Problems and their complexity.
This section contain a list of problems over channel system, and their decidability of complexity over variants of such systems.
Termination problem.
The termination problem consists in deciding, given a channel system formula_1 and an initial configuration formula_41 whether all runs of formula_1 starting at formula_41 are finite. This problem is undecidable over perfect channel systems, even when the system is a counter machine or when it is a one-channel machine.
This problem is decidable but nonprimitive recursive over lossy channel system. This problem is trivially decidable over machine capable of insertion of errors.
Reachability problem.
The reachability problem consists in deciding, given a channel system formula_1 and two initial configurations formula_41 and formula_42 whether there is a run of formula_1 from formula_41 to formula_42. This problem is undecidable over perfect channel systems and decidable but nonprimitive recursive over lossy channel system. This problem is decidable over machine capable of insertion of errors .
Reachability problem.
The deadlock problem consists in deciding whether there is a reachable configuration without successor. This problem is decidable over lossy channel system and trivially decidable over machine capable of insertion of errors. It is also decidable over counter machine.
Model checking problem.
The model checking problem consists in deciding whether given a system formula_1 and a CTL**-formula or a LTL-formula formula_106 or a whether the language defined by formula_1 satisfies formula_106. This problem is undecidable over lossy channel system.
Recurrent state problem.
The recurrent state problem consists in deciding, given a channel system formula_1 and an initial configuration formula_41 and a state formula_111 whether there exists a run of formula_1, starting at formula_41, going infinitely often through state formula_111. This problem is undecidable over lossy channel system, even with a single channel.
Equivalent finite state machine.
Given a system formula_1, there is no algorithm which computes a finite state machine representing formula_50 for the class of lossy channel system. This problem is decidable over machine capable of insertion of error .
Boundedness problem.
The boundedness problem consists in deciding whether the set of reachable configuration is finite. I.e. the length of the content of each channel is bounded. This problem is trivially decidable over machine capable of insertion of errors. It is also decidable over counter machine.
Eventually properties.
The eventuality property, or inevitability property problem consists in deciding, given a channel system formula_1 and a set formula_118 of configurations whether all run of formula_1 starting at formula_41 goes through a configuration of formula_118. This problem is undecidable for lossy channel system with impartiality and with the two other fairness constraints.
Safety property.
The safety property problem consists in deciding, given a channel system formula_1 and a regular set formula_123 whether
Structural termination.
The structural termination problem consists in deciding, given a channel system formula_1 if the termination problem holds for formula_1 for every initial configuration. This problem is undecidable even over counter machine.
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 had 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.