University of Leicester


Language theory for concurrent systems

Associated Researchers: Dr. Kuske

The classical theory of formal languages investigates the sequential behaviour of a system and describes it mathematically by means of algebraic or logical methods. This formal description is the basis for an automatic verification of systems. In the meanwhile, the interest has been shifted from sequential to distributed systems. These distributed systems consist of interacting sequential subsystems that work concurrently. We aim at an extension of the deep results from the theory of formal languages in such a way that the new aspects of concurrent behaviors are reflected. This can lead to a considerable speed-up of the verification of concurrent systems as proved, e.g., by the verification tool SPIN.

A typical example is the generalization of the theory of recognizable languages to Mazurkiewicz-traces in the last 15 years. The results in this field are paradigmatic for further developments: The first being the investigation of idealized systems whose computations are described by partially ordered sets. The second line of research is the attempt to model the behaviour of a system as elements of generalized trace monoids to enable the investigation of more involved features.

© University of Leicester 15th December 2000. Last modified: 8th January 2004, 14:32:05.
Informatics Web Maintainer. This document has been approved by the Head of Department.