Operational Semantics of tcc

The following table summarizes the internal and observable transition relations for tcc.

Let us describe the internal reduction rules:

  • The rule RTell says that the process tell( c ) adds c to the current store d, via conjunction, and evolves into skip.
  • The rule RPar is the standard interleaving rule for parallel composition.
  • Let Q = local (x;c) P in Rule RLoc. The global store is d and the local store is c. We distinguish between the external (corresponding to Q) and the internal point of view (corresponding to P). From the internal point of view, the information about the variable x, possibly appearing in the global store d , cannot be observed. Thus, before reducing P we first hide the information about x that Q may have in d by existentially quantifying x in d. Similarly, from the external point of view, the observable information about x that the reduction of internal agent P may produce (i.e., c') cannot be observed. Thus we hide it by existentially quantifying x in c' before adding it to the global store. Additionally, we make c' the new private store of the evolution of the internal process.
  • Since the process P=unless c next Q executes Q in the next time unit only if the final store at the current time unit does not entail c, in the rule RUnl P evolves into skip if the current store d entails c.
  • Rule RRep dictates that the process !P produces a copy of P at the current time unit, and then persists in the next time unit.
  • Rule RAsk describes the behavior of P=when c do Q. If the current store d entails c, then the process Q is executed.
  • Let ≡ be the smallest congruence satisfying:
    1. P ≡ Q if P and Q differ only by a renaming of bound variables (alpha-conversion).
    2. P || skip ≡ P.
    3. P || Q ≡ Q || P.
    4. P || (Q || R) ≡ (P || Q) || R.

If P≡Q and c is logically equivalent to d, we say that <P,c>≡<Q,d>. Rule RStr says that structurally congruent configurations have the same reductions.

The seemingly missing rules for the processes next P and unless c next P (when c cannot be entailed from the current store) are given by the rule RObs. This rule says that an observable transition from P labeled with (c,d) is obtained from a terminating sequence of internal transitions of the form <P,c>→ *<Q,d>. The process R to be executed in the next time interval is equivalent to F(Q) (the “future” of Q). The process F(Q) is obtained by removing from Q any local information that has been stored in Q, and by “unfolding” the sub-terms within next and unless expressions. More precisely:

  1. F(skip) = skip
  2. F(next P) = P
  3. F(unless c next P) = P
  4. F(P1 || P2) = F(P1) || F(P2)
  5. F( (local x;c)P ) = (local x;true) P
grupos/avispa/operational_semantics_of_tcc.txt · Última modificación: 2011/01/24 15:30 (editor externo)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki