Sebastian Enqvist ; Fatemeh Seifan ; Yde Venema - An expressive completeness theorem for coalgebraic modal mu-calculi

lmcs:3756 - Logical Methods in Computer Science, July 3, 2017, Volume 13, Issue 2 -
An expressive completeness theorem for coalgebraic modal mu-calculiArticle

Authors: Sebastian Enqvist ; Fatemeh Seifan ; Yde Venema

    Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor. We then consider invariance under behavioral equivalence of MSO-formulas. More specifically, we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of the monadic second-order language for a given functor. Using automatatheoretic techniques and building on recent results by the third author, we show that in order to provide such a characterization result it suffices to find what we call an adequate uniform construction for the coalgebraic type functor. As direct applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem for the modal mu-calculus, avoiding the use of syntactic normal forms, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors (including the "game functor"). As a more involved application, involving additional non-trivial ideas, we also derive a characterization theorem for the monotone modal mu-calculus, with respect to a natural monadic second-order language for monotone neighborhood models.

    Volume: Volume 13, Issue 2
    Published on: July 3, 2017
    Accepted on: July 3, 2017
    Submitted on: July 3, 2017
    Keywords: Computer Science - Logic in Computer Science
      Source : OpenAIRE Graph
    • Logic and Automata: a Coalgebraic perspective; Code: 612.001.115

    Consultation statistics

    This page has been seen 1271 times.
    This article's PDF has been downloaded 306 times.