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

J. Engelfriet, C.M. Jonker, J. Treur

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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. Finally, the possibility of incorporating default persistence of information in a system, is explored.
Original languageEnglish
Title of host publicationIntelligent Agents V: Agents Theories, Architectures, and Languages - 5th International Workshop, ATAL 1998, Proceedings
PublisherSpringer/Verlag
Pages177-194
Number of pages17
Volume1555
ISBN (Print)3540657134, 9783540657132
DOIs
Publication statusPublished - 1999
Event5th International Workshop on Agents Theories, Architectures, and Languages, ATAL 1998 - Paris, France
Duration: 4 Jul 19987 Jul 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1555
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

Workshop5th International Workshop on Agents Theories, Architectures, and Languages, ATAL 1998
CountryFrance
CityParis
Period4/07/987/07/98

Bibliographical note

Proceedings title: Intelligent Agents V Proc. of the Fifth International Workshop on Agent Theories, Architectures and Languages, ATAL'98
Publisher: Springer Verlag
Editors: J.P. Mueller, M.P. Singh, A.S. Rao

Fingerprint

Dive into the research topics of 'Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic'. Together they form a unique fingerprint.

Cite this