ProMoca: Probabilistic Modeling and Analysis of Agents in Commitment Protocols

Authors: Akın Günay, Yang Liu, Jie Zhang

JAIR 2016 | Venue PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental Finally, we present empirical results about efficiency and scalability of Pro Moca. We substantially extend our earlier preliminary experimental result (G unay et al., 2015), by conducting a detailed empirical study to validate Pro Moca s practical usefulness and scalability in three well-studied scenarios from the literature, namely aerospace aftercare, international insurance (Jakob, Pˇechouˇcek, Miles, & Luck, 2008), and Net Bill (Sirbu & Tygar, 1995). Our results show that Pro Moca outperforms the state-of-the-art general purpose probabilistic model checker PRISM when verifying compliance and goal satisfaction properties of an agent s behavior in the context of a commitment protocol. In Section 5, we present an empirical evaluation of our framework.
Researcher Affiliation Academia Akın G unay EMAIL Yang Liu EMAIL Jie Zhang EMAIL School of Computer Science and Engineering Nanyang Technological University, Singapore
Pseudocode Yes Algorithm 1: Function update(V, assignments, C) returns the updated valuation V. Algorithm 2: Function update-subscription(V, c) returns the updated valuation V. Algorithm 3: Function fulfillment(V, c, C) updates the valuation V with respect to fulfillment of commitment c. Algorithm 4: Computation of reachability probabilities for target states.
Open Source Code No The paper states: "We implement Pro Moca framework in PAT (Process Analysis Toolkit) (Sun, Liu, Dong, & Pang, 2009)..." and mentions comparing with PRISM. However, there is no explicit statement or link indicating that the source code for Pro Moca's methodology is publicly available.
Open Datasets No The paper states: "We substantially extend our earlier preliminary experimental result (G unay et al., 2015), by conducting a detailed empirical study to validate Pro Moca s practical usefulness and scalability in three well-studied scenarios from the literature, namely aerospace aftercare, international insurance (Jakob, Pˇechouˇcek, Miles, & Luck, 2008), and Net Bill (Sirbu & Tygar, 1995)." and "AGFIL: This example models a real world car insurance claim processing case (Desai et al., 2009)." These refer to scenarios, case studies, and existing protocols rather than concrete datasets with explicit access information.
Dataset Splits No The paper describes using case studies and scenarios with control parameters to vary model complexity, but it does not involve traditional datasets with specified training, validation, or test splits for reproduction.
Hardware Specification Yes We run our experiments on a PC equipped with an Intel i7 3.0 GHz processor and 8GB RAM, running an 64-bit Windows 8 operating system.
Software Dependencies No The paper mentions implementing Pro Moca in PAT (Process Analysis Toolkit) (Sun, Liu, Dong, & Pang, 2009) and comparing it with PRISM (Kwiatkowska, Norman, & Parker, 2011). However, it does not specify version numbers for either PAT or PRISM.
Experiment Setup No The paper describes using "control parameters" (e.g., number of months, customers, claims) to vary the size and complexity of the Pro Moca models for evaluation. It does not provide specific experimental setup details such as hyperparameters, learning rates, batch sizes, or optimizer settings, as it is a model checking framework rather than a machine learning model requiring such configurations.