基于 C2KA 的通信潜力条件形式化

保护通信代理系统免受隐蔽信道通信侵害的一个关键环节，是能够识别给定系统中何时可能存在隐蔽信道，以及哪些代理比其他代理更容易产生隐蔽信道。在本文中，我们提出了隐蔽信道存在的一个必要条件——通信潜力条件（potential for communication condition）的形式化描述。随后，我们讨论了在潜在通信路径中修改系统代理后，通信潜力何时得以保持。我们的方法基于通信并发 Kleene 代数（Communicating Concurrent Kleene Algebra, C2KA）的数学框架。现有方法仅考虑通过共享环境进行的通信潜力，而本文提出的方法还考虑了通过外部刺激进行的通信潜力。