by Lutz Schröder and Dirk Pattinson
Abstract:
For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all mboxrank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatization, in PSPACE. This leads not only to a unified derivation of (known) tight PSPACE-bounds for a number of logics including K, coalition logic, and graded modal logic (and to a new algorithm in the latter case), but also to a previously unknown tight PSPACE-bound for probabilistic modal logic, with rational probabilities coded in binary. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.
Reference:
Lutz Schröder and Dirk Pattinson: PSPACE Bounds for Rank 1 Modal Logics, In Rajeev Alur, ed.: Logic in Computer Science (LICS 06), pp. 231–240, IEEE, 2006. Presentation slides available [preprint]
Bibtex Entry:
@InProceedings{SchroderPattinson06,
author = {Lutz Schr{\"o}der and Dirk Pattinson},
title = {PSPACE Bounds for Rank 1 Modal Logics},
year = {2006},
editor = {Rajeev Alur},
booktitle = {Logic in Computer Science (LICS 06)},
publisher = {IEEE},
pages = {231-240},
keywords = {coalgebra modal logic PSPACE shallow models},
url = {http://dx.doi.org/10.1109/LICS.2006.44},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/CMLpspace.pdf"> [preprint] </a>},
abstract = {For lack of general algorithmic methods that apply to wide classes of
logics, establishing a complexity bound for a given modal logic is often
a laborious task.
The present work is a step towards a general theory of the complexity of
modal logics.
Our main result is that all mbox{rank-1} logics enjoy a shallow model
property and thus are, under mild assumptions on the format of their
axiomatization, in PSPACE. This leads not only to a unified
derivation of (known) tight PSPACE-bounds for a number of logics
including K, coalition logic, and graded modal logic (and to a new
algorithm in the latter case), but also to a previously unknown tight
PSPACE-bound for probabilistic modal logic, with rational probabilities
coded in binary. This generality is made possible by a coalgebraic
semantics, which conveniently abstracts from the details of a given
model class and thus allows covering a broad range of logics in a
uniform way.
},
note = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/slides/rank1pspace.pdf">Presentation slides</a> available},
}