A decision procedure for a fragment of linear time Mu-calculus
Yao Liu, Zhenhua Duan, Cong Tian · International Joint Conference on Artificial Intelligence · 2016
In this paper, we study an expressive fragment, namely Gµ, of linear time µ-calculus as a high-level 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.