Tableau Recycling

G. von Bochmann; Angelika H. Mader; D.K. Probst

doi:10.1007/3-540-56496-9_26

Tableau Recycling

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

198 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 language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings
Editors	Gregor von Bochmann, David Karl Probst
Pages	330-342
Number of pages	13
ISBN (Electronic)	978-3-540-47572-9
DOIs	https://doi.org/10.1007/3-540-56496-9_26
Publication status	Published - Jun 1992
Event	4th Workshop on Computer-Aided Verification, CAV 1992 - Montreal, Canada Duration: 29 Jun 1992 → 1 Jul 1992 Conference number: 4

Conference

Conference	4th Workshop on Computer-Aided Verification, CAV 1992
Abbreviated title	CAV
Country/Territory	Canada
City	Montreal
Period	29/06/92 → 1/07/92

Keywords

IR-56287
EWI-1204

Access to Document

10.1007/3-540-56496-9_26

mader92tableauFinal published version, 606 KB

Cite this

@inproceedings{9327291d900d43d991e6aec5a986dbdd,

title = "Tableau Recycling",

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.",

keywords = "IR-56287, EWI-1204",

author = "{von Bochmann}, G. and Mader, {Angelika H.} and D.K. Probst",

note = "Imported from DIES; 4th Workshop on Computer-Aided Verification, CAV 1992, CAV ; Conference date: 29-06-1992 Through 01-07-1992",

year = "1992",

month = jun,

doi = "10.1007/3-540-56496-9_26",

language = "English",

isbn = "978-3-540-56496-6",

pages = "330--342",

editor = "{von Bochmann}, Gregor and Probst, {David Karl}",

booktitle = "Computer Aided Verification",

}

von Bochmann, G (ed.), Mader, AH & Probst, DK (ed.) 1992, Tableau Recycling. in G von Bochmann & DK Probst (eds), Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings. pp. 330-342, 4th Workshop on Computer-Aided Verification, CAV 1992, Montreal, Canada, 29/06/92. https://doi.org/10.1007/3-540-56496-9_26

Tableau Recycling. / von Bochmann, G. (Editor); Mader, Angelika H.; Probst, D.K. (Editor).
Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings. ed. / Gregor von Bochmann; David Karl Probst. 1992. p. 330-342.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Tableau Recycling

AU - Mader, Angelika H.

A2 - von Bochmann, G.

A2 - Probst, D.K.

A2 - von Bochmann, Gregor

A2 - Probst, David Karl

N1 - Conference code: 4

PY - 1992/6

Y1 - 1992/6

N2 - 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.

AB - 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.

KW - IR-56287

KW - EWI-1204

U2 - 10.1007/3-540-56496-9_26

DO - 10.1007/3-540-56496-9_26

M3 - Conference contribution

SN - 978-3-540-56496-6

SP - 330

EP - 342

BT - Computer Aided Verification

T2 - 4th Workshop on Computer-Aided Verification, CAV 1992

Y2 - 29 June 1992 through 1 July 1992

ER -

Tableau Recycling

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this