A lossy channel system (LCS) is a computational model where nondeterministic finite automata communicate over a faulty network.[1] They are notable in that certain LCS-related verification problems achieve a computational complexity of \(\mathbf{F}_{\omega^\omega}\)-complete, using a complexity class analog of the fast-growing hierarchy.
Priority channel systems allow the automata to mark certain messages as more important than others, yielding a more powerful system with \(\mathbf{F}_{\varepsilon_0}\)-complete verification problems.
Definition[]
An LCS has a finite message alphabet \(M\), set of \(m\) channels, a finite number of states, and a transition table. Each channel is a string containing characters from \(M\). Each character in the channel should be thought of as the value of a message.
The transition table contains a number of productions, which consist of the following:
- The initial state and successive state.
- The channel c to read or write from.
- An opcode, which can be either ? (read) or ! (write).
- The message a to be written or read.
The transition table can be thought of as a directed multigraph where the nodes are states and the productions are edges, placed according to their initial and successive states, and labeled with the channel/opcode/message data.
Agents[]
LCS simulation is done with one or more nondeterministic agents. Multiple agents can run on a single LCS, in which any agent is chosen at each step. Concurrent agents share channels but otherwise do not interact. In this article, we are not concerned with multiple-agent LCS's, which are computationally equivalent.
An LCS agent has an internal state. It may either make a reliable step, where the agent receives or transmits messages, or an lossy step, which simulates the network dropping messages. A configuration consists of the LCS's state and the contents of the channels.
For a reliable step, the agent selects a production with an initial state equal to the current state. What it does next depends on the opcode:
- If the opcode is ?, the agent looks at the selected channel c and ensures that the first message is a. It then removes a from that channel. If the first message is not a, then the agent is not allowed to use this production.
- If the opcode is !, the agent appends a to channel c.
After executing the opcode, the agent moves on to the successive state of the production. Note that the read operation removes from the beginning of the string, and the write operation adds to the end of the string. In this way, channel strings can be thought of as first-in first-out stacks.
For the lossy step, the agent selects a non-empty channel and removes a message from anywhere in that channel.
A simulation is a sequence of configurations formed by repeated legal steps. A simulation is maximal iff it goes on infinitely or halts. Halting is defined as reaching a configuration where no further steps are possible (i.e. all matching productions are read instructions that do not apply).
Properties[]
The interesting problems of channel systems arise when we ask decision problems about them.[2] Given a single-agent channel system and an initial configuration of state and channels, we have the following:
- Reachability: Can a state within a given set be reached?
- Inevitability: Do all maximally long simulations (i.e. running infinitely or until halting) visit a state in a given set? A special case is Termination, which asks whether all maximal simulations halt.
- Recurrent Reachability: Is there a simulation that visits a given state infinitely often?
- Boundedness: Can the channels become arbitrarily large?
If the "lossy" aspect of LCSs is removed, the system becomes Turing-complete, so by Rice's theorem all of the above questions are undecidable.
Surprisingly, with lossy channels, the first two problems do actually become decidable. Even more surprisingly, they are so difficult to solve in general that their complexity classes are googologically large! For \(\alpha \leq \varepsilon_0\), we define the class of functions \(\mathscr{F}_\alpha\) as
\[\mathscr{F}_\alpha = \bigcup_{c < \omega} \text{FDTIME}(f_\alpha^c(n))\]
and the complexity class \(\mathbf{F}_\alpha\) as
\[\mathbf{F}_\alpha = \bigcup_{p \in \mathscr{F}_{<\alpha}} \text{DTIME}(f_\alpha(p(n)))\]
where \(\mathscr{F}_{<\alpha}\) is a shorthand for \(\bigcup_{\beta < \alpha} \mathscr{F}_\alpha\). Here, \(f\) represents the fast-growing hierarchy. Chambart and Schoebelen showed that the problems of Reachability and Inevitability for LCSs are \(\mathbf{F}_{\omega^\omega}\)-complete.
Sources[]
See also[]
Bignum Bakeoff contestants: pete-3.c · pete-9.c · pete-8.c · harper.c · ioannis.c · chan-2.c · chan-3.c · pete-4.c · chan.c · pete-5.c · pete-6.c · pete-7.c · marxen.c · loader.c
Channel systems: lossy channel system · priority channel system
Concepts: Recursion