Rewriting for Preorder Relations

Preorders are often used as a semantic tool in various fields of computer science. Examples in this direction are the preorder semantics defined for process algebra formalisms, such as testing preorders and bisimulation preorders. Preorders turn out to be useful when modelling divergence or partial specification. In this paper we present some results on the possibility of associating to a preorder theory, presented via a set of equality axioms and ordering ones, an equivalent rewriting relation which, together with a proof strategy, allows the decidability of the preorder relation. Our approach has been developed in the framework of a project whose main goal is to develop a verification system for process algebra formalisms based on equational reasoning.