Enriched µ-Calculus Pushdown Module Checking

Abstract The model checking problem for open systems (called module checking ) has been intensively studied in the literature, both for finite–state and infinite–state systems. In this paper, we focus on pushdown module checking with respect to μ –calculus enriched with graded and nominals ( hybrid graded μ -calulus ). We show that this problem is decidable and solvable in double–exponential time in the size of the formula and in exponential time in the size of the system. This result is obtained by exploiting a classical automata–theoretic approach via pushdown nondeterministic parity tree automata. In particular, we reduce in exponential time our problem to the emptiness problem for these automata, which is known to be decidable in Exptime. As a key step of our algorithm, we show an exponential improvement of the construction of a nondeterministic parity tree automaton accepting all models of a formula of the considered logic. This result, not only allows our algorithm to match the known lower bound, but it is also interesting by itself, since it allows investigating decision problems related to enriched μ -calculus formulas in a greatly simplified manner. We conclude the paper with a discussion on the model checking w. r. t. μ -calculus formulas enriched with backward modalities as well.

Authors

• Alessandro Ferrante
• Aniello Murano
• Mimmo Parente

Keywords

No keywords are indexed for this paper.