首页> 外文期刊>Journal of logic and computation >Bisimulations for coalgebras on Stone spaces
【24h】

Bisimulations for coalgebras on Stone spaces

机译:Stone空间上的余数代数的双仿真

获取原文
获取原文并翻译 | 示例
       

摘要

We introduce and study bisimulations for coalgebras on Stone spaces (Kupke et al., 2004, Theoretical Computer Science, 327, 109-134), motivated by previous work on ultrafilter extensions for coalgebras (Kupke et al., 2005, Algebra and Coalgebra in Computer Science, 263-277), bisimulations for the Vietoris functor (Bezhanishvili et al., 2010, Journal of Logic and Computation, 20, 1017-1040) and building on an idea of Gorin and Schroder (2013, Algebra and Coalgebra in Computer Science, 8089, 253-266). We provide a condition under which our notion of bisimulation gives a sound and complete proof method for behavioural equivalence, and show that it generalizes Vietoris bisimulations. Our main technical result proves that the topological closure of any bisimulation between Stone coalgebras in our sense is still a bisimulation. This answers a question raised in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017-1040), and also leads to a simpler proof of the main theorem in that paper, that the topological closure of a Kripke bisimulation is a Vietoris bisimulation. As a second application of our general bisimulation concept, we study neighbourhood bisimulations on descriptive frames for monotone modal logic as they were introduced in Hansen et al. (2009, Logical Methods in Computer Science, 5, 1-38). From our general results we derive that these are sound and complete for behavioural equivalence and that the topological closure of a neighbourhood bisimulation is still a neighbourhood bisimulation, in analogy with the main result in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017-1040). Finally, we apply our result to bisimulations for Stone companions of set functors as defined in Kupke et al.
机译:我们引入和研究Stone空间上的余数代数(Kupke等人,2004,Theoretical Computer Science,327,109-134)的双仿真,这是受先前有关余数代数超滤子扩展的工作(Kupke等人,2005,Algebra和Coalgebra in 2005)的启发计算机科学(263-277),对Vietoris仿函数(Bezhanishvili等人,2010,逻辑与计算杂志,20,1017-1040)的双仿真,并基于Gorin和Schroder(2013,计算机中的代数和Coalgebra)的思想Science,8089,253-266)。我们提供了一个条件,在这个条件下,我们的双仿真概念为行为等效提供了完善而完整的证明方法,并表明它推广了Vietoris双仿真。我们的主要技术结果证明,在我们看来,Stone Coalgebras之间任何双模拟的拓扑关闭仍然是双模拟。这回答了Bezhanishvili等人提出的问题。 (2010,Journal of Logic and Computation,20,1017-1040),并且在该论文中还得到一个简单的主定理证明,即Kripke双仿真的拓扑闭合是Vietoris双仿真。作为我们的一般双仿真概念的第二个应用,我们研究了描述性框架上的邻域双仿真,用于单调模态逻辑,该方法已在Hansen等人中引入。 (2009,计算机科学中的逻辑方法,第5卷,第1-38页)。从我们的一般结果中,我们得出这些对于行为等效而言是合理且完整的,并且类似于Bezhanishvili等人的主要结果,邻域双仿真的拓扑关闭仍然是邻域双仿真。 (2010,逻辑与计算杂志,20,1017-1040)。最后,我们将结果应用于Kupke等人所定义的集合函子的Stone伴随的双仿真。

著录项

  • 来源
    《Journal of logic and computation》 |2018年第6期|991-1010|共20页
  • 作者单位

    Stockholm Univ, Dept Philosophy, Univ Vagen 10 D, Stockholm, Sweden;

    Univ Amsterdam, Computat Sci Lab, Sci Pk 904, NL-1098 XH Amsterdam, Netherlands;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号