AN Effective Tableau System for the Linear Time mu-Calculus

摘要

We present a tableau system for the model checking problem of the linear time mu-calculus. It improves the system of stirlin 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.