• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Propositional dynamic logics for communicating concurrent programs with CCS's parallel operator
【24h】

Propositional dynamic logics for communicating concurrent programs with CCS's parallel operator

机译：用于与CCS并行运算符通信并发程序的命题动态逻辑

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

摘要

This work presents three increasingly expressive Dynamic Logics in which the programs are described in a language based on CCS. Our goal is to build dynamic logics that are suitable for the description and verification of properties of communicating concurrent systems, in a similar way as PDL is used for the sequential case. In order to accomplish that, CCS's operators and constructions are added to a basic modal logic. Doing this, the semantics of CCS's parallel operator allows us to build dynamic logics that support communicating and concurrent programs. We build a simple Kripke semantics for these logics, provide complete axiomatizations for them and show that they have the finite model property. This contrasts with other dynamic logics with parallel operators presented in the literature, such as Peleg's Concurrent PDL with Channels, where either the parallel programs cannot communicate, or at least one of the properties mentioned above (simple Kripke semantics, complete axiomatization and finite model property) is missing.
机译：这项工作提出了三种表现力越来越强的动态逻辑，其中以基于CCS的语言描述了程序。我们的目标是构建动态逻辑，该逻辑适合于描述和验证并发通信系统的属性，就像在顺序情况下使用PDL一样。为此，将CCS的运算符和构造添加到基本模态逻辑中。为此，CCS并行运算符的语义使我们能够构建支持通信程序和并发程序的动态逻辑。我们为这些逻辑构建了一个简单的Kripke语义，为它们提供了完整的公理化并显示了它们具有有限的模型属性。这与文献中提出的带有并行运算符的其他动态逻辑形成了鲜明对比，例如带有通道的Peleg的并行PDL，其中并行程序无法通信，或者至少具有上述属性之一（简单的Kripke语义，完整的公理化和有限的模型属性） ） 不见了。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号