Symbolic Model Checking Epistemic Strategy Logic
Authors: Xiaowei Huang, Ron van der Meyden
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implement the algorithm in a model checker and apply it to an application on train control system. The performance of the algorithm is also reported, with a comparison showing improved results over a previous partially symbolic approach for ATEL model checking. |
| Researcher Affiliation | Academia | Xiaowei Huang and Ron van der Meyden School of Computer Science and Engineering University of New South Wales, Australia |
| Pseudocode | No | The paper describes the symbolic algorithm using mathematical definitions and recursive formulas (Deļ¬nition 1), but it does not present a structured pseudocode block or algorithm listing. |
| Open Source Code | No | The paper mentions that the algorithm has been implemented in an epistemic model checker MCK, but it does not state that the code for their specific implementation or methodology is open-source or provide a link to it. |
| Open Datasets | No | The paper describes a 'train control system' scenario as an application example. This is a self-defined model or system within the paper, not a publicly available dataset with concrete access information (link, DOI, citation). |
| Dataset Splits | No | The paper does not provide specific training/validation/test dataset splits. It describes applying the algorithm to a self-defined 'train control system' with varying numbers of trains. |
| Hardware Specification | Yes | The experiments were conducted on a Debian Linux system, 3.3 GHz Intel i5-2500 CPU, with each process allocated up to 500M memory. |
| Software Dependencies | No | The paper states the algorithm was 'implemented in an epistemic model checker MCK (Gammie and van der Meyden 2004)'. However, it does not provide specific version numbers for MCK or any other software libraries or dependencies. |
| Experiment Setup | Yes | For the train control system, we scale up the number of trains in the system. ... The experiments were conducted on a Debian Linux system, 3.3 GHz Intel i5-2500 CPU, with each process allocated up to 500M memory. |