
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 finitestate (module checking) and infinitestate
(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 Mucalculus), in
both the finitestate and infinitestate settings. Using an automatatheoretic
approach, we show that hybrid graded μcalculus module checking is solvable in
exponential time, while hybrid graded μcalculus pushdown module checking is
solvable in doubleexponential 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 Mucalculus 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/LMCS4(3:1)2008
Hit Counts: 5481 
Creative Commons  