Differences

This shows you the differences between two versions of the page.

--- noforg [2016/06/01 15:03]
matei.popovici
+++ noforg [2016/06/30 16:45] (current)
matei.popovici
@@ Line 1: / Line 1: @@
+===== Strategy definition =====
+ $\hat{s}_A(\hat{h}) = s_A(h)$  (or equivalently  $=s_A(last(\hat{h}))$ ).
+===== Some examples =====
+In the induction step of  $\langle B \rangle \varphi$  where  $\varphi$  contains cooperation modalities, we want to replace each outermost occurrence of  $\xi = \langle A \rangle \gamma$  in  $\varphi$  by a proposition  $p_\xi$ .
+For simplicity, suppose we only have one such occurrence  $\xi$ .
+We also need to modify the model  $M$  to  $M^\xi$ , such that:
+   the original formula holds in  $M$  iff the transformed one holds in  $M^\xi$ .
+We schematically illustrate four such transformations on models.
+==== Example 1 ====
+In  $M$ ,  $\alpha$  is an action profile (action profiles are not illustrated if they are not important).
+Suppose  $012\models \langle A \rangle p$ . In the transformed model, we label state  $012$  by  $p_\xi$ .
+{{nf-1.jpg}}
+==== Example 2 ====
+In  $M$ ,  $\xi=\langle A \rangle G a$ . We have  $012^+ \models \xi$ . In the transformed model, we have an infinite number of states, each one corresponding to a history  $012..2$ . They are all labelled with  $p_\xi$ .
+{{nf-2.jpg}}
+==== Example 3 ====
+The model  $M$  shows that, in some situations, we may need to create states which do not correspond to histories per se.
+{{nf-3.jpg}}
+==== Example 4 ====
+Another interesting example.
+{{nf-4.jpg}}
 ===== Fixing tree proofs ======
 Let  $(M,q)$  be an iCGS and fix  $h\in\Lambda_M(q)$ . Let  $\xi=\langle A'​\rangle \gamma'​$  be an ATL formula where  $\gamma'​$  does not contain cooperation modalities. We construct the model  $(M^{\xi},​q)$  w.r.t.  $(M,q)$ ,  $\xi$  and  $h$ , as follows:
-  * Let  $h'​=hh''​$  (i.e.  $h'$  extends  $h$  by some history) be a history such that  $M,​h'​\models \xi$ .
+  - Let  $h'​=hh''​$  (i.e.  $h'$  extends  $h$  by some history) be a history such that  $M,​h'​\models \xi$ .
-  * We remove from  $M$  all states  $q = h''​[i]$  (i.e. all states from the extension  $h''​$ )
+  - We remove from  $M$  all states  $q = h''​[i]$  (i.e. all states from the extension  $h''​$ )
-  * For each  $h^*$  such that:
+  - For each  $h^*$  such that:
-    *  $h^*$  extends  $h$
+    -  $h^*$  extends  $h$
-    *  $last(h^*) = last(h'​)$
+    -  $last(h^*) = last(h'​)$
-  * create a unique state  $h^*$  in  $M^\xi$ . Each such state corresponds to a "road" starting with  $h$  and leading to the "point" where  $\xi$  holds.
+  - create a unique state  $h^*$  in  $M^\xi$ . Each such state corresponds to a "road" starting with  $h$  and leading to the "point" where  $\xi$  holds.
-  * add transitions exactly as in the unfolding.
+  - add transitions exactly as in the unfolding.
-  * add indistinguishability relations as in the unfolding.
+  - add indistinguishability relations as in the unfolding.
-  * Label this state  $h^*$  with all propositions in  $last(h^*)$ . Additionally, if  $h^*=h'​$ , label it with  $p_\xi$ .
+  - Label this state  $h^*$  with all propositions in  $last(h^*)$ . Additionally, if  $h^*=h'​$ , label it with  $p_\xi$ .
-  * This process is repeated for each  $h'$ , and "duplicate" states  $h^*$  can be "merged"
+  - This process is repeated for each  $h'$ , and "duplicate" states  $h^*$  can be "merged"
 The construction  $M^{\xi}$  //partially unfolds//  $M$ , and creates unique states for all histories starting with  $h$ , and ending with  $last(h'​)$ , for all  $h'$  satisfying the above condition.

pp-cb

User Tools

Site Tools

Differences

Page Tools