Formalizing Group and Propagated Trust in Multi-Agent Systems
Authors: Nagat Drawel, Jamal Bentahar, Amine Laarej, Gaith Rjoub
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 6 Implementation and Experimental Results To support the modeling and verification of BT logic for MASs, we implemented the transformation procedure and developed a tool that automatically: (i) transforms a given BT model and formulae to a valid CTL model and formulae; (ii) interacts with the Nu SMV model checker in order to perform the verification process. For testing, we used the well-known ordering protocol that regulates the interaction between seller and buyer agents introduced in [Desai et al., 2005]. Our motivation is to formalize the protocol requirements using BT model Mb and by expressing a set of properties in BT logic in order to assess the scalability of our technique. We expressed a set of group and propagated trust properties. For example, the formula EF ET (Group, Seller, EF Deliver Goods), checks whether or not there exists a possibility that every member in the group trusts the seller for delivering the requested goods. We measured the transformation times of the models and formulae along with the verification time in seconds and memory usage in megabyte when running on a machine Intel(R) Core(TM) i7-6700 CPU 3.40GHZ with 16 GB memory. We run our experiments with a number of agents ranging from 3 to 66. We considered different numbers of agents to achieve different levels of scalability that makes the problem complex enough to observe significant results. The verification results in Table1 reveal that the number of reachable states reflecting the size of the model increases exponentially with the number of agents, while the space increase is only polynomial. This confirms the PSPACE complexity result. Moreover, the execution time (i.e., the transformation time of both the models and formulae, and the time of the verification process) shows a clear polynomial increase up to 33 agents. After 33, the increase rate is much higher but still polynomial with the number of states, which is inline with the fact that PSPACE=APTIME. |
| Researcher Affiliation | Academia | Nagat Drawel , Jamal Bentahar , Amine Laarej and Gaith Rjoub Concordia University, Montreal, Canada n_drawe@encs.concordia.ca, bentahar@ciise.concordia.ca, laarej.amine@gmail.com, g_rjoub@encs.concordia.ca |
| Pseudocode | Yes | Algorithm 1 Transform Mb = (Sb, Rb, Ib, i,j |(i, j) Agt2}, Vb) into Mc = (Sc, Ic, Rc, Vc) |
| Open Source Code | No | The paper mentions 'we implemented the transformation procedure and developed a tool' but does not provide any link or explicit statement that the source code is publicly available. |
| Open Datasets | No | The paper states 'For testing, we used the well-known ordering protocol that regulates the interaction between seller and buyer agents introduced in [Desai et al., 2005]'. This refers to a case study protocol, not a typical dataset with explicit access information or train/test splits. The paper conducts formal verification, not data-driven machine learning. |
| Dataset Splits | No | The paper describes a formal verification and model checking approach, not machine learning experiments involving data splits for training, validation, or testing. |
| Hardware Specification | Yes | We measured the transformation times of the models and formulae along with the verification time in seconds and memory usage in megabyte when running on a machine Intel(R) Core(TM) i7-6700 CPU 3.40GHZ with 16 GB memory. |
| Software Dependencies | No | The paper mentions 'interacts with the Nu SMV model checker' but does not provide a specific version number for this software dependency. |
| Experiment Setup | Yes | For testing, we used the well-known ordering protocol that regulates the interaction between seller and buyer agents introduced in [Desai et al., 2005]. We run our experiments with a number of agents ranging from 3 to 66. |