Reference:

J. Bradfield, J. Esparza, and A. Mader. An effective tableau system for the linear time mu-calculus. In F. Meyer auf der Heide and B. Monien, editors, Proc. of ICALP'96, number 1099 in Lecture Notes in Computer Science, pages 98–109. Springer-Verlag, 1996.

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.

Suggested BibTeX entry:

@inproceedings{BEM96,
    author = {J. Bradfield and J. Esparza and A. Mader},
    booktitle = {Proc. of ICALP'96},
    editor = {F. Meyer auf der Heide and B. Monien},
    number = {1099},
    pages = {98--109},
    publisher = {{Springer-Verlag}},
    series = {{Lecture Notes in Computer Science}},
    title = {An effective tableau system for the linear time mu-calculus},
    year = {1996}
}