Modeling Process Calculi with PVS

AbstractIn this work we show how process calculi can be embedded into the general-purpose verification system PVS. We make use of PVS's higher order predicate logic to define the abstract co-data type “process” as a terminal coalgebra of the finite power-set functor ℘fin(−)A. In this context we are able to define the (strong) bisimulation in different ways and to prove the equivalence of these definitions. Moreover, coinduction is used as an approach for the definition of process combinators and for the verification of their properties.Other calculi can be integrated in PVS or a like prove-assistant in similar way too