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

Journal of Logic, Language and Information 11 (2):195-225 (2002)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 89,311

External links

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

Through your library


Added to PP

44 (#312,396)

6 months
2 (#634,891)

Historical graph of downloads
How can I increase my downloads?

References found in this work

A deduction model of belief.Kurt Konolige - 1986 - Los Atlos, Calif.: Morgan Kaufmann Publishers.
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.

View all 6 references / Add more references