题名:  connection between logical and algebraic approaches to concurrent systems 
作者:  Zhan Naijun

会议文集:  Mathematical Structures in Computer Science

会议名称:  6th International Conference on Theory and Application of Models of Computation (TAMC 09)

会议日期:  MAY 1822,

出版日期:  2010

会议地点:  Changsha, PEOPLES R CHINA

关键词:  Calculations
; Mathematical operators
; Semantics
; Temporal logic

出版者:  MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

出版地:  32 AVENUE OF THE AMERICAS, NEW YORK, NY 100132473 USA

ISSN:  09601295

部门归属:  Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China.

英文摘要:  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 nondeterministic operator of process algebra can be defined in modal and temporal logics (such as the mucalculus 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 contextfree 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. 
内容类型:  会议论文

URI标识:  http://ir.iscas.ac.cn/handle/311060/8702

Appears in Collections:  计算机科学国家重点实验室 _会议论文

There are no files associated with this item.

Recommended Citation: 
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 1822,.


