EXPTIME tableaux for the coalgebraic mu-calculus
Cirstea, Corina and Kupke, Clemens and Pattinson, Dirk (2011) EXPTIME tableaux for the coalgebraic mu-calculus. Logical Methods in Computer Science, 7 (3). 3. ISSN 1860-5974 (https://doi.org/10.2168/LMCS-7(3:3)2011)
PDF.
Filename: 1105.2246.pdf
Accepted Author Manuscript Download (383kB) |
Abstract
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus and for an extension of coalition logic with fixpoints.
-
-
Item type: Article ID code: 44694 Dates: DateEvent11 August 2011PublishedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 02 Sep 2013 12:50 Last modified: 11 Nov 2024 10:28 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/44694