Global Model Checking on Pushdown Multi-Agent Systems
Authors: Taolue Chen, Fu Song, Zhilin Wu
AAAI 2016 | Venue 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 EMAIL Fu Song Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai, P.R.China EMAIL Zhilin Wu State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing, P.R.China EMAIL |
| 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. |