CSP Semantics over Restriction Spaces

Benoît Ballenghien 📧 and Burkhart Wolff 📧

May 7, 2025

Abstract

We use the Restriction_Spaces library as a semantic foundation for the process algebra framework HOL-CSP, offering a complementary backend to the existing HOLCF infrastructure. The type of processes is instantiated as a restriction space, and we prove that it is complete in this setting. This enables the construction of fixed points for recursive process definitions without having to rely exclusively on a pointed complete partial order. Notably, some operators are constructive without being Scott-continuous, and vice versa, illustrating the genuine complementarity between the two approaches. We also show that key CSP operators are either constructive or non-destructive, and verify the admissibility of several predicates, thereby supporting automated reasoning over recursive specifications.

License

BSD License

Topics

Session HOL-CSP_RS