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

Mai Ajspur; Valentin Goranko

doi:10.1007/978-3-642-36039-8_8

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

Mai Ajspur, Valentin Goranko

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer 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.

Originalsprog	Engelsk
Titel	Logic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings
Udgivelsessted	Heidelberg
Forlag	Springer
Publikationsdato	2013
Sider	80-96
ISBN (Trykt)	978-3-642-36038-1
ISBN (Elektronisk)	978-3-642-36039-8
DOI	https://doi.org/10.1007/978-3-642-36039-8_8
Status	Udgivet - 2013

Navn	Lecture Notes in Computer Science
Vol/bind	7750
ISSN	0302-9743

Link til dokument

10.1007/978-3-642-36039-8_8

Citer dette

@inproceedings{f678d6623d614175a503ade5799ba3c1,

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

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{\textquoteright} 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.",

author = "Mai Ajspur and Valentin Goranko",

year = "2013",

doi = "10.1007/978-3-642-36039-8_8",

language = "English",

isbn = "978-3-642-36038-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "80--96",

booktitle = "Logic and Its Applications",

}

Ajspur, M & Goranko, V 2013, Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge. i Logic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings. Springer, Heidelberg , Lecture Notes in Computer Science, bind 7750, s. 80-96. https://doi.org/10.1007/978-3-642-36039-8_8

Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge. / Ajspur, Mai; Goranko, Valentin.
Logic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings. Heidelberg : Springer, 2013. s. 80-96 (Lecture Notes in Computer Science, Bind 7750).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

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

AU - Ajspur, Mai

AU - Goranko, Valentin

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-36039-8_8

DO - 10.1007/978-3-642-36039-8_8

M3 - Article in proceedings

SN - 978-3-642-36038-1

T3 - Lecture Notes in Computer Science

SP - 80

EP - 96

BT - Logic and Its Applications

PB - Springer

CY - Heidelberg

ER -

Ajspur M, Goranko V. Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge. I Logic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings. Heidelberg : Springer. 2013. s. 80-96. (Lecture Notes in Computer Science, Bind 7750). doi: 10.1007/978-3-642-36039-8_8