Until-Operator

intf0rm
Erstie
Erstie
Beiträge: 13
Registriert: 19. Aug 2013 15:17

Until-Operator

Beitrag 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

Minker
Windoof-User
Windoof-User
Beiträge: 25
Registriert: 28. Sep 2009 16:11

Re: Until-Operator

Beitrag 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.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Until-Operator

Beitrag 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".

Antworten

Zurück zu „Archiv“