noforg
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
noforg [2016/06/07 20:09] 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 ===== | ===== Some examples ===== | ||
| Line 8: | Line 12: | ||
| the original formula holds in $M$ iff the transformed one holds in $M^\xi$. | the original formula holds in $M$ iff the transformed one holds in $M^\xi$. | ||
| - | We schematically illustrate four such transformations. | + | We schematically illustrate four such transformations on models. |
| ==== Example 1 ==== | ==== 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}} | {{nf-1.jpg}} | ||
| ==== Example 2 ==== | ==== 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}} | {{nf-2.jpg}} | ||
| ==== Example 3 ==== | ==== 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}} | {{nf-3.jpg}} | ||
| ==== Example 4 ==== | ==== Example 4 ==== | ||
| + | Another interesting example. | ||
| {{nf-4.jpg}} | {{nf-4.jpg}} | ||
| ===== Fixing tree proofs ====== | ===== Fixing tree proofs ====== | ||
noforg.1465319397.txt.gz ยท Last modified: 2016/06/07 20:09 by matei.popovici
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 3.0 Unported
