An effective tableau system for the linear time mu-calculus

Julian Bradfield, Javier Esparza and Angelika Mader

Abstract: We present a tableau system for the model checking problem of the linear time mu-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.

ECS-LFCS-95-337, December 1995.

This report is available in the following formats:

Previous | Index | Next