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/01 14:52] 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 ====== | ===== 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 $(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'$ | + | - This process is repeated for each $h'$, and "duplicate" states $h^*$ can be "merged" |
| - | The construction $M^{\xi}$ //partially unfolds// $M$, from all histories starting with $h$, up to $last(h')$, for all $h'$ satisfying the above condition. | + | 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. |
| **Lemma 1** | **Lemma 1** | ||
| Line 23: | Line 57: | ||
| **Lemma 2** | **Lemma 2** | ||
| - | Fix h and $X=\{xi_1\ldots,\xi_k\}$. For all $\xi_i$: | + | Fix h and $X=\{\xi_1\ldots,\xi_k\}$. For all $\xi_i$: |
| - | $M,hh''\models {\xi_i} \iff M^X,h\hat{h''} p_{\xi_i}$ | + | $M,hh''\models {\xi_i} \iff M^X,h\hat{h''} \models p_{\xi_i}$ |
| - | **Fixing Proposition 5.4.** | + | **Fixing the proof of Proposition 5.4.** |
| In the induction step, instead of transforming $M$ by relabelling states, we transform $M$ to $M^{X}$ where $X$ contains the outermost occurrences of cooperation modalities in $\gamma$. In the resulting model, these formulae hold in exactly the same partially-unfolded histories, so we can apply the induction step. | In the induction step, instead of transforming $M$ by relabelling states, we transform $M$ to $M^{X}$ where $X$ contains the outermost occurrences of cooperation modalities in $\gamma$. In the resulting model, these formulae hold in exactly the same partially-unfolded histories, so we can apply the induction step. | ||
noforg.1464781953.txt.gz · Last modified: 2016/06/01 14:52 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
