Tableau Recycling

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

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

    2 Citations (Scopus)
    39 Downloads (Pure)

    Abstract

    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
    Pages330-342
    Number of pages13
    ISBN (Electronic)978-3-540-47572-9
    DOIs
    Publication statusPublished - Jun 1992
    Event4th Workshop on Computer-Aided Verification, CAV 1992 - Montreal, Canada
    Duration: 29 Jun 19921 Jul 1992
    Conference number: 4

    Conference

    Conference4th Workshop on Computer-Aided Verification, CAV 1992
    Abbreviated titleCAV
    CountryCanada
    CityMontreal
    Period29/06/921/07/92

    Keywords

    • IR-56287
    • EWI-1204

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

  • Cite this

    von Bochmann, G. (Ed.), Mader, A. H., & Probst, D. K. (Ed.) (1992). Tableau Recycling. In G. von Bochmann, & D. K. Probst (Eds.), Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings (pp. 330-342) https://doi.org/10.1007/3-540-56496-9_26