Neue Frage
2

Omega Automata language translation

gefragt 2017-08-22 21:26:56 +0100

blackmamba Gravatar-Bild

I am having trouble doing translations for finite many subwords:

α contains only finitely many subwords aa
α contains only finitely many subwords a!a and !aa
bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

3

geantwortet 2017-08-22 22:31:52 +0100

PS Gravatar-Bild

aktualisiert 2017-08-23 09:25:09 +0100

Consider any infinite path $\pi$ of a Kripke structure over the variables {a} $\cup V$. We consider it as an infinite word, and each state label, i.e., a set of variables, is considered as a letter of the word. If at some point of time t, we have $K,\pi,t\models a \wedge X a$, we have an occurrence of a subword aa at position t. If that should be found only finitely often, we have to state that after some finite time, it will never be the case. The latter is expressed as a persistence property, so that we get $FG\neg(a\wedge Xa)$.

In many cases (exam questions), the task continues by the construction of some $\omega$-automata. Even if not directly asked for, it is often way better to directly construct deterministic automata so that their negation and other boolean operations are simple. The direct construction of deterministic automata can be done by using only past temporal operators with the basic safety, liveness, persistence and fairness templates.

In the above example, I would therefore rather recommend the equivalent formula $FG\neg$(a $\wedge$ PWX a) or also $FG\neg$(a $\wedge$ PWX a). The standard translation will then give you a DetFG automaton with only one state variable.

The answer to your second question is clearly $FG\neg(\neg a\wedge Xa)$ and the same comments apply for the past operators and the construction of deterministic automata.

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 21:26:56 +0100

Gesehen: 54 mal

Letztes Update: Aug 23