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 systemsthat 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 longstanding
open problems in the field relative to the axiomatization of process
algebras with operators thatlike parallel composition, iteration,
priority and mode transfer operators (such as interrupt and disrupt),
among othersare very useful in the description of key aspects of
reactive computation. Apart from the intrinsic scientific interest of
this workthat 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.
