Institutional Repository
| connection between logical and algebraic approaches to concurrent systems | |
| Zhan Naijun | |
| 2010 | |
| Conference Name | 6th International Conference on Theory and Application of Models of Computation (TAMC 09) |
| Source | Mathematical Structures in Computer Science |
| Pages | 915-950 |
| Conference Date | MAY 18-22, |
| Conference Place | Changsha, PEOPLES R CHINA |
| Publish Place | 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA |
| Publisher | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
| ISSN | 0960-1295 |
| Department | Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China. |
| English Abstract | 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. |
| Keyword | Calculations Mathematical Operators Semantics Temporal Logic |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/8702 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Zhan Naijun. connection between logical and algebraic approaches to concurrent systems[C]. 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA:MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE,2010:915-950. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment