Tableau Recycling

G. von Bochmann (Editor), Angelika H. Mader, D.K. Probst (Editor)

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

    3 Citations (Scopus)
    192 Downloads (Pure)


    In this paper we improve a model checking algorithm based on the tableau method of Stifling and Walker. The algorithm proves whether a property expressed in the modal mu-calculus holds for a state in a finite transition system. It makes subsequent use of subtableaux which were calculated earlier in the proof run. These aubtab|eaux are reduced to expressions. Examples show that both size of tableaux and execution time of the algorithm are reduced.
    Original languageEnglish
    Title of host publicationComputer Aided Verification
    Subtitle of host publicationFourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings
    EditorsGregor von Bochmann, David Karl Probst
    Number of pages13
    ISBN (Electronic)978-3-540-47572-9
    Publication statusPublished - Jun 1992
    Event4th Workshop on Computer-Aided Verification, CAV 1992 - Montreal, Canada
    Duration: 29 Jun 19921 Jul 1992
    Conference number: 4


    Conference4th Workshop on Computer-Aided Verification, CAV 1992
    Abbreviated titleCAV


    • IR-56287
    • EWI-1204


    Dive into the research topics of 'Tableau Recycling'. Together they form a unique fingerprint.

    Cite this