A general conservative extension theorem in process algebras with inequalities

Pedro R. d' Argenio, Chris Verhoef

    Research output: Book/Report › Report › Other research output

    10 Downloads (Pure)

    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, stage operator, priority, recursion, the silent step, autonomous actions, the empty process, divergence, etc.
    Original languageEnglish
    PublisherUniversity of Twente, Department of Computer Science
    Number of pages33
    Publication statusPublished - 1996

    Publication series

    NameMemoranda Informatica
    PublisherUniversity of Twente, Department of Computer Science
    No.96-17

    Fingerprint

    Extension Theorem
    Process Algebra
    Term Rewriting Systems
    Theorem
    Confluence
    Sufficient Conditions
    Transition Systems
    Recursion
    Modulo
    Completeness
    Divergence
    Corollary
    Discrete-time
    Projection
    Term
    Operator

    Keywords

    • FMT-PA: PROCESS ALGEBRAS
    • Structured operational semantics
    • Term deduction system
    • Transition system specification
    • Semantic equivalence
    • Semantic preorder
    • Algebraic system
    • Process algebra
    • Conservative extension

    Cite this

    d' Argenio, P. R., & Verhoef, C. (1996). A general conservative extension theorem in process algebras with inequalities. (Memoranda Informatica; No. 96-17). University of Twente, Department of Computer Science.
    d' Argenio, Pedro R. ; Verhoef, Chris. / A general conservative extension theorem in process algebras with inequalities. University of Twente, Department of Computer Science, 1996. 33 p. (Memoranda Informatica; 96-17).
    @book{e92838fc073e4249983c785a7d69f6c6,
    title = "A general conservative extension theorem in process algebras with inequalities",
    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, stage operator, priority, recursion, the silent step, autonomous actions, the empty process, divergence, etc.",
    keywords = "FMT-PA: PROCESS ALGEBRAS, Structured operational semantics, Term deduction system, Transition system specification, Semantic equivalence, Semantic preorder, Algebraic system, Process algebra, Conservative extension",
    author = "{d' Argenio}, {Pedro R.} and Chris Verhoef",
    year = "1996",
    language = "English",
    series = "Memoranda Informatica",
    publisher = "University of Twente, Department of Computer Science",
    number = "96-17",

    }

    d' Argenio, PR & Verhoef, C 1996, A general conservative extension theorem in process algebras with inequalities. Memoranda Informatica, no. 96-17, University of Twente, Department of Computer Science.

    A general conservative extension theorem in process algebras with inequalities. / d' Argenio, Pedro R.; Verhoef, Chris.

    University of Twente, Department of Computer Science, 1996. 33 p. (Memoranda Informatica; No. 96-17).

    Research output: Book/Report › Report › Other research output

    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 -

    d' Argenio PR, Verhoef C. A general conservative extension theorem in process algebras with inequalities. University of Twente, Department of Computer Science, 1996. 33 p. (Memoranda Informatica; 96-17).

    Access to Document