The power of first-order quantification over states in branching and linear time temporal logics

In this paper, we investigate the power of extending first-order quantification over states to branching and linear time temporal logics. We show that an unrestricted extension significantly enriches the expressive power of mu-calculus, but also leads to a significant jump in model checking complexity. However, by restricting the scope of the extension, we are able to present a powerful extension of mu-calculus that is richer than mu-calculus, but is in the same complexity class as mu-calculus in terms of model checking complexity. In the case of linear time temporal logic, we find that first-order quantification over states is more computationally expensive. We show that even under the most restricted scope of quantification, the program complexity of model checking linear temporal logic (LTL) is NP-hard and coNP-hard. However, we also show that model checking LTL with this generic extension remains PSPACE-complete. (C) 2004 Elsevier B.V. All rights reserved.