pp-cb

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
===== 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$.
  - We remove from $M$ all states $q = h''[i]$ (i.e. all states from the extension $h''$)
  * For each $h^*$ such that:
    * $h^*$ extends $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.
  * add transitions exactly 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$.
  * 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.

**Lemma 1**
Fix $h$. $M,hh''\models \xi \iff M^{\xi},h\hat{h''}\models p_\xi$, where $\hat{h''} = h''[0]h''[0,1]h''[0,2]\ldots h''$.
The proof is similar to the base case $\varphi = \langle A\rangle \gamma$ from the paper.

We recursively define $M^{\{\xi_1,\ldots,\xi_k\}}$ as $(M^{\xi_1})^{\{\xi_2,\ldots,\xi_k\}}$.  

**Lemma 2**
Fix h and $X=\{\xi_1\ldots,\xi_k\}$. For all $\xi_i$:

$M,hh''\models {\xi_i} \iff M^X,h\hat{h''} \models p_{\xi_i}$

**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.




==== Old stuff (10 May) ====
Proof sample of Prop. 5.4. (case $\star$).

$M,h\circ\lambda, k \models \varphi$ iff $T,\hat{h}\circ\hat{\lambda},k\models \varphi$.

Case $\varphi = \langle A \rangle \gamma$ where $\gamma$ contains cooperation modalities. Let $\xi$ designate an arbitrary occurrence of $\langle A' \rangle \gamma'$ in $\gamma$. (for example $\varphi = \langle A \rangle F(p \wedge \langle A' \rangle\gamma')$).


For each $h'$ such that: 
  * $|h'| = k' \geq k$, 
  * $h'[0,k] = h$,
  * $M,h' \circ \lambda',k' \models \xi$

we perform the following relabelings:
  * for each $k \leq i< k'$: relabel each $h'[0,i]\in T$ and $last(h'[0,i])\in M$ with a new proposition $p^{h'}_\xi$.
  * relabel $h'\in T$ and $last(h)\in M$ with a new proposition $q^{h'}_\xi$.

We perform the following transformations on the formula $\varphi$: (unclear in the general case).
  * For example, $\langle A\rangle F (x \wedge \langle B \rangle\gamma)$ is transformed to:
  * $\langle A\rangle p_\xi \mathcal{U} (x \wedge q_\xi)$
  * For example, $\langle A\rangle G (x \wedge \langle B \rangle\gamma)$ is transformed to: ?!?!




==== IGNORE BELOW - Proof (9th May) ====
Proof sample of Prop. 5.4. (case $\star$).

$M,h\circ\lambda, k \models \varphi$ iff $T,\hat{h}\circ\hat{\lambda},k\models \varphi$.


Case $\varphi = \langle A \rangle \gamma$ where $\gamma$ contains cooperation modalities. Let $\xi$ designate an arbitrary occurrence of $\langle A' \rangle \gamma'$ in $\gamma$. (for example $\varphi = \langle A \rangle F(p \wedge \langle A' \rangle\gamma')$).

For each $h'$ such that: 
  * $|h'| = k' \geq k$, 
  * $h'[0,k] = h$,
  * $M,h' \circ \lambda',k' \models \langle A' \rangle\gamma'$

we relabel $h'\in T$ and $last(h')\in M$ with a new proposition $p_\xi$.
pp-cb

User Tools

Site Tools

Page Tools
