A Decision Procedure for a Fragment of Linear Time Mu-Calculus
Abstract
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
Cite
Text
Liu et al. "A Decision Procedure for a Fragment of Linear Time Mu-Calculus." International Joint Conference on Artificial Intelligence, 2016.Markdown
[Liu et al. "A Decision Procedure for a Fragment of Linear Time Mu-Calculus." International Joint Conference on Artificial Intelligence, 2016.](https://mlanthology.org/ijcai/2016/liu2016ijcai-decision/)BibTeX
@inproceedings{liu2016ijcai-decision,
title = {{A Decision Procedure for a Fragment of Linear Time Mu-Calculus}},
author = {Liu, Yao and Duan, Zhenhua and Tian, Cong},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2016},
pages = {1195-1201},
url = {https://mlanthology.org/ijcai/2016/liu2016ijcai-decision/}
}