A Decision Procedure for a Fragment of Linear Time Mu-Calculus / 1195
Yao Liu, Zhenhua Duan, Cong Tian

In this paper, we study an expressive fragment, namely Gmu, of linear time mu-calculus as a high-level goal specification language. We define Goal Progression Form (GPF) for Gmu 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 Gmu formulas which has the same time complexity as the decision problem of Linear Temporal Logic (LTL). However, Gmu is able to express a wider variety of temporal goals compared with LTL.

PDF