Completeness for Context-free Processes

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.