A bisimulation-based method for proving the validity of equations in GSOS languages

MaRDI QIDQ5150127zbMATH OpenFDO

Authors Luca Aceto, Matteo Cimini, Anna Ingolfsdottir

Publication date 9 February 2021

Full work available at URL http://eptcs.web.cse.unsw.edu.au/paper.cgi?SOS2009.1

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Proving the validity of equations in GSOS languages using rule-matching bisimilarity
• GSOS for probabilistic transition systems (extended abstract)
• Bisimilarity of open terms in stream GSOS
• On the bisimulation proof method
• Proving congruence of bisimulation in functional programming languages

Cited in

(7)

• Proving the validity of equations in GSOS languages using rule-matching bisimilarity
• Robustness of equations under operational extensions
• SOS rule formats for zero and unit elements
• Rule formats for distributivity
• On rule formats for zero and unit elements
• PREG axiomatizer -- a ground bisimilarity checker for GSOS with predicates
• Bisimilarity of open terms in stream GSOS

This page was built for publication: A bisimulation-based method for proving the validity of equations in GSOS languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5150127)