# 2016.09.06 : Question6_b

gefragt 2017-08-22 18:19:12 +0100

Das ist ein Wiki-Beitrag. Jeder mit Karma >75 darf diesen Beitrag verbessern.

How the red signed part (in the picture) has been inferred? In the alt solution part : if 'a' hold in initial states, how can we solve it?

bearbeiten retag schließen löschen

1 Antwort

geantwortet 2017-08-22 21:06:56 +0100

Well, a simple answer to the question on the alternative solution: if a would hold on all initial states, then K $\models$ a ∨ A$\varphi$ would simply hold, since all initial states will satisfy "a", and thus also a ∨ A$\varphi$.

About the equivalence in the first part: That is difficult to explain in one step. It roughly goes through the following equivalences:

• K $\models A{\cal A}_\forall(Q,\varphi_I,\varphi_R,\varphi_F)$
• K,s $\models A{\cal A}_\forall(Q,\varphi_I,\varphi_R,\varphi_F)$ for all initial states s
• K,$\pi,0\models {\cal A}_\forall(Q,\varphi_I,\varphi_R,\varphi_F)$ for all initial paths $\pi$
• K,$\pi,0\models \neg{\cal A}_\exists(Q,\varphi_I,\varphi_R,\neg\varphi_F)$ for all initial paths $\pi$

Now, K,$\pi,0\models {\cal A}_\exists(Q,\varphi_I,\varphi_R,\neg\varphi_F)$ holds, if and only if the path $\pi$ is accepted by the $\omega$-automaton encoded by ${\cal A}_\exists(Q,\varphi_I,\varphi_R,\neg\varphi_F)$. This is the case if and only if the product structure of K and the automaton (or more precise with its associated Kripke structure) will have a path $\xi$ that satisfies $\varphi_I\wedge\neg\varphi_F$. Note that the paths in the product structure are composed of a path of the original structure K and also of a run through the automaton.

• $K_\times,\xi,0\models \neg(\varphi_I\wedge\neg\varphi_F)$ for all paths $\xi$ that contain some initial paths of K
• $K_\times,\xi,0\models \varphi_I\to\varphi_F$ for all paths $\xi$ that contain some initial paths of K
• $K_\times\models A(\varphi_I\to\varphi_F)$
• $K_\times\models\varphi_I\to A(\varphi_F)$

The last step holds since $\varphi_I$ is a propositional formula. These explanations just sketch a real proof, they are a bit unsound here and there, but I hope one can follow the general lines of the explanation.

mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

Statistik

Gefragt: 2017-08-22 18:19:12 +0100

Gesehen: 69 mal

Letztes Update: Aug 22 '17