On Syntactic and Semantic Action Refinement

M. Hagiya (Editor), U. Goltz, J.C. Mitchell (Editor), R. Gorrieri, Arend Rensink

    Research output: Contribution to conferencePaperpeer-review

    10 Citations (Scopus)
    177 Downloads (Pure)


    The semantic definition of action refinement on labelled event structures is compared with the notion of syntactic substitution, which can be used as another notion of action refinement in a process algebraic setting. This is done by studying a process algebra equipped with the ACP sequential composition, parallel composition with an explicit synchronisation set, and an operator for action refinement. On the one hand, the language (including the refinement operator) is given a flow event structure semantics. On the other hand, a reduction procedure transforms a process term P into a flat term (i.e., with the refinement operator not occurring in it) red(P) by means of syntactic substitution, defined in a structural inductive way. The main aim of the paper is to find general conditions under which the terms P and red(P) have the same semantics. The results we present are essentially dependent on the question whether the refined action can be synchronised or not. In the latter case, P and red(P) give rise to isomorphic flow event structures under mild assumptions. The former case is considerably more difficult. We give necessary and sufficient semantic conditions under which refinement can be distributed over synchronisation up to isomorphic domains of configurations. Subsequently we also give sufficient (but not necessary) syntactic conditions for reducible terms.
    Original languageUndefined
    Number of pages20
    Publication statusPublished - 1994
    EventInternational Symposium on Theoretical Aspects of Computer Software, TACS 1994 - Sendai, Japan
    Duration: 19 Apr 199422 Apr 1994


    ConferenceInternational Symposium on Theoretical Aspects of Computer Software, TACS 1994
    Abbreviated titleTACS


    • EWI-8251
    • IR-66641

    Cite this