Introduction to Modal and Temporal Mu-Calculi Julian Bradfield - University of Edinburgh (UK)
This talk will provide an introduction to the modal mu-calculus 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 mu-calculus, the result of adding fixpoint
operators to basic modal logic. I cover the formal syntax and semantics,
and then give more informally the game-based intuition that is most
useful in understanding formulae of the logic.
I next describe global and local model-checking techniques.
Finally, I will discuss the relationship between modal mu-calculus,
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 mu-calculi: an introduction' in Handbook of
Process Algebra (ed. Bergstra, Ponse and Smolka), 293-330, 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 model-checking 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 |