Alessandro Ferrante ; Aniello Murano ; Mimmo Parente - Enriched MU-Calculi Module Checking

lmcs:829 - Logical Methods in Computer Science, July 29, 2008, Volume 4, Issue 3 -
Enriched MU-Calculi Module Checking

Authors: Alessandro Ferrante ; Aniello Murano ; Mimmo Parente

    The model checking problem for open systems has been intensively studied in the literature, for both finite-state (module checking) and infinite-state (pushdown module checking) systems, with respect to Ctl and Ctl*. In this paper, we further investigate this problem with respect to the \mu-calculus enriched with nominals and graded modalities (hybrid graded Mu-calculus), in both the finite-state and infinite-state settings. Using an automata-theoretic approach, we show that hybrid graded \mu-calculus module checking is solvable in exponential time, while hybrid graded \mu-calculus pushdown module checking is solvable in double-exponential time. These results are also tight since they match the known lower bounds for Ctl. We also investigate the module checking problem with respect to the hybrid graded \mu-calculus enriched with inverse programs (Fully enriched \mu-calculus): by showing a reduction from the domino problem, we show its undecidability. We conclude with a short overview of the model checking problem for the Fully enriched Mu-calculus and the fragments obtained by dropping at least one of the additional constructs.

    Volume: Volume 4, Issue 3
    Published on: July 29, 2008
    Accepted on: June 25, 2015
    Submitted on: September 24, 2007
    Keywords: Computer Science - Logic in Computer Science,F.1.1,F.1.2,F.3.1,D.2.4

    Linked data

    Source : ScholeXplorer IsReferencedBy ARXIV 1607.03354
    Source : ScholeXplorer IsReferencedBy DOI 10.4204/eptcs.218.1
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1607.03354
    • 1607.03354
    • 10.48550/arxiv.1607.03354
    • 10.4204/eptcs.218.1
    • 10.4204/eptcs.218.1
    • 10.4204/eptcs.218.1
    Extended Graded Modalities in Strategy Logic
    Aminof, Benjamin ; Malvone, Vadim ; Murano, Aniello ; Rubin, Sasha ;

    5 Documents citing this article


    Consultation statistics

    This page has been seen 333 times.
    This article's PDF has been downloaded 205 times.