Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is (...) explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence. (shrink)

1.1 - Background - page 17 1.2 - The Style of Approach - page 18 1.3 - Motivation - page 19 1.4 - Style of Presentation - page 20 1.5 - Outline of the Thesis - page 21..