An Effective Tableau System for the Linear Time µ-Calculus

Julian Bradfield; Javier Esparza; Angelika H. Mader

doi:10.1007/3-540-61440-0_120

An Effective Tableau System for the Linear Time µ-Calculus

Julian Bradfield
, Javier Esparza
, Angelika H. Mader

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

8 Citations (Scopus)

294 Downloads (Pure)

Abstract

We present a tableau system for the model checking problem of the linear time µ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.

Original language	English
Title of host publication	Automata, Languages and Programming
Subtitle of host publication	23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings
Editors	Friedhelm Meyer, Burkhard Monien
Publisher	Springer
Pages	98-109
Number of pages	12
ISBN (Electronic)	978-3-540-68580-7
ISBN (Print)	978-3-540-61440-1
DOIs	https://doi.org/10.1007/3-540-61440-0_120
Publication status	Published - Jul 1996
Event	23rd International Colloquium on Automata, Languages and Programming, ICALP 1996 - Paderborn, Germany Duration: 8 Jul 1996 → 12 Jul 1996 Conference number: 23

Conference

Conference	23rd International Colloquium on Automata, Languages and Programming, ICALP 1996
Abbreviated title	ICALP
Country/Territory	Germany
City	Paderborn
Period	8/07/96 → 12/07/96

Keywords

EWI-1122
IR-56233

Access to Document

10.1007/3-540-61440-0_120

effective_BradfieldFinal published version, 614 KB

Cite this

@inproceedings{afaff81f56c3426cad0fe4997b3f3340,

title = "An Effective Tableau System for the Linear Time µ-Calculus",

abstract = "We present a tableau system for the model checking problem of the linear time µ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.",

keywords = "EWI-1122, IR-56233",

author = "Julian Bradfield and Javier Esparza and Mader, \{Angelika H.\}",

note = "Imported from DIES; 23rd International Colloquium on Automata, Languages and Programming, ICALP 1996, ICALP ; Conference date: 08-07-1996 Through 12-07-1996",

year = "1996",

month = jul,

doi = "10.1007/3-540-61440-0\_120",

language = "English",

isbn = "978-3-540-61440-1",

pages = "98--109",

editor = "Friedhelm Meyer and Burkhard Monien",

booktitle = "Automata, Languages and Programming",

publisher = "Springer",

address = "Germany",

}

Bradfield, J, Esparza, J & Mader, AH 1996, An Effective Tableau System for the Linear Time µ-Calculus. in F Meyer & B Monien (eds), Automata, Languages and Programming: 23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings. Springer, pp. 98-109, 23rd International Colloquium on Automata, Languages and Programming, ICALP 1996, Paderborn, Germany, 8/07/96. https://doi.org/10.1007/3-540-61440-0_120

An Effective Tableau System for the Linear Time µ-Calculus. / Bradfield, Julian; Esparza, Javier; Mader, Angelika H.
Automata, Languages and Programming: 23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings. ed. / Friedhelm Meyer; Burkhard Monien. Springer, 1996. p. 98-109.

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

TY - GEN

T1 - An Effective Tableau System for the Linear Time µ-Calculus

AU - Bradfield, Julian

AU - Esparza, Javier

AU - Mader, Angelika H.

N1 - Conference code: 23

PY - 1996/7

Y1 - 1996/7

N2 - We present a tableau system for the model checking problem of the linear time µ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.

AB - We present a tableau system for the model checking problem of the linear time µ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.

KW - EWI-1122

KW - IR-56233

U2 - 10.1007/3-540-61440-0_120

DO - 10.1007/3-540-61440-0_120

M3 - Conference contribution

SN - 978-3-540-61440-1

SP - 98

EP - 109

BT - Automata, Languages and Programming

A2 - Meyer, Friedhelm

A2 - Monien, Burkhard

PB - Springer

T2 - 23rd International Colloquium on Automata, Languages and Programming, ICALP 1996

Y2 - 8 July 1996 through 12 July 1996

ER -

An Effective Tableau System for the Linear Time µ-Calculus

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this