全可逆性的安全性与活性理论（扩展摘要）
计算机科学中的逻辑
2016-08-01 v2
摘要
我们研究一种可逆演算中的安全性与活性理论，其中归约全序排列且回滚将系统引导至过去状态。与先前关于通信事务的工作类似，活性与安全性分别对应于 should-testing 和 inverse may-testing 预序。我们在可逆演算中为这些预序开发了完全抽象模型，这些模型仅基于前向迁移，从而为此类系统的精化提供了简单的证明技术。我们表明，在安全性方面，全可逆性是 CCS 的保守扩展。然而在活性方面，向 CCS 添加全可逆性可区分更多系统。据我们所知，该工作提供了安全性和活性的首个刻画，以及首个用于可逆演算的测试理论。
引用
@article{arxiv.1604.05555,
title = {A Safety and Liveness Theory for Total Reversibility (Extended Abstract)},
author = {Claudio Antares Mezzina and Vasileios Koutavas},
journal= {arXiv preprint arXiv:1604.05555},
year = {2016}
}