Process Algebra in Pvs

The aim of this work is to investigate mechanical support for process algebra, both for concrete appli-cations and theoretical properties. Two approaches are presented using the verification system PVS. One approach declares process terms as an uninterpreted type and specifies equality on tenns by axioms. This is convenient for concrete applications where the rewrite mechanisms of PVS can be exploited. For the verification of theoretical results, often induction principles are needed. They are provided by the second approach where process tenns are defined as an abstract datatype with a separate equivalence relation.