Seite 1 von 1

Until-Operator

Verfasst: 3. Mär 2014 21:53
von intf0rm
Hallo,

in der Vorlesung wurde mal gesagt, dass der Until-Operator auch nur mithilfe der temporal-logischen Konnektiven [] und <> geschrieben werden kann.
Meine Frage wäre, wie das geht. Ich würde folgendes vorschlagen: Statt (A U B) soll <>!A ==> <>[]B
geschrieben werden.
Vielen Dank schonmal.
vg

Re: Until-Operator

Verfasst: 3. Mär 2014 22:43
von Minker
Man kann [] und <> durch U ausdrücken. Um das nachzuvollziehen, kann man sich überlegen, dass die Semantik von A U B so definiert ist, dass unter anderem B auf jeden Fall irgendwann erfüllt sein muss, damit A U B erfüllt sein kann.
Dadurch kann man (<> phi) durch (true U phi) ausdrücken. Um auch [] auszudrücken, kann man benutzen, dass (![]phi <-> <>!phi). (siehe auch Folie 28 des Foliensatzes zur Linear Temporal Logic)
Der Vorschlag, dass man A U B durch <>!A ==> <>[]B ausdrücken kann, würde zulassen, dass es zwischen dem nicht Erfüllen von A und der Erfüllen von B noch weitere Zustände geben kann, was nicht der Semantik von U entspricht.

Re: Until-Operator

Verfasst: 4. Mär 2014 14:22
von Nathan Wasser
Um es noch deutlicher zu sagen: Until ist mächtiger als <> und []. Man kann den Until-Operator mit sicherheit nicht durch <> und/oder [] ausdrücken.

Nebenbei bedeutet "a U b", dass "b" irgendwann mindestens einmal gilt (und "a" muss in allen Zuständen gelten vor dem ersten Zustand in dem "b" gilt), und nicht etwa, dass "b" irgendwann immer gilt.

Ausserdem bedeutet "a U b" nicht unbedingt, dass "a" jemals gelten muss, sehr wohl aber "b".