带谓词的GSOS公理化
计算机科学中的逻辑
2011-08-17 v1
摘要
本文介绍了GSOS规则格式的一种扩展，该扩展包含诸如终止、收敛和发散等谓词。针对这种格式，我们推广了Aceto、Bloom和Vaandrager提出的技术，用于在GSOS系统上自动生成双相似性的基完备公理化。我们的过程已在一个工具中实现，该工具接收SOS规范作为输入，并自动推导出相应的公理化。这为通过定理证明技术检查进程项上的强双相似性铺平了道路。
引用
@article{arxiv.1108.3124,
title = {Axiomatizing GSOS with Predicates},
author = {Luca Aceto and Georgiana Caltais and Eugen-Ioan Goriac and Anna Ingolfsdottir},
journal= {arXiv preprint arXiv:1108.3124},
year = {2011}
}
备注
In Proceedings SOS 2011, arXiv:1108.2796