有损信道系统

消息可以消失，却不能凭空插入、复制或重新排序。这个错误模型扩大了系统可能行为：可靠执行仍然允许，但还要考虑所有丢失模式。一个协议在此模型下安全，才经受了任意丢包的考验。

丢失会使某些任务更难完成，却让某些验证问题更容易决定，因为它允许大队列先删成小队列，再模仿小队列的动作。

接收队首和删除中间消息不同 ​

假设控制边要求接收 $b$。可靠队列 ab 的队首为 $a$，因此不能执行；有损语义可以先删除 $a$，留下 b，然后接收成功，队列变空。

对队列 abac，一次丢失可得到 ac、bac 或空串，但不能得到 ca，因为顺序不允许改变，也不能得到 aaac，因为不能复制消息。

子词顺序怎样给单调性 ​

规定两个配置可比时控制状态相同，且各信道逐项满足子词关系。Higman 引理公理库Higman 引理Higman lemma把良拟序从字母提升到有限字符串的子词嵌入，给出最小坏序列机制并区分子序列、子串和前缀。保证有限字母表字串是 wqo，有限乘积和有限控制并合后仍为 wqo。

若小队列配置 $s$ 能执行一步，而 $s⪯t$，大队列 $t$ 可以先删去额外消息得到 $s$，再复制其前置丢失、可靠操作和后置丢失，甚至到达与 $s$ 完全相同的后继。因此它在上述子词顺序下构成强兼容的良结构转移系统公理库良结构迁移系统Well structured transition system · WSTS把良拟序与迁移兼容性分开验证，以普通 Petri 网和零测试说明何时能安全地用大状态模拟小状态。。

可靠 FIFO 系统没有这项模拟能力：小队列 b 能接收 $b$，更大的 ab 虽包含它为子词，却被队首 $a$ 阻塞。这说明可判定性变化来自丢失语义与顺序的配合，不只是信道长度无界。

控制状态错误如何变成覆盖 ​

设错误控制状态为 $q_{\mathrm{b}\mathrm{a}\mathrm{d}}$。所有信道均为空的配置 $(q_{\mathrm{b}\mathrm{a}\mathrm{d}},\epsilon ,\dots ,\epsilon )$ 的向上闭包，恰为所有处于错误控制状态的配置。因此控制状态可达性是一个覆盖问题。

给定有限基，可按有限条发送、接收规则计算最小前驱；再调用 后向覆盖算法公理库覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。。例如接收 $a$ 后至少保留子词 $v$，所需最小输入队列为 $av$；发送 $a$ 的前驱则要区分目标子词是否使用了新加的最后一个 $a$，两种情况取有限并再最小化。

有限控制有损信道的覆盖/控制状态可达性可判定，但最坏复杂度极高。不能由 Higman 引理直接推出多项式甚至初等复杂度，也不能把同一结论转给可靠无界 FIFO 通信系统。[1,2]

本模型不承诺每条消息最终送达。若所有重传都可以丢失，协议可能永远收不到确认；证明活性需要另给公平性、限制丢失或概率模型。给丢包概率并问“几乎必然完成”，已经是在研究概率信道系统，不是本页的非确定语义。