Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow us to obtain sound and complete characterizations of (at least some of) these combined inductive/coinductive properties of binary session types. In particular, we illustrate the role of corules in characterizing fair termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and fair subtyping, a liveness-preserving refinement relation for session types. The characterizations we obtain are simpler compared to the previously available ones and corules provide insight on the liveness properties being ensured or preserved. Moreover, we can conveniently appeal to the bounded coinduction principle to prove the completeness of the provided characterizations.

翻译：通信协议的许多特性结合了安全和活性两个方面。由于通常在界定和证明这些特性时通常采用截然不同的技术(分别是上岗和上岗),因此很难通过单一的推理系统来说明这种合并特性。在本文中,我们表明通用推理系统使我们能够对这些二会话类型(至少部分)的感应/诱导性综合特性进行健全和完整的定性。我们特别说明了共同规则在下列方面的作用:公平终止(总是能够最终终止的协议财产)的定性、公平遵守(始终可以扩展以达到客户满意程度的相互作用财产)和公平分级法、对会话类型保持活性改进关系。我们获得的定性比以前已有的特征和共同规则更简单,有助于深入了解正在确保或保存的活性特性。此外,我们可以方便地呼吁受约束的硬币原则,以证明所提供的定性的完整性。