The Complexity of Model Checking Succinct Multiagent Systems
Authors: Xiaowei Huang, Qingliang Chen, Kaile Su
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | This paper studies the complexity of model checking multiagent systems, in particular systems succinctly described by two practical representations: concurrent representation and symbolic representation. The logics we concern include branching time temporal logics and several variants of alternating time temporal logics. This paper is to clarify the computational complexities of model checking these logics on multiagent systems. The complexity result of a model checking problem provides a theoretical indication on the scalability of a model checking algorithm. We prove the results for concurrent representation and symbolic representations. |
| Researcher Affiliation | Academia | Xiaowei Huang Jinan University, China CSE, UNSW, Australia; Qingliang Chen Jinan University, Guangzhou 510632, China; Kaile Su Jinan University, China IIIS, Griļ¬th University, Australia |
| Pseudocode | No | The paper describes algorithms in natural language within the proofs (e.g., in the proof of Theorem 2), but it does not include any formally structured pseudocode blocks or algorithms. |
| Open Source Code | No | The paper does not provide any statement or link indicating that the authors have released open-source code for the methodology or analysis described in the paper. It mentions external model checkers like Verics and Nu SMV as examples of tools that use the representations discussed, but this is not a release of their own code. |
| Open Datasets | No | This paper is theoretical and focuses on computational complexity proofs. It does not involve empirical training of models on datasets, and therefore no mention of publicly available training datasets or access information is present. |
| Dataset Splits | No | This paper is theoretical and focuses on computational complexity proofs. It does not involve empirical experiments with dataset splits, and therefore no specific dataset split information for validation is provided. |
| Hardware Specification | No | The paper is theoretical, presenting complexity results and proofs. It does not describe any empirical experiments that would require specific hardware, and thus no hardware specifications are provided. |
| Software Dependencies | No | The paper is theoretical, focusing on complexity analysis and proofs. It does not describe empirical experiments that would require specific software dependencies with version numbers. |
| Experiment Setup | No | The paper is theoretical, focusing on complexity analysis and proofs. It does not describe an empirical experimental setup with details like hyperparameters, training configurations, or system-level settings. |