ICE-TCS Lectures Series - Matteo Cimini - A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages

An ICE-TCS  talk will be delivered on Friday, 23 October, by Matteo Cimini (Reykjavik University). The talk, entitled A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages, will be held in room K5 at Reykjavík University (Kringlan 1) from 14:00 till 15:00. 

Further information about forthcoming ICE- TCS events may be found on the ICE-TCS news page

Abstract

In this talk, I will present a bisimulation-based method for establishing the soundness of equations between 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 transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proven and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but I will offer offer some completeness results for restricted classes of GSOS specifications.