A Logic-Functional Approach to the Execution of CCS Specifications Modulo Behavioural Equivalences

This paper reports on a work that proposes a kernel for an execution environment for the operational semantics and the behavioural equivalences of CCS. The proposed execution environment distinguishes itself by being formal, by dealing with the behavioural equivalences as schemes of axioms, differently from other approaches based on automata, and by giving the possibility to define several strategies of verification in a modular and flexible way. The environment, obtained by techniques of logic-functional programming, treats basic CCS with bounded recursion. A particular strategy of verification is presented.