操作扩展下方程的鲁棒性
计算机科学中的逻辑
2010-12-01 v1
摘要
在开放项上成立的可靠行为方程，在底层操作语义经过保守扩展后可能变得不可靠。提供方程得以保持的判据极为有用；特别是，它可以避免在扩展指定语言时重复证明。本文研究了开放项上几种互模拟概念下可靠方程的保持性：Robert de Simone提出的闭实例互模拟和形式假设互模拟，以及Arend Rensink提出的假设保持互模拟。对于形式假设互模拟和假设保持互模拟，我们证明了开放项上的任意可靠方程都能被所有不添加标号的不相交扩展所保持。我们还定义了形式假设互模拟和假设保持互模拟的轻微变体，使得所有可靠方程都能被任意不相交扩展所保持。最后，我们给出了两组句法判据（分别针对方程和操作扩展），并证明了每组判据都足以保持闭实例互模拟。
引用
@article{arxiv.1011.6435,
title = {Robustness of Equations Under Operational Extensions},
author = {Peter D. Mosses and MohammadReza Mousavi and Michel A. Reniers},
journal= {arXiv preprint arXiv:1011.6435},
year = {2010}
}
备注
In Proceedings EXPRESS'10, arXiv:1011.6012