Abstract In this paper, we study an expressive fragment, namely Gµ , of linear time µ-calculus as a highlevel goal specification language. We define Goal Progression Form (GPF) for Gµ formulas and show that every closed formula can be transformed into this form. Based on GPF, we present the notion of Goal Progression Form Graph (GPG) which can be used to describe models of a formula. Further, we propose a simple and intuitive GPG-based decision procedure for checking satisfiability of Gµ formulas which has the same time complexity as the decision problem of Linear Temporal Logic (LTL). However, Gµ is able to express a wider variety of temporal goals compared with LTL.