Combining epistemic logic and Hennessy-Milner logic

Sophia Knight, Radu Mardare, Prakash Panangaden

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Scopus citations

Abstract

We define an epistemic logic for labelled transition systems by introducing equivalence relations for the agents on the states of the labelled transition system. The idea is that agents observe the dynamics of the system modulo their ability to distinguish states and in the process learn about the current state and past history of the execution. This is in the spirit of dynamic epistemic logic but is a direct combination of Hennessy-Milner logic and epistemic logic. We give an axiomatization for the logic and prove a completeness theorem with respect to the class of models obtained by unfolding labelled transition systems.

Original languageEnglish (US)
Title of host publicationLogic and Program Semantics
Subtitle of host publicationEssays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday
EditorsRobert Constable, Alexandra Silva
Pages219-243
Number of pages25
DOIs
StatePublished - 2012
Externally publishedYes

Publication series

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

Fingerprint Dive into the research topics of 'Combining epistemic logic and Hennessy-Milner logic'. Together they form a unique fingerprint.

Cite this