episciences.org_829_1652938401
1652938401
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
18605974
07
29
2008
Volume 4, Issue 3
Enriched MUCalculi Module Checking
Alessandro
Ferrante
Aniello
Murano
Mimmo
Parente
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 \mucalculus
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 \mucalculus module checking is solvable
in exponential time, while hybrid graded \mucalculus 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 \mucalculus enriched with inverse
programs (Fully enriched \mucalculus): 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.
07
29
2008
829
arXiv:0805.3462
10.48550/arXiv.0805.3462
10.2168/LMCS4(3:1)2008
https://lmcs.episciences.org/829

https://lmcs.episciences.org/829/pdf