Architectures and time with recursive hierarchical alternating transition systems

Statecharts have been proposed as a powerful and concise language to specify the behavior of reactive systems. We have used statecharts in the context of the conception and implementation of reactive systems and discovered some limitations of the formalism. We describe some of these limitations and propose a new variant on the statecharts model, which we call recursive hierarchical alternating transition systems automata. We claim that recursive hierarchical alternating transition systems automata are more intuitive and have cleaner semantics than statecharts. We show how recursive hierarchical alternating transition systems automata can be used to model architectures of hierarchical control systems such as those used in flexible manufacturing systems. Furthermore, time information can be added to the architecture to reflect communication delays in the system. This information can be used to verify correctness and responsiveness constraints for the system