Verifying Temporal Properties using Explicit Approximants: Completeness for Context-free Processes

Ulrich Schoepp, Alex Simpson

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


We present a sequent calculus for formally verifying modal mu-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the explicit manipulation of fixed-point approximants. We develop a new syntax for approximants, incorporating, in particular, a mechanism for approximant modification. We make essential use of this feature to prove our main result: the sequent calculus is complete for establishing arbitrary mu-calculus properties of context-free processes.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Start Conference Manager
Conference Systems