Abstract We proposed a syntactical format, the _path_ format, for structured operational semantics in which predicates may occur. We proved that strong bisimulation is a congruence for all the operators that can be defined within the _path_ format. To show that this format is useful we provided many examples that we took from the literature about CCS, CSP, and ACP; they do satisfy the _path_ format but no formats proposed by others. The examples include concepts like termination, convergence, divergence, weak bisimulation, a zero object, side conditions, functions, real time, discrete time, sequencing, negative premises, negative conclusions, and priorities (or a combination of these notions).
Keywords and Phrases: structured operational semantics, term deduction system, transition system specification, structured state system, labelled transition system, strong bisimulation, congruence theorem, predicate.
1980 Mathematics Suject Classification (1985 Revision): 68Q05, 68Q55. CR Categories: D.3.1, F.1.1, F.3.2, F.4.3.
Note: Partial support received from the European Communities under CONCUR 2, BRA 7166.
Abstract 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 giving sufficient conditions for a system of operational rules and an extension ensuring that 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. As a first application of our conservativity results, we 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 other applications to show that our results are useful. The applications include (but are not limited to) various real and discrete time settings in \ccs, \acp, and \atp\ and the notions projection, renaming, state operator, priority, recursion, the silent step (both the weak and branching variants), and the empty process (or combinations of these notions).
Keyword Codes: F.1.2, F.3.2, F.4.3.
Keywords: Concurrency; Operational Semantics; Algebraic language theory.
Abstract We set up a formal framework to describe term deduction systems, such as transition system specifications in the style of Plotkin, and conditional term rewriting systems. This framework has the power to express many-sortedness, general binding mechanisms and substitutions, among other notions such as negative premises and unary predicates on terms.
The framework is used to present a conservativity format in operational semantics, which states sufficient criteria to ensure that the extension of a transition system specification with new rules does not affect the behaviour of the original terms.
Furthermore, we show how general theorems in structured operational semantics can be transformed into results in conditional term rewriting. We apply this approach to the conservativity theorem, which yields a result that is useful in the field of abstract data types.
Abstract 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, state operator, priority, recursion, the silent step, autonomous actions, the empty process, divergence, etc.
1980 Mathematics Suject Classification (1985 Revision): 68Q05, 68Q10, 68Q42, 68Q55, 03C05.
CR Categories: D.3.1, F.1.1, F.3.2, F.4.3.
Keywords: structured operational semantics, term deduction system, transition system specification, semantic equivalence, semantic preorder, algebraic system, process algebra, conservative extension.