Language Preorder as a Precongruence

Groote and Vaandrager introduced the tyft format, which is a congruence format for strong bisimulation equivalence. This article proposes additional syntactic requirements on the tyft format, extended with predicates, to obtain a precongruence format for language preorder. 1 Introduction Structural operational semantics [20] is a popular method to provide formal languages, process algebras, and specification languages with an interpretation. It is based on the use of transition systems. Given a set of states, the transitions between these states are obtained inductively from a transition system specification (TSS), which consists of transition rules. Validity of the (positive) premises of such a rule, under a certain substitution, implies validity of the conclusion of this rule under the same substitution. This article considers transition systems in which states are the closed terms generated by a single-sorted first-order signature, and transitions are supplied with labels. Labelled..