首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:Robustness of Equations Under Operational Extensions
  • 本地全文:下载
  • 作者:Peter D. Mosses ; MohammadReza Mousavi ; Michel A. Reniers
  • 期刊名称:Electronic Proceedings in Theoretical Computer Science
  • 电子版ISSN:2075-2180
  • 出版年度:2010
  • 卷号:41
  • 页码:106-120
  • DOI:10.4204/EPTCS.41.8
  • 出版社:Open Publishing Association
  • 摘要:Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language.

    This paper investigates preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of them to be sufficient for preserving ci-bisimilarity.

国家哲学社会科学文献中心版权所有