A Decision Procedure for a Fragment of Linear Time Mu-Calculus
Authors: Yao Liu, Zhenhua Duan, Cong Tian
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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). Theorem 2 Every closed formula ' can be transformed into GPF. Theorem 3 Transforming a formula φ into GPF by algorithm GPFTr can be completed in 2O(|φ|). Theorem 6 A closed formula φ is satisfiable iff a -path can be found in Gφ. Theorem 8 For a given closed formula φ, the GPG-based decision procedure can be done in 2O(|φ|). |
| Researcher Affiliation | Academia | ICTT and ISN Laboratory, Xidian University |
| Pseudocode | Yes | Algorithm 1 GPFTr(φ), Algorithm 2 GPGCON(φ), Algorithm 3 Nu Search(n0) |
| Open Source Code | No | The paper does not contain any statement about releasing open-source code for the methodology described, nor does it provide a direct link to a code repository. |
| Open Datasets | No | The paper is theoretical and does not involve datasets or empirical training. Therefore, it does not mention public or open datasets. |
| Dataset Splits | No | The paper is theoretical and does not involve datasets or empirical validation. Therefore, it does not provide dataset splits for validation. |
| Hardware Specification | No | This is a theoretical paper and does not describe any experiments that would require specific hardware. No hardware specifications are mentioned. |
| Software Dependencies | No | This is a theoretical paper and does not describe any experiments that would require specific software dependencies with version numbers. No such details are provided. |
| Experiment Setup | No | This is a theoretical paper and does not involve an experimental setup with hyperparameters or training settings. No such details are provided. |