Process Algebra and Equivalences
Process algebras are formalisms for modeling the behavior of systems. Process algebraic techniques and algorithms can be used to show that two (models of) systems are related in some precisely defined way, e.g., that one of them can simulate the other. This can be useful in showing that one system is an implementation or a refinement of another. This ability to apply automatic or manual techniques for demonstrating the relation between pairs of systems can be used during a stepwise refinement software development process. According to this approach, the development starts with the specification, and gradually refines it into actual code, where in each stage the correctness is preserved by enforcing some equivalence relation. Refinement also allows describing a system in a hierarchical way, where each rank in the hierarchy is equivalent to the previous one in a formally defined way.
KeywordsCritical Section Process Algebra Simulation Relation Agent Variable Proof Rule
Unable to display preview. Download preview PDF.
- R. Milner, Communication and Concurrency, Prentice-Hall, 1995.Google Scholar
- R. Milner, Communicating and Mobile Systems: the ir-calculus, Cambridge University Press, 1999.Google Scholar
- R. Lai, A. Jirachiefpattana, Communication Protocol Specification and Verification, Kluwer Academic Publishers, 1998.Google Scholar
- J. C. M. Baeten, ed., Applications of Process Algebra Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1991.Google Scholar
- G. Bruns, Distributed System Analysis with CCS, Prentice-Hall, 1996.Google Scholar
- M. Hennessy, Algebraic Theory of Processes, MIT Press, 1988.Google Scholar
- R. J. van Glabbeek, The Linear Time-Branching Time Spectrum (Extended Abstract), CONCUR 1990, Theories of Concurrency, Amsterdam, The Netherlands, Lecture Notes in Computer Science 458, Springer-Verlag, 1990, 278–297.Google Scholar
- R. J. van Glabbeek, The Linear Time—Branching Time Spectrum II, E. Best (ed.), 4th international conference on Concurrency theory, CONCUR 1993, Lecture Notes in Computer Science 715, Springer-Verlag, Hildesheim, Germany, 66–81.Google Scholar