# Computational Accountability in MAS Organizations with ADOPT
## 4 The ADOPT Accountability Protocol
### Verifying ADOPT  
We now verify the correctness of the ADOPT protocol discussed above. To this end, we have to verify two aspects: first, the adherence of ADOPT to the five principles we have identified as necessary conditions for accountability; and second, the satisfaction of some fundamental properties that any good protocol should possess, specifically _safety_ and _liveness_ conditions. According to the literature about protocol verification [51; 52; 53], safety means that a protocol never enters an unacceptable state, whereas liveness, strictly related to state reachability, means that the protocol always progresses towards its completion. As usual in protocol verification, we will turn to a temporal logic for formalizing and validating the protocol dynamics. In particular, the verification of ADOPT has to be focused on the treatment of the commitments that are created along the interaction, since these encode the relations upon which the accountability is established. Intuitively, we have to demonstrate that ADOPT allows the commitments to progress towards satisfaction. This demands for logics that are capable of handling commitments directly. [PERSON] et al. [PERSON] et al. (2018) have proposed a temporal logic, named CTLC (i.e., computation-tree logics with commitments), which is an extension of CTL ([PERSON], 2018) with a modality operator for social commitments. In addition, the authors show how commitment-based protocols, specified in CTLC, can be checked by resorting to existing model-checking engines. Specifically, CTLC can be reduced to CTLK ([PERSON], 2018), an epistemic logic on branching time whose calculus has been implemented in the MCMAS model checker ([PERSON], 2018). In a nutshell, the CTLC syntax is as follows:  
\[\varphi:=p\mid\
eg\varphi\mid\varphi\vee\varphi\mid\mathtt{EX}\varphi\mid \mathtt{EG}\varphi\mid\mathtt{E}(\varphi\mathtt{U}\varphi)\mid\mathtt{C}(i,j, \varphi),\]  
where \(p\) is an atomic proposition, and where the temporal modalities have the same semantics as in CTL. For example, \(\mathtt{EX}\varphi\) means that \"there is a path where \(\varphi\) holds at the next state in the path\", whereas \(\mathtt{EG}\varphi\) means that \"there is a path where \(\varphi\) holds in every state along that path\". Finally, \(\mathtt{E}(\varphi_{1}\mathtt{U}\varphi_{2})\) means that \"there is a path along which \(\varphi_{1}\) holds in every state until \(\varphi_{2}\) holds\". The same shortcuts defined for CTL are also valid in CTLC: \(\
eg\mathtt{EX}\
eg\varphi\equiv\mathtt{AX}\varphi\) can be read as \"\(\varphi\) holds in all the next states reachable from the current one\"; \(\
eg\mathtt{EF}\
eg\varphi\equiv\mathtt{AG}\varphi\): \"\(\varphi\) holds in every state of each path outgoing from the current state\"; and \(\
eg\mathtt{EG}\
eg\varphi\equiv\mathtt{AF}\varphi\): \"\(\varphi\) will eventually hold in every path outgoing from the current state\". The peculiar characteristic of CTLC is the modality \(\mathtt{C}(i,j,\varphi)\), that is read: \"agent \(i\) commits towards agent \(j\) to bring about proposition \(\varphi\)\". Since the modality operator only tackles base commitments, a conditional commitment \(\mathtt{C}(i,j,\psi,\varphi)\) must be reduced to the formula \(\psi\rightarrow\mathtt{C}(i,j,\varphi)\), and in the following we will use \(\mathtt{CC}(i,j,\psi,\varphi)\) as a shortcut of such a reduction. The interpretation of a CTLC formula is based on Kripke models where a specific accessibility relation \(R_{sc}\) is defined for the commitment modality \(\mathtt{C}\). Providing a detailed reporting of the CTLC semantics is out of the scope of this paper. For our purposes, it is sufficient to say that a commitment modality \(\mathtt{C}(i,j,\varphi)\) is satisfied in a model \(M\) at a state \(w\) iff \(\varphi\) is true in every accessible state from \(w\) using the accessibility relation \(R_{sc}\). For the sake of readability, we will just report some of the formulas that have actually been used for the verification of the ADOPT protocol.