Modal µ-Calculus, Model Checking and Gauß Elimination

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

    15 Citations (Scopus)
    152 Downloads (Pure)

    Abstract

    In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gauß elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.
    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    Subtitle of host publicationFirst International Workshop, TACAS '95, Aarhus, Denmark, May 19-20, 1995. Selected Papers
    EditorsE. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, B. Steffen
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages72-88
    Number of pages17
    ISBN (Electronic)978-3-540-48509-4
    ISBN (Print)978-3-540-60630-7
    DOIs
    Publication statusPublished - May 1995
    Event1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995 - Aarhus, Denmark
    Duration: 19 May 199520 May 1995
    Conference number: 1

    Workshop

    Workshop1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995
    Abbreviated titleTACAS
    Country/TerritoryDenmark
    CityAarhus
    Period19/05/9520/05/95

    Fingerprint

    Dive into the research topics of 'Modal µ-Calculus, Model Checking and Gauß Elimination'. Together they form a unique fingerprint.

    Cite this