Process algebra needs proof methodology

It's widely appreciated that knowing that a distributed system or protocol behaves correctly is generally hard, and that process algebras provide useful formalisms for reasoning about these. Less appreciated is how hard it is to turn informal correctness proofs into formal proofs using process algebras.

Process algebra needs proof methodology (Fokkink, Groote & Reniers), an introductory article published a year ago in the Bulletin of the EATCS, provides a nice introduction to the problem of making process algebras more tractable for correctness reasoning, using Tanenbaum's sliding window protocol as a running example of a surprisingly hard-to-formalise proof.

Perhaps as interesting for LtU readers is that the article comes from the negelected "third" approach to process algebra (after CCS and CSP), namely the Algebra of Communicating Processes of Bergstra and Klop.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

BEATCS concurrency column & process algebra diary

It occurs to me that the Bulletin of the EATCS is not the most well-known publication, and its excellent concurrency column desrves to be more widely appreciated, particularly Luca Aceto's Some of My Favourite Results in Classic Process Algebra. Luca also has a process algebra diary.


I haven't seen the Favourite Results column before. Sure looks interesting.