Colloquium Speaker

Speaker:Martti Tienari
Department of Computer Science
University Of Helsinki, Finland
Topic:Behavioral Equivalences in the Verification of Concurrent Systems
Date:Thursday, November 16, 2000
Time:11:00 AM
Place:Gould-Simpson, Room 701


Refreshments will be served in the 7th-floor lobby of Gould-Simpson at 10:45 AM


ABSTRACT


Labeled transition systems form an established formal model of concurrent systems. Many formal specification languages (e.g. CSP, CCS, and LOTOS) can be provided with semantics expressed in terms of transition systems. Behavioural equivalences between transition systems can be used widely in the verification of concurrent systems.

The lecture gives an introduction to process equivalence concepts and shows with application examples their utility in the verification of some simple class-room size examples of concurrency. Recent research results at the University of Helsinki achieved in this area are surveyed.