10.2168/LMCS-4(3:1)2008
https://lmcs.episciences.org/829
Ferrante, Alessandro
Alessandro
Ferrante
Murano, Aniello
Aniello
Murano
Parente, Mimmo
Mimmo
Parente
Enriched MU-Calculi Module Checking
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.
episciences.org
Computer Science - Logic in Computer Science
F.1.1
F.1.2
F.3.1
D.2.4
2015-06-25
2008-07-29
2008-07-29
eng
journal article
arXiv:0805.3462
10.48550/arXiv.0805.3462
1860-5974
https://lmcs.episciences.org/829/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 4, Issue 3
Researchers
Students