Model Checking Temporal Epistemic Logic under Bounded Recall
Authors: Francesco Belardinelli, Alessio Lomuscio, Emily Yu7071-7078
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained. In Section 4 we introduce an implementation that we built supporting bounded recall and report the experimental results obtained when model checking agents under various sizes of recall. (See also Table 1 and Table 2 for experimental results) |
| Researcher Affiliation | Academia | 1Imperial College London, UK 2Johannes Kepler University Linz, Austria |
| Pseudocode | Yes | The semantics of CTLKBR can be checked by using the procedure VERIFY(ϕ, h), reported below, which operates recursively by the depth of the formula. The cases are as follows: VERIFY(p, h): ... VERIFY(ϕ φ, h): ... |
| Open Source Code | Yes | We implemented the algorithms of the previous section into an experimental checker called MCMASBR (MCMASBR 2020), which extends the open source checker MCMAS (Lomuscio, Qu, and Raimondi 2017) by adding support to bounded recall semantics; [...] MCMASBR. 2020. MCMASBR. https://vas.doc.ic.ac.uk/software/mcmas/extensions/. |
| Open Datasets | No | The paper uses illustrative examples (N-Transmission-Protocol, Train-Gate-Controller) for evaluation, not publicly available datasets with specified access information (links, DOIs, or formal citations). |
| Dataset Splits | No | The paper describes experimental scenarios but does not specify explicit train/validation/test dataset splits, as this is not typical for model checking experiments. |
| Hardware Specification | Yes | Table 1 shows the experimental results obtained with MCMASBR running on an Intel R Core TM i7-2600 CPU 3.40GHz machine with 16GB RAM running Ubuntu v18.04.2 (Linux kernel v4.15). |
| Software Dependencies | Yes | MCMASBR (MCMASBR 2020) [...] running Ubuntu v18.04.2 (Linux kernel v4.15). |
| Experiment Setup | Yes | Verification under bounded recall semantics is carried out by invoking the tool with the command-line flag -bpr [window_size], where the size of the recall window is specified by the user. [...] To evaluate the cost of bounded recall, we now report how the performance of MCMASBR scales as we increase the value of the window size and the example size. |