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

}