TY - BOOK

T1 - A general conservative extension theorem in process algebras with inequalities

AU - d' Argenio, Pedro R.

AU - Verhoef, Chris

PY - 1996

Y1 - 1996

N2 - We prove a general conservative extension theorem for transition system based process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem which gives sufficient conditions for a system of operational rules and an extension of it in order to ensure conservativity, that is, provable 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 we prove a completeness theorem. We also prove 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 equational process theory to a small term rewriting system under the condition that the large system is a conservative extension of the small one. We provide many applications to show that our results are useful. 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, autonomous actions, the empty process, divergence, etc.

AB - We prove a general conservative extension theorem for transition system based process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem which gives sufficient conditions for a system of operational rules and an extension of it in order to ensure conservativity, that is, provable 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 we prove a completeness theorem. We also prove 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 equational process theory to a small term rewriting system under the condition that the large system is a conservative extension of the small one. We provide many applications to show that our results are useful. 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, autonomous actions, the empty process, divergence, etc.

KW - FMT-PA: PROCESS ALGEBRAS

KW - Structured operational semantics

KW - Term deduction system

KW - Transition system specification

KW - Semantic equivalence

KW - Semantic preorder

KW - Algebraic system

KW - Process algebra

KW - Conservative extension

M3 - Report

T3 - Memoranda Informatica

BT - A general conservative extension theorem in process algebras with inequalities

PB - University of Twente, Department of Computer Science

ER -