Hierarchical and Recursive State Machines with Context-Dependent Properties

Hierarchical and recursive state machines are suitable abstract models for many software systems. In this paper we extend a model recently introduced in literature, by allowing atomic propositions to label all the kinds of vertices and not only basic nodes. We call the obtained models context-dependent hierarchical/recursive state machines. We study on such models cycle detection, reachability and Ltl model-checking. Despite of a more succinct representation, we prove that Ltl model-checking can be done in time linear in the size of the model and exponential in the size of the formula, as for standard Ltl model-checking. Reachability and cycle detection become NP-complete, and if we place some restrictions on the representation of the target states, we can decide them in time linear in the size of the formula and the size of the model.