connection between logical and algebraic approaches to concurrent systems
文献类型：会议论文
| 作者 | Zhan Naijun |
| 出版日期 | 2010 |
| 会议名称 | 6th International Conference on Theory and Application of Models of Computation (TAMC 09) |
| 会议日期 | MAY 18-22, |
| 会议地点 | Changsha, PEOPLES R CHINA |
| 关键词 | Calculations Mathematical operators Semantics Temporal logic |
| 页码 | 915-950 |
| 英文摘要 | The logical and algebraic approaches are regarded as two of the dominant methodologies for the development of reactive and concurrent systems. It is well known that the logic approach is more abstract, but lacks compositionality; while the algebraic approach is inherently compositional, but lacks abstractness. However, connecting the two approaches is a major challenge in computer science, and many efforts have been directed to resolving the problem. Linking the algebraic approach to the logical approach has been satisfactorily resolved through the notion of characteristic formulae. But very limited success has been achieved so far in the other direction, as most of the established results have been developed only with respect to a simple semantics, which has usually been strong bisimulation. However, in practice, an observational semantics like weak bisimulation, which is much more complicated, is thought to be more useful. In this paper, we investigate how to connect the logical and algebraic approaches with respect to the observational preorder, which is a generalisation of weak bisimulation that takes divergence into account. We show the following results. First, we prove that the non-deterministic operator of process algebra can be defined in modal and temporal logics (such as the mu-calculus and the Fixpoint Logic with Chop) with respect to the observational preorder (in fact, the kernel of its precongruence). In this way, we can apply the logical approach to the design of a complex system in a compositional way. Second, we present two algorithms for constructing the characteristic formulae for a context-free process up to the preorder and its precongruence, respectively. The effect of this is that all the reductions for processes that are usually done in an algebraic setting can be handled in a logical setting. |
| 会议录 | Mathematical Structures in Computer Science
 |
| 会议录出版者 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
| 会议录出版地 | 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA |
| ISSN号 | 0960-1295 |
| 源URL | [http://124.16.136.157/handle/311060/8702]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _会议论文 |
| 推荐引用方式 GB/T 7714 | Zhan Naijun. connection between logical and algebraic approaches to concurrent systems[C]. 见:6th International Conference on Theory and Application of Models of Computation (TAMC 09). Changsha, PEOPLES R CHINA. MAY 18-22,. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。