## Paper: PSPACE reasoning for coalgebraic modal logic (at LICS 2006)

**Lutz Schröder 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 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.

### BibTeX

@InProceedings{SchrderPattinson-PSPACEreasoningforc, author = {Lutz Schröder and Dirk Pattinson}, title = {PSPACE reasoning for coalgebraic modal logic}, booktitle = {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)}, year = {2006}, month = {August}, pages = {231--240}, location = {Seattle, Washington, USA}, publisher = {IEEE Computer Society Press} }