General Conservative Extension Theorem in Process Algebra

摘要

The authors proved a general conservative extension theorem for transition systembased process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem giving sufficient conditions for a system of operational rules and an extension ensuring that outgoing transitions from an original term in the extension are the same as in the original system. As a simple corollary of the conservative extension theorem, the authors proved a completeness theorem. As a first application of their conservativity results, the authors proved a general theorem giving sufficient conditions to reduce the question of ground confluence modulo some equations for a large term rewriting system associated with an equation process theory to a small term rewriting system under the condition that the large system is a conservative extension of the small one. The authors proved many other applications to show that the results are useful. The applications include (but are not limited to) various real and discrete time settings in Calculus of Communicating Systems (CCS), Algebra of Communicating Processes (A CP), and Algebra of Timed Processes (ATP), and the notions projection, renaming, state operator, priority, recursion, the silent step, and the empty process.