Verifying temporal properties using explicit approximants: completeness for context-free processes

Ulrich Schöpp; Alexander Simpson

doi:10.1007/3-540-45931-6_26

Verifying temporal properties using explicit approximants: completeness for context-free processes

Ulrich Schöpp, Alexander Simpson

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Publisher	Springer-Verlag GmbH
Pages	372-386
Number of pages	15
ISBN (Print)	978-3-540-43366-8
DOIs	https://doi.org/10.1007/3-540-45931-6_26
Publication status	Published - 2002

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	2303
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/3-540-45931-6_26

download 7Accepted author manuscript, 265 KB

http://www.springerlink.com/content/cpgmlqk33ybf1uub

Models and Axioms for the Semantics of Computation
Simpson, A.
EPSRC
1/10/01 → 30/09/06
Project: Research

Cite this

@inproceedings{270a578b0af741b49f8f24b85dacb086,

title = "Verifying temporal properties using explicit approximants: completeness for context-free processes",

abstract = "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. ",

author = "Ulrich Sch{\"o}pp and Alexander Simpson",

year = "2002",

doi = "10.1007/3-540-45931-6_26",

language = "English",

isbn = "978-3-540-43366-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "372--386",

booktitle = "Foundations of Software Science and Computation Structures",

}

Verifying temporal properties using explicit approximants: completeness for context-free processes. / Schöpp, Ulrich; Simpson, Alexander.

Foundations of Software Science and Computation Structures. Springer-Verlag GmbH, 2002. p. 372-386 (Lecture Notes in Computer Science; Vol. 2303).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Verifying temporal properties using explicit approximants: completeness for context-free processes

AU - Schöpp, Ulrich

AU - Simpson, Alexander

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-45931-6_26

DO - 10.1007/3-540-45931-6_26

M3 - Conference contribution

SN - 978-3-540-43366-8

T3 - Lecture Notes in Computer Science

SP - 372

EP - 386

BT - Foundations of Software Science and Computation Structures

PB - Springer-Verlag GmbH

ER -

Verifying temporal properties using explicit approximants: completeness for context-free processes

Abstract

Publication series

Access to Document

Fingerprint

Projects

Models and Axioms for the Semantics of Computation

Cite this