Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions

This paper defines a formal framework for the modular and hierarchical model-checking of mu-calculus against modular transitions systems. Given a formula phi, a module can be analysed alone, in such a way that the truth value of phi may be decided without the need to analyse other modules. If no conclusion can be drawn locally, the analysis provides information allowing to reduce the module to a smaller one that is equivalent with respect to the truth value of phi. This way, modules can be incrementally analysed, reduced and composed to other reduced modules until a conclusion is reached. On the one hand, modular analysis allows to avoid modules compositions and thus the corresponding combinatorial explosion, on the other hand, hierarchical analysis allows to reduce the modules that must be composed, which limits combinatorial explosion. Moreover, by proposing three complementary formula-dependent reductions, we expect better reductions than general approaches like bisimulation or tau reductions. The current paper is focused on defining the theoretical tools for this approach, finding interesting strategies to apply them efficiently is left to future work.