Hierarchical predicate transition nets have recently been introduced as a visual formalism for specifying complex reactive systems. They extend predicate transition nets with hierarchical structures so that large systems can be specified and understood stepwisely, and thus are more suitable for real-world applications. In this paper, we provide a formal syntax and an algebraic semantics for hierarchical predicate transition nets, which establish the theory of hierarchical predicate transition nets for precise specification and formal reasoning.
