Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

Compositional verification aims at managing the complexity of the verification process by exploiting compositionality of the system architecture. In this paper we explore the use of a temporal epistemic logic to formalize the process of verification of compositional multi-agent systems. The specification of a system, its properties and their proofs are of a compositional nature, and are formalized within a compositional temporal logic: Temporal Multi-Epistemic Logic. It is shown that compositional proofs are valid under certain conditions. Moreover, the possibility of incorporating default persistence of information in a system, is explored. A completion operation on a specific type of temporal theories, temporal completion, is introduced to be able to use classical proof techniques in verification with respect to non-classical semantics covering default persistence. © 2002 Kluwer Academic Publishers.