EXPTIME tableaux for the coalgebraic mu-calculus

Corina Cirstea, Clemens Kupke, Dirk Pattinson

Research output: Contribution to journalArticle

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.
LanguageEnglish
Article number3
Number of pages33
JournalLogical Methods in Computer Science
Volume7
Issue number3
DOIs
Publication statusPublished - 11 Aug 2011

Fingerprint

Computability and decidability
μ-calculus
Tableaux
Modal Logic
Fixpoint
Semantics
Concretes
Coalitions
Logic
Probabilistic Logic
Tableau
Decidability
Parity
Completeness
Calculus
Game
Unknown
Operator
Framework
Class

Keywords

  • coalgebra
  • modal logic
  • tableau-based decision procedures
  • EXPTIME
  • coalgebraic approach

Cite this

@article{56c73c2473af475f82a37de7f58fd825,
title = "EXPTIME tableaux for the coalgebraic mu-calculus",
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.",
keywords = "coalgebra, modal logic, tableau-based decision procedures, EXPTIME, coalgebraic approach",
author = "Corina Cirstea and Clemens Kupke and Dirk Pattinson",
year = "2011",
month = "8",
day = "11",
doi = "10.2168/LMCS-7(3:3)2011",
language = "English",
volume = "7",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "3",

}

EXPTIME tableaux for the coalgebraic mu-calculus. / Cirstea, Corina; Kupke, Clemens; Pattinson, Dirk.

In: Logical Methods in Computer Science, Vol. 7, No. 3, 3, 11.08.2011.

Research output: Contribution to journalArticle

TY - JOUR

T1 - EXPTIME tableaux for the coalgebraic mu-calculus

AU - Cirstea, Corina

AU - Kupke, Clemens

AU - Pattinson, Dirk

PY - 2011/8/11

Y1 - 2011/8/11

N2 - 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.

AB - 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.

KW - coalgebra

KW - modal logic

KW - tableau-based decision procedures

KW - EXPTIME

KW - coalgebraic approach

UR - http://www.lmcs-online.org/ojs/viewarticle.php?id=687&layout=abstract

U2 - 10.2168/LMCS-7(3:3)2011

DO - 10.2168/LMCS-7(3:3)2011

M3 - Article

VL - 7

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

M1 - 3

ER -