An effective tableau system for the linear time μ-calciilus

Julian Bradfield, Javier Esparza, Angelika Mader

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

8 Scopus citations

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 - 23rd International Colloquium, ICALP 1996, Proceedings
EditorsFriedhelm Meyer auf der Heide, Burkhard Monien
PublisherSpringer Verlag
Pages98-109
Number of pages12
ISBN (Print)3540614400, 9783540614401
DOIs
StatePublished - 1996
Event23rd International Colloquium on Automata, Languages, and Programming, ICALP 1996 - Paderborn, Germany
Duration: 8 Jul 199612 Jul 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1099
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Colloquium on Automata, Languages, and Programming, ICALP 1996
Country/TerritoryGermany
CityPaderborn
Period8/07/9612/07/96

Keywords

  • Linear-time μ-calculus
  • Local model-checking
  • Tableau systems
  • Temporal logic

Fingerprint

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

Cite this