Proving the validity of equations in GSOS languages using rule-matching bisimilarity (Q2883120)

GSOS (i.e., generalized structural operational semantics) rules specify the transitions that a process expression \(f(x_1,\dots,x_n)\) can make in terms of the transitions that the \(x_i\) can and/or cannot make. Here \(f\) is the process operator whose semantics is being defined. This paper considers the problem of proving that two process expressions that may contain uninstantiated process variables are equivalent, that is, for any instantiation of all variables, the resulting process expressions are bisimilar. The idea is to exhibit a bisimulation-like relation between the uninstantiated process expressions. The method is sound but not complete. To facilitate working at the uninstantiated level, GSOS rules are replaced by ``ruloids'' which specify the transitions of process contexts \(D[x1,\dots,x_n]\) instead of process expressions. Here \(D\) may be a more complicated expression than just a single operator like \(f\). The paper contains a theorem saying that for any finite set of GSOS rules, the relevant set of ruloids can be effectively constructed. The paper demonstrates that a number of process equations such as \((x;y);z = x;(y;z)\) can be proven with the method. It also presents initial results on subclasses for which the method is complete, and discusses extension to GSOS rules with predicates.