The importance of formal methods for ensuring extreme high reliability requirements of safety and mission critical systems is widely known, but mature formal methods for concurrent and distributed systems are still lacking. Hierarchical predicate transition nets for system specifications and temporal logic techniques for analyzing predicate transition nets have recently been developed. This research furthers previous work with the following objectives: 1) to define an algebraic semantics of hierarchical predicate transition nets in order to carry out various algebraic transformations; 2) to design a more usable and powerful specification methodology to facilitate the practical applications of hierarchical predicate transition nets to realworld systems; 3) to develop a variety of effective analysis techniques to ensure the correctness of hierarchical predicate transition net specifications. This research represents a significant step towards a solid understanding of hierarchical predicate transition nets and their relationship with other specification methods and will lay the foundation of a new and effective formal specification and verification methodology for concurrent and distributed systems based on hierarchical predicate transition nets.
