Ready, Set, Go: Structural Operational Semantics for Linear-Time Process Algebras

We investigate the relationship between operational semantics, equational semantics, and ready equivalence (a well-known relative of failure equivalence and testing equivalence) in process algebra. We give a class of structural operational semantic rules, called winterized rules, which define operations respecting ready equivalence. The class of winterized rules is surprisingly broad; it includes some copying operations which would seem to violate ready equivalence. Membership in this class is decidable in $O(n^{2})$ time. We show that for any process algebra defined by such rules has complete equational axiom system. These methods - winterizability in particular - apply mutatis mutandis to other linear-time process equivalences