Model Checking Causality
Authors: Tiago de Lima, Emiliano Lorini
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In Section 4 we present a model checking algorithm for our language based on a polysize reduction to QBF. We illustrate its implementation on an example by providing some experimental results on computation time. and Table 1 shows the performance of the symbolic model checker on different instances of Example 5. Execution times correspond to the elapsed time to perform (1). |
| Researcher Affiliation | Academia | Tiago de Lima1 and Emiliano Lorini2 1CRIL, Univ Artois & CNRS, France 2IRIT, CNRS, Toulouse University, France delima@cril-lab.fr, Emiliano.Lorini@irit.fr |
| Pseudocode | No | Definition 14 (Translation) describes the translation process but it's not formatted as pseudocode or a labeled algorithm block. |
| Open Source Code | Yes | 4Available: https://src.koda.cnrs.fr/tiago.de.lima/cmc/-/releases/0.1.0.0 |
| Open Datasets | No | The paper uses 'instances of Example 5' for its evaluation, which is a conceptual example within the logical framework, not a publicly available dataset in the traditional sense. |
| Dataset Splits | No | The paper concerns model checking of logical formulas and does not involve data splitting for training, validation, or testing. |
| Hardware Specification | Yes | It was compiled with GHC 9.4.8 in a Mac Book Air with a 1.6 GHz Dual-Core Intel Core i5 processor and 16 GB of RAM, running mac OS Sonoma 14.1.2. |
| Software Dependencies | Yes | The program is implemented in Haskell and the BDD library used is Has Cac BDD [Gattinger, 2023]. It was compiled with GHC 9.4.8 and in references: Gattinger, M. (2023). Has Cac BDD, 2023. Version 0.1.0.4, Feb. 3, 2023. |
| Experiment Setup | No | The paper describes the varying number of agents for 'instances of Example 5' and the specific formula being checked, but it does not specify hyperparameters or training configurations typically found in machine learning experiments. |