Introduction to Modal and Temporal MuCalculi Julian Bradfield  University of Edinburgh (UK)
This talk will provide an introduction to the modal mucalculus and
related logics, suitable for those with some exposure to modal or
temporal logic, but without prior knowledge of fixpoint logics.
I start by reviewing the basic semantic setting of processes modelled as
transition systems, and briefly review basic modal logic and temporal
logics such as CTL.
I then introduce modal mucalculus, the result of adding fixpoint
operators to basic modal logic. I cover the formal syntax and semantics,
and then give more informally the gamebased intuition that is most
useful in understanding formulae of the logic.
I next describe global and local modelchecking techniques.
Finally, I will discuss the relationship between modal mucalculus,
automata and games, and some of the theoretical questions that have been
and are now of interest.
The talk is based on parts of the chapter, written with Colin Stirling,
'Modal logics and mucalculi: an introduction' in Handbook of
Process Algebra (ed. Bergstra, Ponse and Smolka), 293330, Elsevier,
2001. Types for Cryptographic Protocols Andrew D. Gordon  Microsoft Research, Cambridge (UK)
A standard approach to proving properties of a cryptographic security
protocol is to encode it within a process calculus, and then to apply
standard techniqes from concurrency theory such as modelchecking or
equational reasoning. A promising recent development is to verify
properties such as secrecy and authenticity via behavioural type
systems. This tutorial reviews the known type systems and results in
this area, and suggests areas for further research.


concur02@fi.muni.cz 