Back to Summer 2010 Seminars Index

Research Seminars
Summer 2010

Tools for CSP

Markus Roggenbach (University of Wales)
19 May, 2:00pm in CS103, hosted by Jeremy Jacob

Children & Candy Puzzle: ``There are k children sitting in a circle. In the beginning, each child holds an even number of candies. The following step is repeated indefinitely: Every child passes half of her candies to the child on her left; any child who is left with an odd number of candies is given another candy from the teacher. Claim: Eventually, all children will hold the same number of candies.''

Taking the above described ``Children & Candy Puzzle'' as a starting point, we discuss how to model it in the process algebra CSP and how to prove its claim using standard CSP tools for simulation (ProBe), model checking (FDR), and theorem proving (CSP-Prover). Besides the power to analyze a single system, the theorem proving approach offers the possibility for deeper reflections on CSP. Here we discuss how it allows one to verify the algebraic laws of the language, and, furthermore, how it allows to prove meta results such as the completeness of axiomatic semantics.