In this paper, a set of useful refinement rules on hierarchical predicate transition nets (HPrTNs in the sequel) is presented. These rules help a user to develop a large HPrTN in a stepwise approach supporting both top-down and bottom-up development styles. Furthermore, we have shown that these rules either preserve or facilitate the verification of many system behavioral properties. Another nice feature of these rules is that their applications always result in a valid partial view and an extended and integrated definition of the original HPrTN. We also briefly discuss related works on refinement techniques based on Petri nets and other specification methods.
