Model Checking Fixed Point Logic with Chop

Martin Lange; Colin Stirling

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

Model Checking Fixed Point Logic with Chop

Martin Lange, Colin Stirling

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

Abstract

This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC’s model checking problem over finite transition systems. It is proved to be Pspace-hard. A tableau model checker is given and an upper Exptime bound is derived from it. For a fixed alternation depth FLC’s model checking problem turns out to be Pspace-complete.

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings
Publisher	Springer Berlin Heidelberg
Pages	250-263
Number of pages	14
ISBN (Electronic)	978-3-540-45931-6
ISBN (Print)	978-3-540-43366-8
DOIs	https://doi.org/10.1007/3-540-45931-6_18
Publication status	Published - 2002

Publication series

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

Access to Document

10.1007/3-540-45931-6_18

http://link.springer.com/chapter/10.1007%2F3-540-45931-6_18

Cite this

Lange, M., & Stirling, C. (2002). Model Checking Fixed Point Logic with Chop. In Foundations of Software Science and Computation Structures: 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings (pp. 250-263). (Lecture Notes in Computer Science; Vol. 2303). Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-45931-6_18

Lange, Martin ; Stirling, Colin. / Model Checking Fixed Point Logic with Chop. Foundations of Software Science and Computation Structures: 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings. Springer Berlin Heidelberg, 2002. pp. 250-263 (Lecture Notes in Computer Science).

@inproceedings{b53b61fa0db24860ab1a4d64a4add4b7,

title = "Model Checking Fixed Point Logic with Chop",

abstract = "This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC{\textquoteright}s model checking problem over finite transition systems. It is proved to be Pspace-hard. A tableau model checker is given and an upper Exptime bound is derived from it. For a fixed alternation depth FLC{\textquoteright}s model checking problem turns out to be Pspace-complete.",

author = "Martin Lange and Colin Stirling",

year = "2002",

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

language = "English",

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

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "250--263",

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

}

Lange, M & Stirling, C 2002, Model Checking Fixed Point Logic with Chop. in Foundations of Software Science and Computation Structures: 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2303, Springer Berlin Heidelberg, pp. 250-263. https://doi.org/10.1007/3-540-45931-6_18

Model Checking Fixed Point Logic with Chop. / Lange, Martin; Stirling, Colin.

Foundations of Software Science and Computation Structures: 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings. Springer Berlin Heidelberg, 2002. p. 250-263 (Lecture Notes in Computer Science; Vol. 2303).

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

TY - GEN

T1 - Model Checking Fixed Point Logic with Chop

AU - Lange, Martin

AU - Stirling, Colin

PY - 2002

Y1 - 2002

N2 - This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC’s model checking problem over finite transition systems. It is proved to be Pspace-hard. A tableau model checker is given and an upper Exptime bound is derived from it. For a fixed alternation depth FLC’s model checking problem turns out to be Pspace-complete.

AB - This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC’s model checking problem over finite transition systems. It is proved to be Pspace-hard. A tableau model checker is given and an upper Exptime bound is derived from it. For a fixed alternation depth FLC’s model checking problem turns out to be Pspace-complete.

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

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

M3 - Conference contribution

SN - 978-3-540-43366-8

T3 - Lecture Notes in Computer Science

SP - 250

EP - 263

BT - Foundations of Software Science and Computation Structures

PB - Springer Berlin Heidelberg

ER -

Lange M, Stirling C. Model Checking Fixed Point Logic with Chop. In Foundations of Software Science and Computation Structures: 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings. Springer Berlin Heidelberg. 2002. p. 250-263. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-45931-6_18

Model Checking Fixed Point Logic with Chop

Abstract

Publication series

Access to Document

Fingerprint

Cite this