Many real computer systems exhibit concurrrency, i.e. they consist of a number of components that work largely independently but also interact with each other. Such concurrent systems are difficult to design because concepts like causality, nondeterminism, synchronization, communication and timing constraints require an elaborate refined treatment which, in its complexity, can only be handled on a formal basis. This led to an intensive research into formal mehods for the specification, design, verification and analysis of concurrent systems. At the heart of these mehods are semantic models, tailored for the treatment of particular aspects of concurrent systems. We observe two directions in this research.

The investigation of semantic foundations of concurrent systems, which is characterized by emphasizing mathematically tractable semantic domains equipped with suitable operators for system composition. Often this poses mathematically interesting problems in domain theory. To solve them, concurrent systems are studied at a high level of abstraction. For example, uninterpreted action symbols rather than state transforming actions are considered.

The application of given semantic models to obtain logics, algorithms and calculi for the specification, verification and design of concurrent systems. Typically this work is driven by concrete case studies, which often reveal the need for changes or at least adaptations of the known abstract semantic models for concurrency.

The aim of the proposed Dagstuhl seminar was the discussion of semantic foundations of concurrent systems in the light of their applicability for the verification and design of concurrent systems. This concerned in particular the impact of the mathematical structures of the semantic domains on the compositionality of the various verification methods.

Particular topics of interest were:

• new developments in the semantics of concurrency,
• the relationship between different semantic models,
• semantic based approaches to the verification and design of concurrent systems,
• the suitability of specific semantic models for the task of reasoning about concurrent systems.

The programme of the seminar was intense and stimulating; it comprised 32 talks and one evening discussion on the impact of semantics. The abstracts of the talks are recorded in this report in the order of presentation.

The evening discussion reviewed visible achievements of semantics like the use of model checking and abstract interpretation, the design of functional and synchronous languages, the influence of Hoare's CSP on Ada and OCCAM, the clarification of various concepts concerning the computational process like interleaving versus partial order semantics, the use of types, fixed points and invariants. The renewed interest in logics and category theory was cited amongst the scientific impacts of semantics.

As new research areas for semantics the following were recommended: security, performance analysis, the integration of semantics with complexity, hardware design languages and hybrid systems.

Creative Commons BY 3.0 DE