An Effective Tableau System for the Linear Time µ-Calculus

Julian Bradfield, Javier Esparza, Angelika H. Mader

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

    8 Citations (Scopus)
    26 Downloads (Pure)

    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
    Pages98-109
    Number of pages12
    ISBN (Electronic)978-3-540-68580-7
    ISBN (Print)978-3-540-61440-1
    DOIs
    Publication statusPublished - Jul 1996
    Event23rd International Colloquium on Automata, Languages and Programming, ICALP 1996 - Paderborn, Germany
    Duration: 8 Jul 199612 Jul 1996
    Conference number: 23

    Conference

    Conference23rd International Colloquium on Automata, Languages and Programming, ICALP 1996
    Abbreviated titleICALP
    CountryGermany
    CityPaderborn
    Period8/07/9612/07/96

    Keywords

    • EWI-1122
    • IR-56233

    Fingerprint Dive into the research topics of 'An Effective Tableau System for the Linear Time µ-Calculus'. Together they form a unique fingerprint.

  • Cite this

    Bradfield, J., Esparza, J., & Mader, A. H. (1996). An Effective Tableau System for the Linear Time µ-Calculus. In F. Meyer, & B. Monien (Eds.), Automata, Languages and Programming: 23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings (pp. 98-109). Springer. https://doi.org/10.1007/3-540-61440-0_120