// Trust models for user-centric networks from // M. Kwiatkowska, D. Parker and A. Simaitis // Strategic analysis of trust models for user-centric networks. // In: Proc. SR’13. EPTCS, vol. 112, pp. 53–60 (2013) // (have simplified the reward structures) // originally based on the trust model of // A. Bogliolo, P. Polidori, A. Aldini, W. Moreira, P. Mendes, M. Yildiz, C. Ballester, and J.-M. Seigneur. // Virtual Currency and Reputation-Based Cooperation Incentives in User-Centric Networks. // In: Proc. IWCMC-2012, Cyprus, 2012 // turn-based stochastic game smg const int K; // number of services const int td; // trust model // model parameters const double alpha_all = 0.8; // recommendation influence parameter const int st_init_all = med; // initial service trust for all providers const int reduct_all = td; // trust decrease for all providers const bool hide_all = false; // allow information hiding const double cancel = 0.05; // probability to cancel fair request const bool init_know_all = true; // sharing of initial trust const double die_prob = 0; // probability provider dies after serving a request const int cmax = 10; // maximum service cost const int cmin = 2; // minimum service cost player requester1 requester1, [pay11], [nopay11], [pay21], [nopay21], [pay31], [nopay31], [try11], [try21], [try31], [buy] endplayer player provider1 provider1, [accept11], [refuse11], [reveal11], [notreveal11] endplayer player provider2 provider2, [accept21], [refuse21], [reveal21], [notreveal21] endplayer player provider3 provider3, [accept31], [refuse31], [reveal31], [notreveal31] endplayer // probability to share information formula rev_prob = know21&(trust11>trust21) | know31&(trust11>trust31) ? 0 : 1; module requester1 x1 : [0..43] init 0; // states of the module //ns1 : [0..K] init 0; // number of requested services ps1 : [0..K] init 0; // number of payed services nps1 : [0..K] init 0; // number of unpayed services unpaid1 : bool init false; // choose service provider [try11] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=11) & (unpaid1'=false); [try21] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=21) & (unpaid1'=false); [try31] x1=0 & (y1+y2+y3=0) & ps1+nps1 < K -> (x1'=31) & (unpaid1'=false); // or buy the service off-market [buy] x1=0 & (y1+y2+y3=0) -> (x1'=41) & (unpaid1'=false); // finished sending requests [] x1=0 & (y1+y2+y3=0) & (ps1+nps1=K) -> (x1'=1) & (unpaid1'=false); [] x1=1 -> true; // reply from first requester and then decide to pay or not [accept11] x1=11 -> (x1'=12); [refuse11] x1=11 -> (x1'=13); [pay11] x1=12 -> (x1'=0) & (ps1'=min(K,ps1+1)); [nopay11] x1=12 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); [] x1=13 -> (x1'=0); // reply from second requester and then decide to pay or not [accept21] x1=21 -> (x1'=22); [refuse21] x1=21 -> (x1'=23); [pay21] x1=22 -> (x1'=0) & (ps1'=min(K,ps1+1)); [nopay21] x1=22 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); [] x1=23 -> (x1'=0); // reply from third requester and then decide to pay or not [accept31] x1=31 -> (x1'=32); [refuse31] x1=31 -> (x1'=33); [pay31] x1=32 -> (x1'=0) & (ps1'=min(K,ps1+1)); [nopay31] x1=32 -> (x1'=0) & (nps1'=min(K,nps1+1)) & (unpaid1'=true); [] x1=33 -> (x1'=0); // finish paying off-market [] x1=41 -> (x1'=0) & (ps1'=min(K,ps1+1)); endmodule label "finished" = x1=1; // requester finished // factor alpha of the cost formula const double alpha1 = alpha_all; const double alpha2 = alpha_all; const double alpha3 = alpha_all; // trust formula formula trusteq1 = min(top, !know21 & !know31 ? trust11 : floor(alpha1*trust11 + (1-alpha1)*recommend)); formula recommend = ((know21 ? trust21 : 0) + (know31 ? trust31 : 0)) / ((know21 ? 1 : 0) + (know31 ? 1 : 0)); // initial knowledge parameters const bool init_know11 = init_know_all; const bool init_know21 = init_know_all; const bool init_know31 = init_know_all; // initial trust parameters const int dt_init1 = st_init_all; // dispositional trust const int st_init1 = st_init_all; // service trust level const int trust_init1 = dt_init1; // initial trust const int tth_init1 = high; // trust threshold (see the cost formula) const int dt_init2 = st_init_all; const int st_init2 = st_init_all; const int trust_init2 = dt_init2; const int tth_init2 = high; const int dt_init3 = st_init_all; const int st_init3 = st_init_all; const int trust_init3 = dt_init3; const int tth_init3 = high; // trust reduction rates (0:NULL; 1:-1; 2:-2) const int reduct1 = reduct_all; const int reduct2 = reduct_all; const int reduct3 = reduct_all; // enable information withholding // info about requester 1 const bool hide11 = hide_all; const bool hide21 = hide_all; const bool hide31 = hide_all; module provider1 alive1 : bool init true; y1 : [0..4] init 0; // states of the module st1 : [0..level] init st_init1; // service trust level dt1 : [0..level] init dt_init1; // dispositional trust tth1 : [0..level] init tth_init1; // trust threshold (see the cost formula) trust11 : [0..level] init trust_init1; // trust towards the requester know11: bool init init_know11; // interaction flag // initiate connection with requester [try11] alive1 & (y1=0) -> ((trusteq1 < st1) ? 1 : 0) + ((trusteq1 < st1) ? 0 : 1) * cancel : (y1'=4) + (1-(((trusteq1 < st1) ? 1 : 0) + ((trusteq1 < st1) ? 0 : 1) * cancel)) : (y1'=3); [try11] !alive1 & y1=0 -> (y1'=4); // accept or refuse requester1 [accept11] (y1=3) & (trusteq1 >= st1) -> (y1'=1); //[refuse11] (y1=4) & (trusteq1 < st1) -> (y1'=0); [refuse11] (y1=4) -> (y1'=0); // settle payment with requester1 [pay11] (y1=1) -> (y1'=2) & (trust11' = (trust11 < top ? trust11+1 : top)); [nopay11] (reduct1=1) & (y1=1) -> (y1'=2) & (trust11' = (trust11 > null ? trust11-1 : null)); [nopay11] (reduct1=2) &(y1=1) -> (y1'=2) & (trust11' = (trust11 > null ? trust11-2 : null)); [nopay11] (reduct1=0) & (y1=1) -> (y1'=2) & (trust11'=null); // decide to reveal info about requester to other providers or not [reveal11] (y1=2) -> (1-die_prob) * rev_prob : (y1'=0) & (know11'=true) + (1-die_prob) * (1-rev_prob) : (y1'=0) & (know11'=false) + die_prob : (y1'=0) & (alive1'=false) & (trust11'=trust_init1) & (know11'=false); [notreveal11] hide11 & (y1=2) -> (y1'=0) & (know11'=false); endmodule module provider2 = provider1 [y1=y2, st1=st2, dt1=dt2, tth1=tth2, trust11=trust21, know11=know21, alive1=alive2, alpha1=alpha2, trust21=trust11, know21=know11, // renaming parameters trust formula dt_init1=dt_init2, st_init1=st_init2, trust_init1=trust_init2, tth_init1=tth_init2, try11=try21, init_know11=init_know21, accept11=accept21, refuse11=refuse21, pay11=pay21, nopay11=nopay21, reduct1=reduct2, reveal11=reveal21, notreveal11=notreveal21, hide11=hide21] endmodule module provider3 = provider1 [y1=y3, st1=st3, dt1=dt3, tth1=tth3, trust11=trust31, know11=know31, alive1=alive3, alpha1=alpha3, trust31=trust11, know31=know11, // renaming parameters trust formula dt_init1=dt_init3, st_init1=st_init3, trust_init1=trust_init3, tth_init1=tth_init3,try11=try31, init_know11=init_know31, accept11=accept31, refuse11=refuse31, pay11=pay31, nopay11=nopay31, reduct1=reduct3, reveal11=reveal31, notreveal11=notreveal31, hide11=hide31] endmodule // trust level aliases const int level = 10; const int null = 0; const int low = 2; const int med = 5; const int high = 8; const int top = 10; // highest price in the market formula max_price = max((trust11 < tth1) ? cmin + ceil(((cmax - cmin) / tth1) * (tth1 - trust11)) : cmin, (trust21 < tth2) ? cmin + ceil(((cmax - cmin) / tth2) * (tth2 - trust21)) : cmin, (trust31 < tth3) ? cmin + ceil(((cmax - cmin) / tth3) * (tth3 - trust31)) : cmin); //formula max_price = cmax; // maximum difference between trust // changed to action reward formula max_diff = max(max(trust11-trust21,trust21-trust11), max(trust11-trust31,trust31-trust11), max(trust21-trust31,trust31-trust21)); // cost of obtaining services rewards "cost" !unpaid1 & y1=2 : (trust11 < tth1) ? cmin + ceil(((cmax - cmin) / tth1) * (tth1 - trust11)) : cmin; !unpaid1 & y2=2 : (trust21 < tth2) ? cmin + ceil(((cmax - cmin) / tth2) * (tth2 - trust21)) : cmin; !unpaid1 & y3=2 : (trust31 < tth3) ? cmin + ceil(((cmax - cmin) / tth3) * (tth3 - trust31)) : cmin; x1=41 : max_price; endrewards // obtain an paid service rewards "payed" !unpaid1 & y1=2 : 1; !unpaid1 & y2=2 : 1; !unpaid1 & y3=2 : 1; endrewards // obtain an unpaid service rewards "nopayed" unpaid1 & y1=2 : 1; unpaid1 & y2=2 : 1; unpaid1 & y3=2 : 1; endrewards // total services rewards "accepted" [accept11] true : 1; [accept21] true : 1; [accept31] true : 1; endrewards