Modal µ-Calculus, Model Checking and Gauß Elimination

Hendrik Brinksma (Editor), Angelika H. Mader, W.R. Cleaveland (Editor), K.G. Larsen (Editor), K.G. Larsen (Editor), T. Margaria (Editor), B. Steffen (Editor)

    Research output: Contribution to conferencePaper

    52 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 languageUndefined
    Pages72-88
    Number of pages17
    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
    CountryDenmark
    CityAarhus
    Period19/05/9520/05/95

    Keywords

    • IR-56275
    • EWI-1156

    Cite this

    Brinksma, H. (Ed.), Mader, A. H., Cleaveland, W. R. (Ed.), Larsen, K. G. (Ed.), Larsen, K. G. (Ed.), Margaria, T. (Ed.), & Steffen, B. (Ed.) (1995). Modal µ-Calculus, Model Checking and Gauß Elimination. 72-88. Paper presented at 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, Aarhus, Denmark. https://doi.org/10.1007/3-540-60630-0_4