This work is licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works License. A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages∗

This paper presents a bisimulation-based method for establishing the soundness of equations be-tween terms constructed using operations whose semantics is specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone’s FH-bisimilarity and uses tran-sition rules as schematic transitions in a bisimulation-like relation between open terms. The sound-ness of the method is proven and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but the article offers some completeness results for restricted classes of GSOS specifications.