Verifying Pushdown Multi-Agent Systems against Strategy Logics
Authors: Taolue Chen, Fu Song, Zhilin Wu
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we investigate model checking algorithms for variants of strategy logic over pushdown multi-agent systems, modeled by pushdown game structures (PGSs). We consider various fragments of strategy logic, i.e., SL[CG], SL[DG], SL[1G] and BSIL. We show that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, which are not harder than the problem for the subsumed logic ATL . When BSIL is concerned, the model checking problem becomes 2EXPTIME-complete. Our algorithms are automata-theoretic and based on the saturation technique, which are amenable to implementations. |
| Researcher Affiliation | Academia | Taolue Chen Department of Computer Science Middlesex University London, UK Fu Song Shanghai Key Laboratory of Trustworthy Computing East China Normal University, China Zhilin Wu State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, China |
| Pseudocode | No | The paper describes algorithms textually and mathematically, but it does not contain a structured pseudocode or algorithm block. |
| Open Source Code | No | The paper does not contain any explicit statements or links indicating that source code for the described methodology is publicly available. |
| Open Datasets | No | This paper is theoretical and does not involve training models on empirical datasets. It mentions "regular valuations" in the context of defining the logic, not as a dataset for training. |
| Dataset Splits | No | This paper is theoretical and does not involve empirical validation splits for datasets. |
| Hardware Specification | No | The paper is theoretical and does not describe any experimental hardware specifications (e.g., GPU/CPU models, memory details). |
| Software Dependencies | No | The paper is theoretical and does not mention specific software dependencies with version numbers (e.g., libraries, frameworks, or solvers) required for replication. |
| Experiment Setup | No | The paper is theoretical and does not describe an empirical experimental setup, including hyperparameters or system-level training settings. |