PROJECT OVERVIEW

Algebraic process calculi (also known as "process algebras") like Milner's Calculus of Communicating Systems and Hoare's Communicating Sequential Processes are prototype specification languages for reactive systems---that is, for devices that compute by reacting to stimuli from their environment. Examples of reactive systems are operating systems, communication protocols, control programs and embedded system devices like mobile telephones.

Since process algebras may be used for the description of both actual systems and their specifications, an important component of their theory is a notion of equivalence or approximation between process terms. One term may describe an implementation, while another may stand for the specification of the behaviour to be achieved; to say that these terms are equivalent means that they describe essentially the same behaviour, albeit at different levels of abstraction or refinement. The verification of the correctness of a concurrent system described as a term in a process algebra can thus be formally phrased as an "equivalence checking problem".

One of the natural outcomes of the algebraic structure of process description languages is that we can formulate general equivalences between process terms that we expect to hold with respect to the chosen notion of behavioral semantics in terms of equations. Several natural questions immediately arise pertaining to the (non-)existence of (finite) collections of laws that allow us to prove by "substituting equals for equals" all of the valid equalities between process descriptions over fragments of process algebras. A collection of laws with the above property is called a complete axiomatization of the algebra under study.

A complete axiomatization of a behavioural equivalence yields a purely syntactic characterization, independent of the chosen model of reactive systems and of the details of the definition of the chosen behavioural equivalence, of the semantics of the process algebra. This bridge between syntax and semantics plays an important role in both the practice and the theory of process algebras. From the point of view of practice, these proof systems can be used to perform system verifications in a purely syntactic way using general purpose theorem provers or proof checkers like Coq or PVS, and form the basis of purpose built axiomatic verification tools like PAM. From the theoretical point of view, complete axiomatizations of behavioural equivalences capture the essence of different notions of semantics for processes in terms of a basic collection of identities, and this often allows one to compare semantics which may have been defined in very different styles and frameworks. Complete axiomatizations therefore serve a fundamental, unifying and clarifying purpose.

In this project, we study some challenging open axiomatization problems in the theory of concurrent processes. The main purpose of the proposed work is to obtain a fuller understanding of the expressive power of equational logic in the characterization of behavioural equivalences by attempting to settle some long-standing open problems in the field relative to the axiomatization of process algebras with operators that---like parallel composition, iteration, priority and mode transfer operators (such as interrupt and disrupt), among others---are very useful in the description of key aspects of reactive computation. Apart from the intrinsic scientific interest of this work---that will lead to an improved understanding of the power of the classic logic of equations in describing and reasoning about a ubiquitous class of computing systems---, this project will also foster the development of research activities in Iceland that combine Computer Science and classic fields of Mathematics and Logic like universal algebra, model theory, proof theory and equational logic.