Algorithm and Information Colloquium (AIC)

Title: Connection between Logical Approach and Algebraical Approach to Concurrent Systems

Speaker: Naijun Zhan

Time: 16:30 – 17:30, April 21, 2010, Wednesday

Place: Lecture Room, Level 3, Building No. 5, Institute of Software

Tea time:　16:00 – 16:30, Common Room, Level 3, Building No. 5

Abstract:

Logical approach and algebraical approach are thought as two of dominant methodologies for development of concurrent and reactive systems. In general speaking, logical approach is more abstract, but lacks compositionality; in contrast, algebraic approach inherently owns compositionality, but lacks abstractness. How to relate the two approaches is a challenge in computer science. There are lots of efforts that have been done towards attacking such issue.  In this paper, we further investigate this issue and obtain the following results: Firstly, we prove that the non-deterministic operator in process algebra can be defined in modal and temporal logics (e.g. the $\mu$-calculus and the Fixpoint Logic with Chop) w.r.t. the observational semantics. Thus, we can apply logical approach to design a complex system in a compositional way; Secondly, we give a uniform approach to constructing the characteristic formulae of a context-free process up to some behaviour preorders. So,  all reductions concerning processes that are usually done in an algebraical framework can be done in a logical framework.
 
As Basic Process Algebra (BPA) plays the core of most process algebras and Fixpoint Logic with Chop is very powerful modal logic into which most well-known modal and temporal logics can be encoded, all the above investigations are done within BPA and FLC.

Biography:

Dr. Naijun Zhan is a professor of State Key Lab. of Computer Science. He did his phd in theoretical computer science from Institute of Software, Chinese Academy of Sciense in 2000. After that, he worked at Faculty of Mathematics and Informatics, Univeristy of Mannheim, Germany, as a reserach assistant till June, 2004. His current research interests cover formal semantics, design and verification calculi of concurrent and reactive  systems, program verification, modal and temporal logics, real-time and hybrid systems, component-based methods and so on.