An effective tableau system for the linear time μ-calculus

Julian Bradfield; Javier Esparza; Angelika Mader

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

An effective tableau system for the linear time μ-calculus

Julian Bradfield, Javier Esparza, Angelika Mader

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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
Volume	1099
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 - 1996

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	1099

Keywords / Materials (for Non-textual outputs)

temporal logic
linear-time μ-calculus
local model-checking
tableau systems

Access to Document

10.1007/3-540-61440-0_120

http://dx.doi.org/10.1007/3-540-61440-0_120

Cite this

Bradfield, J., Esparza, J., & Mader, A. (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 (Vol. 1099, pp. 98-109). (Lecture Notes in Computer Science; Vol. 1099). Springer. https://doi.org/10.1007/3-540-61440-0_120

@inproceedings{9b51afd09f6b4466994e0614dae1a9c5,

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 = "temporal logic, linear-time μ-calculus, local model-checking, tableau systems",

author = "Julian Bradfield and Javier Esparza and Angelika Mader",

year = "1996",

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

language = "English",

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

volume = "1099",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "98--109",

editor = "Friedhelm Meyer and Burkhard Monien",

booktitle = "Automata, Languages and Programming",

address = "United Kingdom",

}

Bradfield, J, Esparza, J & Mader, A 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. vol. 1099, Lecture Notes in Computer Science, vol. 1099, Springer, pp. 98-109. 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.
Automata, Languages and Programming: 23rd International Colloquium, ICALP '96 Paderborn, Germany, July 8–12, 1996 Proceedings. ed. / Friedhelm Meyer; Burkhard Monien. Vol. 1099 Springer, 1996. p. 98-109 (Lecture Notes in Computer Science; Vol. 1099).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - An effective tableau system for the linear time μ-calculus

AU - Bradfield, Julian

AU - Esparza, Javier

AU - Mader, Angelika

PY - 1996

Y1 - 1996

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 - temporal logic

KW - linear-time μ-calculus

KW - local model-checking

KW - tableau systems

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

VL - 1099

T3 - Lecture Notes in Computer Science

SP - 98

EP - 109

BT - Automata, Languages and Programming

A2 - Meyer, Friedhelm

A2 - Monien, Burkhard

PB - Springer

ER -

An effective tableau system for the linear time μ-calculus

Abstract

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this