Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge

Mai Ajspur, Valentin Goranko

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between time and knowledge. We discuss some complications that occur, even in the single-agent case, when interactions between time and knowledge are assumed and show how the method of incremental tableaux can be adapted to work in EXPSPACE, respectively 2EXPTIME, for these logics, thereby also matching the upper bounds obtained for them by Halpern and Vardi.
Original languageEnglish
Title of host publicationLogic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings
PublisherSpringer
Publication date2013
Pages80-96
ISBN (Print)978-3-642-36038-1
ISBN (Electronic)978-3-642-36039-8
DOIs
Publication statusPublished - 2013
Event5th Indian Conference on Logic and its Applications (ICLA 2013) - Chennai, India
Duration: 10 Jan 201312 Jan 2013
http://www.imsc.res.in/~icla/

Conference

Conference5th Indian Conference on Logic and its Applications (ICLA 2013)
CountryIndia
CityChennai
Period10/01/201312/01/2013
Internet address
SeriesLecture Notes in Computer Science
Volume7750
ISSN0302-9743

Fingerprint Dive into the research topics of 'Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge'. Together they form a unique fingerprint.

Cite this