Corina Cirstea ; Clemens Kupke ; Dirk Pattinson - EXPTIME Tableaux for the Coalgebraic mu-Calculus

lmcs:784 - Logical Methods in Computer Science, August 11, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:3)2011
EXPTIME Tableaux for the Coalgebraic mu-CalculusArticle

Authors: Corina Cirstea ORCID; Clemens Kupke ; Dirk Pattinson

    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.


    Volume: Volume 7, Issue 3
    Published on: August 11, 2011
    Imported on: April 26, 2010
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1, F.3.1, F.1.1
    Funding:
      Source : OpenAIRE Graph
    • Coalgebraic Modal Logic: Fixpoints and Nested Modalities; Funder: UK Research and Innovation; Code: EP/F031173/1

    14 Documents citing this article

    Consultation statistics

    This page has been seen 1445 times.
    This article's PDF has been downloaded 408 times.