Compositional verification of multi-agent systems in temporal multi-epistemic logic

Abstract

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.

Download options

PhilArchive



    Upload a copy of this work     Papers currently archived: 72,856

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
42 (#274,373)

6 months
1 (#386,040)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Adding a Temporal Dimension to a Logic System.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
Minimal Temporal Epistemic Logic.Joeri Engelfriet - 1996 - Notre Dame Journal of Formal Logic 37 (2):233-259.
Specification of Nonmonotonic Reasoning.Joeri Engelfriet & Jan Treur - 2000 - Journal of Applied Non-Classical Logics 10 (1):7-26.

Add more references