• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Programming languages and systems >Towards a General Theory of Barbs,Contexts and Labels
【24h】

Towards a General Theory of Barbs,Contexts and Labels

机译：迈向倒钩，语境和标签的通论

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Barbed bisimilarity is a widely-used behavioural equivalence for interactive systems: given a set of predicates (denoted "barbs", and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility, this definition of equivalence is unsatisfactory, since often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified. Should a labelled operational semantics be available for our system, more efficient observational equivalences might be adopted. To this end, a series of techniques have been proposed to derive labelled transition systems (LTSs) from unlabelled ones, the main example being Leifer and Milner's reactive systems. The underlying intuition is that labels are the "minimal" contexts that allow for a reduction to be performed. We introduce a framework that characterizes (weak) barbed bisimilarity via transition systems whose labels are (possibly minimal) contexts. Differently from other proposals, our theory is not dependent on the way LTSs are built, and it relies on a simple set-theoretical presentation. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of mobile ambients and HoCore, recasting the (weak) barbed bisimilarities of these calculi via label-based behavioural equivalences.
机译：倒钩双相似性是交互式系统广泛使用的行为对等物：给定一组谓词（表示为“倒钩”，并表示对状态的基本观察）和一组上下文（代表可能的执行环境），则认为两个系统是如果它们在插入任何选定的上下文中时验证相同的倒钩，则等效。尽管具有灵活性，但对等价的定义并不令人满意，因为量化常常是在无限的上下文中进行的，因此很难验证带倒钩的双相似性。如果标记的操作语义可用于我们的系统，则可以采用更有效的观察等效项。为此，已经提出了一系列技术来从未标记的过渡系统衍生出标记的过渡系统（LTS），主要的例子是莱弗和米尔纳的反应系统。基本的直觉是标签是允许执行缩减的“最小”上下文。我们介绍了一个框架，该框架通过标签为（可能是最小的）上下文的过渡系统来表征（弱）倒钩双相似性。与其他建议不同，我们的理论不依赖于LTS的构建方式，而是依赖于简单的集合论表示。为了为我们的形式主义提供一个测试平台，我们通过解决移动环境和HoCore的语义来实例化它，并通过基于标签的行为等效来重铸这些计算的（弱）带刺的双相似性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号