The modal mu-calculus offers a rich logic for expressing temporal
properties of processes, and much effort has gone into developing
techniques for automatically model-checking such properties of
finite state processes. However, general processes (for example
arbitrary CCS processes) are not finite state, and the
problem of checking whether a process (expressed in a process
algebra) satisfies a formula is undecidable.
In the face of undecidability, one seeks formal systems that are
sound for establishing properties of processes. Although necessarily
incomplete, one would like to find systems that provide perspicuous
reasoning methods which suffice in practice. Much of the talk will be
devoted to presenting a sequent calculus, strongly based on a system
proposed by Mads Dam and Dilian Gurov, that I believe satisfies
these requirements. The crucial idea, due to Dam and Gurov, is to
introduce explicit mu-calculus approximants into the proof system,
allowing induction and coinduction arguments to be subsumed by
a global combinatorial condition on proofs.
It is an interesting question to what extent the methods
provided by the proof system do suffice in practice. One way
of addressing this is to obtain restricted completeness results,
showing completeness in special cases where such results are at least
possible in theory. I shall conclude by discussing a new result in
this direction, due to my MSc student Ulrich Schoepp. He has
shown that the proof system is complete for establishing
arbitrary mu-calculus properties of context-free processes.
The decidability of this problem has long been known, but
previous algorithms have used techniques specific to
context-free processes. As far as we know, this is the first
such result based on showing that general purpose techniques
suitable for arbitrary processes are complete when specialised
to context-free processes.