A GENERAL CONSERVATIVE EXTENSION THEOREM IN-PROCESS ALGEBRAS WITH INEQUALITIES

We prove a general conservative extension theorem for transition syste m based process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem which gives suffic ient conditions for a system of operational rules and an extension of it in order to ensure conservativity, that is, provable transitions fr om an original term in the extension are the same as in the original s ystem. As a simple corollary of the conservative extension theorem we prove a completeness theorem. We also prove a general theorem giving s ufficient conditions to reduce the question of ground confluence modul e some equations for a large term rewriting system associated with an equational process theory to a small term rewriting system under the c ondition that the large system is a conservative extension of the smal l one. We provide many applications to show that our results are usefu l. The applications include (but are not limited to) various real and discrete time settings in ACP, ATP, and CCS and the notions projection , renaming, stage operator, priority, recursion, the silent step, auto nomous actions, the empty process, divergence, etc.