Skip to main navigation Skip to search Skip to main content

Decidable extensions of Hennessy-Milner Logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a new class of logics for specifying and model-checking properties of distributed systems – Dynamic Epistemic Spatial Logics. They have been designed as extensions of Hennessy-Milner logic with spatial operators (inspired by Cardelli-Gordon-Caires spatial logic) and epistemic operators (inspired by dynamic-epistemic logics). Our logics focus on observers, agents placed in different locations of the system having access to some subsystems. Treating them as epistemic agents, we develop completely axiomatized and decidable logics that express the information flow between them in a dynamic and distributed environment. The knowledge of an epistemic agent, is understood as the information, locally available to our observer, about the overall-global system.
Original languageEnglish
Title of host publicationFormal Techniques for Networked and Distributed Systems - FORTE 2006
EditorsE. Najm, J. F. Pradat-Peyre, V. V. Donzeau-Gouge
Pages196-211
Number of pages16
Volume4229
ISBN (Electronic)978-3-540-46220-0
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743

Keywords

  • Hennessy-Milner logic
  • modelling
  • distributed systems
  • Cardelli-Gordon-Caires spatial logic
  • epistemic operators
  • epistemic agent

Fingerprint

Dive into the research topics of 'Decidable extensions of Hennessy-Milner Logic'. Together they form a unique fingerprint.

Cite this