Program Complexity in Hierarchical Module Checking

Abstract

Module checking is a well investigated technique for verifying the correctness of open systems, which are systems characterized by an ongoing interaction with an external environment. In the classical module checking framework, in order to check whether an open system satisfies a required property, we first translate the entire system into an open model (module) that collects all possible behaviors of the environment and then check it with respect to a formal specification of the property.

Recently, in the case of closed system, Alur and Yannakakis have considered hierarchical structure models in order to have models exponentially more succinct. A hierarchical model uses as nodes both ordinary nodes and supernodes, which are hierarchical models themselves. For CTL specifications, it has been shown that for the simple case of models having only single-exit supernodes, the hierarchical model checking problem is not harder than the classical one. On the contrary, for the more general multiple-exit case, the problem becomes Pspace-complete.

In this paper, we investigate the program complexity of the CTL hierarchical module checking problem, that is, we consider the module checking problem for a fixed CTL formula and modules having also supernodes that are modules themselves. By exploiting an automata-theoretic approach through the introduction of hierarchical Büchi tree automata, we show that, in the single-exit case, the addressed problem remains in Ptime, while in the multiple-exit case, it becomes Pspace-complete.

Work partially supported by MIUR PRIN Project no.2007-9E5KM8 and grant “Formal Methods for Closed and Open Systems” ex-60% 2006 Università di Salerno.