A Multi-Modal Framework for Achieving Accountability in Multi-Agent Systems

The authors present a multi-modal, model-theoretic framework for achieving accountability in multi-agent systems through formal proof. Their framework provides modalities for knowledge, provability, and time. With these modalities, they formalise the two main aspects of accountability, which are: soundness (accountability proper), i.e., for correct agents, the provability of their correctness by themselves; and completeness (auditability), i.e., for faulty agents, the eventual provability of their faultiness by others. In their framework, the accountability proof of a particular system is reduced to the proof of a few key lemmata, which the system designer needs to establish for a considered system.