Structural model checking for communicating hierarchical machines

In this paper we consider the problem of model checking for well structured Communicating Hierarchical Machines (CHMs), i.e. Finite State Machines with additional features of hierarchy and concurrency. For model checking we follow the automaton theoretic approach, defining an algorithm which solves the problem of model checking without flattening the structure of CHMs. © Springer-Verlag 2004.