An effective tableau system for the linear time μ-calculus

Julian Bradfield, Javier Esparza, Angelika Mader

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


We present a tableau system for the model checking problem of the linear time μ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings
EditorsFriedhelm Meyer, Burkhard Monien
PublisherSpringer Berlin Heidelberg
Number of pages12
ISBN (Electronic)978-3-540-68580-7
ISBN (Print)978-3-540-61440-1
Publication statusPublished - 1996

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


  • temporal logic
  • linear-time μ-calculus
  • local model-checking
  • tableau systems


Dive into the research topics of 'An effective tableau system for the linear time μ-calculus'. Together they form a unique fingerprint.

Cite this