Diferencias

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

Enlace a la vista de comparación

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
 
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki