Muestra las diferencias entre dos versiones de la página.

grupos:avispa:operational_semantics_of_tcc [2009/11/12 19:27] caolarte |
grupos:avispa:operational_semantics_of_tcc [2011/01/24 15:30] (actual) |
||
---|---|---|---|

Línea 1: | Línea 1: | ||

+ | ====== Operational Semantics of tcc ====== | ||

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

+ | |||

+ | {{ :grupos:avispa:sos.png |}} | ||

+ | |||

+ | 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: | ||

+ | - P ≡ Q if P and Q differ only by a renaming of bound variables (alpha-conversion). | ||

+ | - P || **skip** ≡ P. | ||

+ | - P || Q ≡ Q || P. | ||

+ | - 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>→ <sup>*</sup><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: | ||

+ | - F(**skip**) = **skip** | ||

+ | - F(**next** P) = P | ||

+ | - F(**unless** c **next** P) = P | ||

+ | - F(P1 || P2) = F(P1) || F(P2) | ||

+ | - F( (**local** x;c)P ) = (**local** x;true) P |