• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Concurrency Theory(CONCUR 2004); 20040831-20040903; London; GB >Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency
【24h】

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

机译：消除并发空间逻辑中的量词和不确定性

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

摘要

Aiming at a deeper understanding of the essence of spatial logics for concurrency, we study a minimal spatial logic without quantifiers or any operators talking about names. The logic just includes the basic spatial operators void, composition and its adjunct, and the next step modality; for the model we consider a tiny fragment of CCS. We show that this core logic can already encode its own extension with quantifiers, and modalities for actions. Prom this result, we derive several consequences. Firstly, we establish the intensionality of the logic, we characterize the equivalence it induces on processes, and we derive characteristic formulas. Secondly, we show that, unlike in static spatial logics, the composition adjunct adds to the expressiveness of the logic, so that adjunct elimination is not possible for dynamic spatial logics, even quantifier-free. Finally, we prove that both model-checking and satisfiability problems are undecidable in our logic. We also conclude that our results extend to other calculi, namely the π-calculus and the ambient calculus.
机译：为了更深入地了解并发空间逻辑的本质，我们研究了一种最小的空间逻辑，无需量词或任何运算符都在谈论名称。逻辑仅包括基本的空间运算符void，组成及其辅助，以及下一步模态。对于模型，我们考虑CCS的微小片段。我们证明了这种核心逻辑已经可以使用量词和操作方式对自己的扩展进行编码。证明这个结果，我们会得出一些后果。首先，我们建立逻辑的内涵，描述它在过程中引起的等价，并推导特征公式。其次，我们表明，与静态空间逻辑不同，合成辅助功能增加了逻辑的表达能力，因此动态空间逻辑甚至无量词的辅助功能消除都是不可能的。最后，我们证明模型检查和可满足性问题在我们的逻辑中都是无法确定的。我们还得出结论，我们的结果扩展到其他演算，即π演算和环境演算。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号