A Decision Procedure for a Fragment of Linear Time Mu-Calculus
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 1195-1200.
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.
@inproceedings{ijcai2016p173,
title = {A Decision Procedure for a Fragment of Linear Time Mu-Calculus},
author = {Liu, Yao and Duan, Zhenhua and Tian, Cong},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-16}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Subbarao Kambhampati},
pages = {1195--1200},
year = {2016},
month = {7},
url = {https://ijcai.org/proceedings/2016/173},
}
TY - CPAPER TI - A Decision Procedure for a Fragment of Linear Time Mu-Calculus AU - Liu, Yao AU - Duan, Zhenhua AU - Tian, Cong T2 - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2016 SP - 1195 EP - 1200 UR - https://ijcai.org/proceedings/2016/173 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
