Backward Responsibility in Transition Systems Using General Power Indices
Authors: Christel Baier, Roxane van den Bossche, Sascha Klüppelholz, Johannes Lehmann, Jakob Piribauer
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We provide an implementation, show how a stochastic algorithm can be used to analyse large models and evaluate our implementation with several experiments in Section 5.We have evaluated this on a collection of benchmarks. alternating bit is a simple message transition protocol, brp is a protocol to transfer files consisting of N chunks (with MAX attempts), crowds models anonymised message routing through a group of size CS (with TR total runs), dining philosophers models the well-known dining philosophers problem, dresden railways models the switches in Dresden Central Station, where a train has to be routed to a specific platform and generals models the n-generals problem, who have to decide independently whether to attack or not. |
| Researcher Affiliation | Academia | Christel Baier1,2, Roxane van den Bossche3, Sascha Kl uppelholz1, Johannes Lehmann1, Jakob Piribauer1 * 1TU Dresden, Germany 2Centre for Tactile Internet with Human-in-the-Loop (Ce TI) 3Universit e Paris-Saclay, ENS Paris-Saclay, France |
| Pseudocode | No | The paper describes algorithms and methods in text and mathematical formulations but does not include any figure, block, or section explicitly labeled 'Pseudocode' or 'Algorithm'. |
| Open Source Code | Yes | We have developed a tool that computes optimistic and pessimistic backward responsibility1 (Lehmann 2024). 1Available at https://github.com/johannesalehmann/backwardresponsibility |
| Open Datasets | Yes | The benchmarks brp and crowds are taken from Kwiatkowska, Norman, and Parker (2012). This citation refers to "The PRISM Benchmark Suite," indicating a publicly available dataset/benchmark suite. |
| Dataset Splits | No | The paper describes analysis on existing transition systems and models (e.g., railway network, peg solitaire, dining philosophers, PRISM benchmarks) but does not mention data splits for training, validation, or testing, as it's not a machine learning paper with typical dataset splits. |
| Hardware Specification | Yes | All benchmarks were run on a Mac Book Pro running mac OS 13.3 with an 8-core M2 chip and 24 GB of memory. |
| Software Dependencies | No | Our tool uses the model checker PRISM (Kwiatkowska, Norman, and Parker 2011) to build the model and check the safety property. While PRISM is mentioned and cited, its specific version number is not provided, nor are other software dependencies with versions for the authors' tool. |
| Experiment Setup | Yes | For each model, we have sampled for t seconds (where t {1, 10, 60}) and then computed the responsibility of all states using these samples. To evaluate the quality of our samples, we have repeated this procedure 20 times and determined the standard deviation of the estimated responsibility from the actual value. |