Langshaw: Declarative Interaction Protocols Based on Sayso and Conflict
Authors: Munindar P. Singh, Samuel H. Christie V., Amit K. Chopra
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Table 2 shows the performance (averaged over 10 runs) of testing liveness (including the time for constructing a tableau) for several protocols from the literature. The times for safety are similar, though slightly faster in most cases. |
| Researcher Affiliation | Academia | 1Department of Computer Science, North Carolina State University, Raleigh, NC 27695, USA 2School of Computing and Communications, Lancaster University, Lancaster LA1 4WA, UK |
| Pseudocode | Yes | Listing 1 Purchase in Langshaw.Listing 2 A simple protocol to explain BSPL constructs.Listing 3 Purchase: Completion requirements.Listing 4 Realizing the Reject and Deliver conflict.Figure 1: Synchronous semantics for Langshaw. |
| Open Source Code | Yes | The code and all examples are available online at https://gitlab.com/masr/langshaw |
| Open Datasets | Yes | Purchase, Unsafe Purchase, and Nonlive are as specified above. The remaining protocols are in the online supplement (URL below). |
| Dataset Splits | No | The paper discusses liveness and safety verification of protocols but does not specify dataset splits (e.g., training, validation, test percentages or counts) for these tasks. The protocols are treated as complete instances for verification. |
| Hardware Specification | Yes | Our experimental rig was an ASUS Zenbook S13 with an AMD Ryzen 7 6800U CPU and 16GB of LPDDR5 RAM, running Linux. |
| Software Dependencies | No | The paper states "We implemented our verifier for Langshaw protocols in Python" but does not provide specific version numbers for Python or any other libraries/dependencies used. |
| Experiment Setup | Yes | Table 2 shows the performance (averaged over 10 runs) of testing liveness (including the time for constructing a tableau) for several protocols from the literature. The times for safety are similar, though slightly faster in most cases. The node and branch numbers are sometimes fractions, due to unordered sets in the implementation randomizing the selection and thus producing different numbers of nodes and branches in different runs of the verifier. |