Neue Frage
0

# 2013.10.07 : Question 6_e

gefragt 2017-08-22 18:42:24 +0100

Dieser Post ist als Wiki-Post markiert

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

aktualisiert 2017-08-22 18:42:24 +0100

arsinux Gravatar-Bild

Is this answer really sufficient? Bildbeschreibung

bearbeiten retag Als beleidigend melden schließen löschen

Kommentare

due to image uploading restrictions I can not upload the Automaton itself.

arsinux ( 2017-08-22 18:47:09 +0100 )bearbeiten

2 Antworten

1

geantwortet 2017-08-22 23:36:06 +0100

PS Gravatar-Bild

aktualisiert 2017-08-23 09:19:31 +0100

The answer given in the current solution that you mention is definitely not sufficient. The trouble is here that Auto is an existential nondeterministic $\omega$-automaton so that the alternation between the universal A and the existential quantification made by the $\omega$-automaton makes trouble. We therefore have to convert the $\omega$-automaton into a deterministic one or at least into a universal one for checking the property. As stated in the solution, that is not that easy in general.

In the particular example, however, only one transition is missing in the automaton to make it deterministic: in state {}, there is no input for {}. The acceptance condition is G[a SU m] which is equivalent to G(a$\vee$m) $\wedge$ G F m so that it follows that if in state {}, the missing input {} should be obtained, the acceptance condition is violated. We can therefore allow that additional input on the self-loop of state {} so that the automaton becomes a deterministic one this way. The acceptance condition will reject the added runs.

Having determined the automaton this way, the alternation problem is gone, and the question can be answered.

A direct way to answer to the problem without determination problems, would be to consider the language of accepted words of the automaton. As can be easily seen, it can only accept words where m is at most once false. Starting in state s1 of the Kripke structure, there is however a path s1,s2,s5,s2,s5,... that will infinitely often visit state s2 that cannot be accepted by the automaton. Hence, it is not true that all initial paths of the structure are accepted by the automaton.

bearbeiten Als beleidigend melden löschen publish Link mehr

Kommentare

The example solution has been changed after the question has been posed here.

PS ( 2017-08-23 13:31:36 +0100 )bearbeiten
0

geantwortet 2017-08-22 20:40:17 +0100

contradictioned Gravatar-Bild

The question is composed of two parts: (1) Check whether it holds and (2) explain your claim.

For checking whether it holds, you have to check if $A(Auto)$ holds. A wild guess would be, that it does not hold, and there is a simple example that you can use to show that, so the answer would be "it does not hold".

For explaining the claim, you have to say something like "on all paths Auto has to hold, however there is one where it does not hold".

What you answered does not fit the question, you answered a question along the lines of "Why is it harder to check $A \varphi$ than $E \varphi$"

bearbeiten Als beleidigend melden löschen publish Link 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]

Fragen-Tools

Beobachten
1 Follower

Statistik

Gefragt: 2017-08-22 18:42:24 +0100

Gesehen: 675 mal

Letztes Update: Aug 23