Model Checking Multi-Agent Systems against LDLK Specifications
Authors: Jeremy Kong, Alessio Lomuscio
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We introduce MCMASLDLK, an extension of the open-source model checker MCMAS implementing the algorithm presented, and discuss the experimental results obtained. |
| Researcher Affiliation | Academia | Jeremy Kong and Alessio Lomuscio Department of Computing, Imperial College London jeremykong91@gmail.com, a.lomuscio@imperial.ac.uk |
| Pseudocode | Yes | Algorithm 1 Symbolic LDLK Model Checking Algorithm |
| Open Source Code | Yes | The sources and executables of the resulting toolkit, called MCMASLDLK, are available from [MCMASLDLK, 2017]. |
| Open Datasets | No | As a testbed we took the prisoners and lightbulb scenario [Ditmarsch et al., 2010]. This is a description of a system to model check, not a dataset for training/testing. No public dataset access information is provided. |
| Dataset Splits | No | The paper discusses model checking a scenario rather than training/testing on a dataset, thus no specific dataset split information for reproduction is provided. |
| Hardware Specification | Yes | We report below experiments run on virtual machines with two 2.70GHz CPUs and 16 GB of RAM running Ubuntu v15.10 (Linux kernel v4.2). |
| Software Dependencies | Yes | We implemented the algorithms introduced in Section 3 on top of version 1.2.2 of MCMAS [Lomuscio et al., 2015], an open-source BDD-based symbolic model checker. |
| Experiment Setup | Yes | MCMASLDLK employs several optimisations. First, note that the checker s performance is affected by the size of the alternating automata constructed. To mitigate this MCMASLDLK employs: propositional shortcircuiting (PS): instead of constructing the corresponding alternating automaton, subformulae free of dynamic modalities and states where they hold are identified; and fresh atomic propositions for these are introduced. reachability pruning (RP): Since ϵ-NFA states with no inbound non-ϵ transitions are never transitioned to in alternating automata, these are not included in the alternating automata (but are still considered in the ϵ-NFAs to find critical sets). The automata remain polynomial (so the complexity is unaffected), but we found these optimisations useful in practice. We further optimised MCMASLDLK for efficiently computing conjuncts (ECC) for the symbolic breakpoint construction, which involves computing TI TLC TR (notation from [Bloem et al., 2006]). |