# # 2013.10.07 : Question 6_e

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

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

bearbeiten retag schließen löschen

## Kommentare

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

## 2 Antworten

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

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.

mehr

## Kommentare

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

( 2017-08-23 13:31:36 +0200 )bearbeiten

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

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$"

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:42:24 +0200

Gesehen: 735 mal

Letztes Update: Aug 23 '17