使用同品种器械公理化GSOS
Axiomatizing GSOS with Predicates
摘要：
在本文中，我们介绍了一个扩展的GSOS规则格式的谓词，如终止，收敛和发散。对于这种格式，我们推广了Aceto，Bloom和Vaandrager提出的技术，用于自动生成GSOS系统的双相似性的地面完整公理化。我们的程序是在一个工具，接收SOS规范作为输入，并自动导出相应的公理化。这为通过定理证明技术检查过程项的强双相似性铺平了道路。
英文摘要：
In this paper, we introduce an extension of the GSOS rule format with predicates such as termination, convergence and divergence. For this format we generalize the technique proposed by Aceto, Bloom and Vaandrager for the automatic generation of ground-complete axiomatizations of bisimilarity over GSOS systems. Our procedure is implemented in a tool that receives SOS specifications as input and derives the corresponding axiomatizations automatically. This paves the way to checking strong bisimilarity over process terms by means of theorem-proving techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
