Trapping Mutual Exclusion in the Box Calculus

Javier Esparza and Glenn Bruns

Abstract: The box calculus is a process algebra with a simple Petri net semantics. We show that it allows verification from process algebra and Petri nets to be combined. This is done by proving some properties of mutual exclusion algorithms.

LFCS report ECS-LFCS-94-295, July 1994.

Javier Esparza is now at the Department of Computer Science, Technische Universität München, where his email address is esparza@informatik.tu-muenchen.de.

Previous | Index | Next