|
|
VOLUME 4, ISSUE 3, PAPER 1
|
Enriched μ-Calculi Module Checking
|
©Ferrante Alessandro, Universita' di Salerno
©Aniello Murano, Universita' di Napoli
©Mimmo Parente, Universita' di Salerno
|
Abstract
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 μ-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 μ-calculus module checking is solvable in
exponential time, while hybrid graded μ-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 μ-calculus enriched with inverse
programs (Fully enriched μ-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.
|
Publication date: July 30, 2008
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(3:1)2008
Hit Counts: 3412 |
 Creative Commons | |
