@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",
}