# Computational Accountability in MAS Organizations with ADOPT
## 4 The ADOPT Accountability Protocol
### Verifying ADOPT
#### 4.3.2 Reachability Property and Principles 4 and 5  
Principles 4 and 5, instead, concern goals, which are dynamic by nature. Specifically, Principle 4 states that an agent is only accountable for those goals for which it has taken an explicit commitment, whereas Principle 5 allows an agent to negotiate the provisions necessary for achieving a specific goal. The verification of these principles requires one to consider the dynamics of the accountability protocol, and overlaps with the _reachability_ property we are interested in verifying in ADOPT. Relying on CTLC, it is possible to express useful properties about commitment satisfaction, and hence, about the correctness of the ADOPT protocol. For instance, for each commitment \(C(i,j,\psi,\varphi)\) that is foreseen by the protocol, one can verify that when the commitment is created it can also be satisfied. This corresponds to expression of the following reachability property in CTLC: AF EF(createdC \(\rightarrow\) CC\((i,j,\psi,\varphi)\)), where createdC is an atomic proposition that becomes true when the given commitment \(C(i,j,\psi,\varphi)\) is created (i.e., when a specific message is sent by the debtor agent). This formula is valid if and only if in all the possible paths (i.e., runs of ADOPT), a state will be reached from which there exists at least one path along which either createdC is false (the commitment is not created), or createdC is true and the modality CC\((i,j,\psi,\varphi)\) will eventually be satisfied. Please recall that CC\((i,j,\psi,\varphi)\) is just a shortcut for \(\psi\rightarrow\) C\((i,j,\varphi)\). This formula is satisfied either when \(\psi\) is false, corresponding to the case in which the commitment expires (for example, released by the creditor); or when \(\psi\) is true and hence C\((i,j,\varphi)\) must hold. The latter corresponds to the case in which the commitment is, firstly, detached by the creditor and, then, satisfied by the debtor. Intuitively, this can be verified simply by looking at the sequence diagrams in Figures 1 and 2, and observing that whenever a commitment is created by a message of the debtor, the creditor has always the chance to release that commitment or detach it. Similarly, whenever a commitment is detached, the protocol encompasses at least a run along which the debtor can send a message whose meaning consists of the progression of that commitment to satisfaction.  
In short, it is possible to show that the above formula holds for every commitment that may arise in ADOPT. This means that in every possible run of ADOPT, there is always an execution path along which the conditional commitment \(C(i,j,\psi,\varphi)\), once created, can always be released by the creditor, or satisfied by the debtor. As a consequence, we can conclude that Principles 4 and 5 of the accountability requirements are actually satisfied, since the agent will have also the chance to agree to achieve a goal by creating a commitment (specifically C\({}_{4}\) of the goal-agreement phase), and by negotiating its provisions again via a commitment (specifically C\({}_{3}\)). An agent, thus, will only be accountable for the goals it has agreed upon, possibly having also established some necessary provisions.