Resumé
| Originalsprog | Engelsk |
|---|---|
| Titel | Logic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings |
| Udgivelses sted | Heidelberg |
| Forlag | Springer |
| Publikationsdato | 2013 |
| Sider | 80-96 |
| ISBN (Trykt) | 978-3-642-36038-1 |
| ISBN (Elektronisk) | 978-3-642-36039-8 |
| DOI | |
| Status | Udgivet - 2013 |
| Navn | Lecture Notes in Computer Science |
|---|---|
| Vol/bind | 7750 |
| ISSN | 0302-9743 |
Citer dette
}
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
SP - 80
EP - 96
BT - Logic and Its Applications
PB - Springer
CY - Heidelberg
ER -