Global Model Checking on Pushdown Multi-Agent Systems
Authors: Taolue Chen, Fu Song, Zhilin Wu
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We first give a triply exponential-time model checking algorithm for ATL over PGSs. The algorithm is based on the saturation method, and is the first global model checking algorithm with a matching lower bound. Next, we study the model checking problem for the alternating-time μ-calculus. We propose an exponential-time global model checking algorithm which extends similar algorithms for pushdown systems and modal μ-calculus. The algorithm admits a matching lower bound, which holds even for the alternation-free fragment and ATL. |
| Researcher Affiliation | Academia | Taolue Chen Department of Computer Science Middlesex University London, United Kingdom t.chen@mdx.ac.uk Fu Song Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai, P.R.China fsong@sei.ecnu.edu.cn Zhilin Wu State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing, P.R.China wuzl@ios.ac.cn |
| Pseudocode | No | The paper describes algorithmic approaches and theoretical constructions but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide any statement or link indicating that the source code for the described methodology is publicly available. |
| Open Datasets | No | This is a theoretical paper focusing on algorithms and complexity, and does not involve experimental evaluation on datasets. Therefore, no public dataset information is provided. |
| Dataset Splits | No | This is a theoretical paper and does not involve experimental evaluation with dataset splits. |
| Hardware Specification | No | This is a theoretical paper focusing on algorithms and complexity, and does not report any experimental hardware specifications. |
| Software Dependencies | No | This is a theoretical paper and does not report on software dependencies with specific version numbers for experimental reproducibility. |
| Experiment Setup | No | This is a theoretical paper and does not describe experimental setup details such as hyperparameters or training settings. |