An effective tableau system for the linear time μ-calculus

Julian Bradfield, Javier Esparza, Angelika Mader

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

Abstract

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
Pages98-109
Number of pages12
Volume1099
ISBN (Electronic)978-3-540-68580-7
ISBN (Print)978-3-540-61440-1
DOIs
Publication statusPublished - 1996

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1099

Keywords

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

Fingerprint

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

Cite this