Projects per year
We present a sequent calculus for formally verifying modal μ-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, modalities for approximant modification. We make essential use of this feature to prove our main result: the sequent calculus is complete for establishing arbitrary μ-calculus properties of context-free processes.
|Title of host publication||Foundations of Software Science and Computation Structures|
|Number of pages||15|
|Publication status||Published - 2002|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|
FingerprintDive into the research topics of 'Verifying temporal properties using explicit approximants: completeness for context-free processes'. Together they form a unique fingerprint.
- 1 Finished
Models and Axioms for the Semantics of Computation
1/10/01 → 30/09/06