PROJECT OVERVIEW

Algebraic process theories, also known as process algebras, are prototype specification languages for reactive systems---that is, for devices that compute by reacting to stimuli from their environment. The main strength of such theories lies in the equational (calculational) style of reasoning they support. For each process theory, several natural questions immediately arise pertaining to the (non-)existence of (finite or recursive) sets of laws that allow one to prove by "substituting equals for equals" all of the valid equalities between process descriptions (closed or open terms) over fragments of the process theory at hand.

Currently, answering such questions is only possible via delicate, error-prone and lengthy proofs. This project aims at establishing a generic framework for answering such questions efficiently and at applying the proposed general theory to solve some of the main open problems in the study of the equational logic of processes.