The search functionality is under construction.
The search functionality is under construction.

Keyword Search Result

[Keyword] full abstractness(1hit)

1-1hit
  • Fully Abstract Models for Communicating Processes with respect to Weak Linear Semantics with Divergence

    Eiichi HORITA  

     
    PAPER

      Vol:
    E75-D No:1
      Page(s):
    64-77

    The semantics of a language for communicating processes is investigated, and three full abstractness results for are established. The language contains atomic actions, termination, inaction, sequential composition, alternative composition, parallel composition, action restriction, and a form of guarded recursion. (The guardedness restriction on recursion is needed to establish one of the full abstractness results.) Three Plotkin-style operational semantics WL, CWL, and IWL of the language are defined. These semantics are linear in that the meaning of each program in any of these semantics is a set of action sequences the program may perform, and are weak in that the action sequences are obtained by ignoring (finte sequences of) internal moves. All the three semantics distinguish divergence (an infinite sequence of internal moves) from deadlock. The semantics IWL differs from the other two in that IWL is a so-called interal action semantics taking into account only internal moves under the assumption that the environment allows no (external) communication actions, and hence, the only possible actions for processes are internal moves, whereas the other two semantics take into account communication actions in addition to internal moves. The two semantics WL and CWL differ each other in that CWL is a so- called completed trace semantics, whereas WL is not. Then, two compositional models RF and IRF for the language are proposed, and the full a bstractness of RF (resp. of IRF) w. r. t. WL and CWL (resp. w. r. t. IWL), as expressed in the following, is established:s1s2(*) S[][S[]is a context of ⇒S[s1]S[s2]],where ,RF,WL, RF,CWL, IRF,IWL. A similar full abstractness result has been established by Bergstra, Klop, and Olderog for a language without recursion or internal moves. Moreover, Rutten investigated the semantics of a language similar to , in the framework of complete metric spaces, and showed that the failures model is fully abstract w. r. t. a strong linear semantics L, where L is strong in that it does not abstract from internal moves. The full abstractness of RF w. r. t. CWL, expressed in (*) with ,RF,CWL, is an extension of the result of Bergstra et al. to a language with recursion and internal moves. Also, the full abstractness of IRF w. r. t. IWL, expressed in (*) with ,IRF,IWL, is an extension of the Rutten's result, to the case of weak linear semantics with divergence.