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/rapportKonferencebidrag i proceedingsForskningpeer review

    Resumé

    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.
    OriginalsprogEngelsk
    TitelLogic and Its Applications : 5th Indian Conference, ICLA 2013, Chennai, India, January 10-12, 2013. Proceedings
    Udgivelses stedHeidelberg
    ForlagSpringer
    Publikationsdato2013
    Sider80-96
    ISBN (Trykt)978-3-642-36038-1
    ISBN (Elektronisk)978-3-642-36039-8
    DOI
    StatusUdgivet - 2013
    NavnLecture Notes in Computer Science
    Vol/bind7750
    ISSN0302-9743

    Citer dette

    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 (s. 80-96). Heidelberg : Springer. Lecture Notes in Computer Science, Bind. 7750 https://doi.org/10.1007/978-3-642-36039-8_8
    Ajspur, Mai ; Goranko, Valentin. / Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge. 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).
    @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’ 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",
    pages = "80--96",
    booktitle = "Logic and Its Applications",
    publisher = "Springer",

    }

    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/rapportKonferencebidrag i proceedingsForskningpeer 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 -

    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). https://doi.org/10.1007/978-3-642-36039-8_8