Model Checking Fixed Point Logic with Chop

Martin Lange, Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication5th 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
PublisherSpringer Berlin Heidelberg
Number of pages14
ISBN (Electronic)978-3-540-45931-6
ISBN (Print)978-3-540-43366-8
Publication statusPublished - 2002

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Model Checking Fixed Point Logic with Chop'. Together they form a unique fingerprint.

Cite this