Enriched MU-Calculi Module Checking

Details Enriched MU-Calculi Module Checking Enriched MU-Calculi Module Checking

2008-05-22

arxiv.org/abs/0805.3462v2

LMCS 4 (3:1) 2008

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-4(3:1)2008

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.

Affiliated with

Also associated with

No associations

Rating

Enriched MU-Calculi Module Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Enriched MU-Calculi Module Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Enriched MU-Calculi Module Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-511051