Tableaux-based decision method for single-agent linear time synchronous temporal epistemic logics with interacting time and knowledge

In Kamal Lodaya (ed.), Logic and its Applications. Springer. pp. 80--96 (2013)
Download Edit this record How to cite View on PhilPapers
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.
PhilPapers/Archive ID
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Added to PP index

Total downloads
48 ( #28,473 of 37,180 )

Recent downloads (6 months)
8 ( #28,953 of 37,180 )

How can I increase my downloads?

Monthly downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.