具有协同规则的推理系统用于二进制会话类型的安全性和活性属性
摘要：通信协议的许多属性将安全性和活性方面结合起来。通过单个推理系统对这些组合的属性进行表征是困难的，因为它们在定义和证明中通常涉及到根本不同的技术（分别是协同归纳和归纳）。在本文中，我们展示了广义推理系统可以让我们获取二进制会话类型中这些组合内部的归纳/协同归纳属性（至少其中一些）的准确而完整的表征。特别地，我们说明了结合规则在表征公平终止（协议总能最终终止的属性）、公平符合（交互总是可以扩展以达到客户满意的属性）和公平子类型关系（会话类型的活性保持细化关系）中的作用。我们得到的表征相比以前可用的表征更简单，而规则则提供了对所确保或保存的活性属性的洞察。此外，我们可以方便地通过有界协同归纳原理来证明提供的表征的完备性。
作者：Luca Ciccone, Luca Padovani
论文ID：2108.01503
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22