Trace rewriting systems

We first describe a finite state machine based module interface specification method — trace assertion method. Then, viewing trace assertions in a trace specification as defining an equivalence relation among traces, we define a trace rewriting system from the specification. Such a trace rewriting system resembles some aspects of string rewriting, membership conditional rewriting and priority rewriting. We prove that a proper trace rewriting system is both terminating and confluent and compare trace rewriting systems with term rewriting systems.