Differences

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

--- noforg [2016/06/07 20:07]
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$.
-However, we also want to modify the model $M$ to $M^\xi$, such that if the original formula holds in $M$ iff the transformed one holds in $M^\xi$.
+For simplicity, suppose we only have one such occurrence $\xi$.
-We schematically illustrate 4 such transformations.
+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 ======

pp-cb

User Tools

Site Tools

Differences

Page Tools