Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Proof search specifications of bisimulation and modal logics for the &pgr;-calculus
Tiu A., Miller D. ACM Transactions on Computational Logic11 (2):1-35,2010.Type:Article
Date Reviewed: May 17 2010

In a small but vibrant corner of the computer science world, theoreticians continue an elegant and subtle program to try to elucidate the meaning of computation. Milner, Parrow, and Walker’s &pgr;-calculus [1] has advocated a particular approach, where communication is at the heart of the matter. This view now has applications in areas as far apart as security and biology. Logicians have risen to the challenge of providing a formal foundation and have expanded on basic notions of metalogics and embeddings, based on the use of &lgr;-abstractions.

Many presentations of this kind of work can be extremely dense and difficult for anyone except those heavily involved with the subject. This paper, on the other hand, is very well written and its length allows the concepts to be explained very clearly and intuitively.

With some previous understanding of logical foundations in computing in place, the build-up to the logic FO&lgr;&Dgr;∇ (pronounced fold-nabla) is natural and well articulated. It explores the notion of encoding an object-level abstraction into a metalevel abstraction, and scopes issues within the sequent notation. The ∇ quantifier is introduced in Section 2, in order to capture the notion of a local signature useful in modeling names in &pgr;-calculus. The logic FO&lgr;&Dgr;∇ itself is placed in a more rigorous setting in Section 3. Section 4 introduces a more formal relation with &pgr;-calculus, starting with the finite version of the calculus. Tiu and Miller explain the encoding in easy terms and discuss the examples.

Readers who have some previous understanding of bisimulation will find it easy to follow the intuitive exposition in Section 5 of variant concepts of equivalence supported by open, late, and early bisimulation. The definitions are compared with earlier work by Sangiorgi and Walker [2], in a way that delineates the importance of choosing an appropriate style of embedding. The situation gets more complicated in Section 6, where there is not only the specification of processes in &pgr;-calculus and the embedding in FO&lgr;&Dgr;∇, but also a description of the behavior in modal logic that is translated to &lgr;-tree syntax. Further complications arise in Section 7, where nonterminating processes are introduced. But the clear style of writing continues, including a long example, so this technically challenging section is still accessible. The authors change gears in Section 8, which discusses proof search issues. This section covers a lot of ground, but in a more cursory manner. The concluding sections are short, consisting mostly of ideas for further work.

Overall, this is a detailed paper with many results that will be of interest to specialists in the areas of process algebras and abstract syntax. It may also be of interest to the nonspecialist, as a clear exposition of the techniques used in this very rich area of research.

Reviewer:  Sara Kalvala Review #: CR138004 (1010-1040)
1) Milner, R.; Parrow, J.; Walker, D. A calculus of mobile processes--Part 1 and Part 2. Information and Computation 100, (1992), 1–77.
2) Sangiorgi, D.; Walker, D. &pgr;-calculus: a theory of mobile processes. Cambridge University Press, Cambridge, MA, 2001.
Bookmark and Share
  Featured Reviewer  
 
Specification Techniques (F.3.1 ... )
 
 
Proof Theory (F.4.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Specification Techniques": Date
Compatibility problems in the development of algebraic module specifications
Ehrig H., Fey W., Hansen H., Löwe M., Jacobs D., Parisi-Presicce F. Theoretical Computer Science 77(1-2): 27-71, 1990. Type: Article
Oct 1 1991
Transformations of sequential specifications into concurrent specifications by synchronization guards
Janicki R., Müldner T. Theoretical Computer Science 77(1-2): 97-129, 1990. Type: Article
Jul 1 1991
Regularity of relations
Jaoua A., Mili A., Boudriga N., Durieux J. Theoretical Computer Science 79(2): 323-339, 1991. Type: Article
Apr 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy