Automated Analysis of Commitment Protocols Using Probabilistic Model Checking
Authors: Akın Günay, Song Songzheng, Yang Liu, Jie Zhang
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We conducted a set of experiments to evaluate the execution performance of our algorithms and the effect of our reduction technique. For these experiments we implemented Algorithms 1 and 2. We systematically created a set of protocol models based on our e-commerce protocol for evaluation as follows2. We combined n number of copies of the base ecommerce protocol, such that each copy of the base protocol uses new identifiers for Buyer and Provider, and the commitments are created between these new roles and the original Seller. Hence, each copy of the basic protocol can be executed independent from the other copies. We run our experiments on a PC equipped with an Intel i7 3.0 GHz processor and 4GB RAM running 64-bit Windows 7 operating system. We verify all three properties for each protocol according to the beliefs of Seller. For brevity we present only the result for the verification of the conformance property in Table 1. However, we observed similar results for other properties. |
| Researcher Affiliation | Academia | Akın G unay and Song Songzheng and Yang Liu and Jie Zhang School of Computer Engineering, Nanyang Technological University, Singapore akingunay@ntu.edu.sg, songsz@ntu.edu.sg, yangliu@ntu.edu.sg, zhangj@ntu.edu.sg |
| Pseudocode | Yes | Algorithm 1: Algorithm to create the PA α and terminal states F from the protocol P, agent X and domain D. Algorithm 2: Computation of the probability to reach the target states from the initial state. |
| Open Source Code | No | The implementations and protocol models can be downloaded from http://pat.sce.ntu.edu.sg/akin. This URL is a general project page, not a direct code repository. |
| Open Datasets | No | The paper describes how they systematically created a set of protocol models based on their e-commerce protocol for evaluation, but does not provide access information for this specific dataset. It states 'We systematically created a set of protocol models based on our e-commerce protocol for evaluation as follows2. We combined n number of copies of the base ecommerce protocol...' |
| Dataset Splits | No | The paper describes systematic creation of protocol models for evaluation but does not specify any training/test/validation dataset splits or cross-validation setup. |
| Hardware Specification | Yes | We run our experiments on a PC equipped with an Intel i7 3.0 GHz processor and 4GB RAM running 64-bit Windows 7 operating system. |
| Software Dependencies | No | The paper mentions 'implemented Algorithms 1 and 2' but does not specify any software dependencies with version numbers (e.g., Python version, specific libraries, model checkers, etc.). |
| Experiment Setup | No | The paper describes the creation of protocol models and mentions evaluating properties, but does not provide specific experimental setup details such as hyperparameters, learning rates, or optimizer settings, as it is not a machine learning paper in that sense. |