Also wir brauchen noch ein paar Serialfüße, um den Zettel zu bewegen.

Ich erinnere mich an die Herrn Eskimo-Logik, die solche Modaloperatoren über die Aktionen des Systems indiziert hat.

Das ist z.B. der Box A.

Das heißt, für alle Art Transitionen, die ich machen kann, will das ich einen Zustand anschließend erreiche, der viel erfüllt.

An diesen drei Stellen dann viel, total, Dein und A.V. Ich kann eine Art Transition machen, mit der ich viel erreiche.

Das ist z.B. der Markt, der nicht viel erhaltet.

Das ist schöne Brute. Die Methodie ist, dass diese Logik für endlich verzweigende Systeme ausdrucksstark ist.

Was wir damit nicht machen können, ist das, was man unter ernsthafter Systemspezifikation versteht.

Das hier wäre eine Aktion Reset, die sagt, wir können auf den Knopf drücken, wenn das System abgestürzt ist, dann nehmen wir es wieder in konsistenten Zustand.

Das ist die verlehnende Datenreduktion.

So etwas hier wäre eine unangenehme Eigenschaft, die wir nicht wollen.

Wenn die Resetaktion blockiert ist, dass wir in einem Zustand sind, der so tot ist, dass wir nicht mehr den Resetknopf drücken können.

Das ist eine sehr schlache Spezifikation, das sagt nur, dass der Resetknopf nicht völlig geblockt ist.

Das ist nicht ausschließlich unangenehme Situationen, wie das Resetknopf zwar gedrückt werden kann, aber den Zustand nicht ändert.

Dann müsste man hier statt Truth noch etwas stärkeres hinterstrahlen.

Es wäre eine Eigenschaft des Systems, die wir bei diesen Resetknoppen sicher wollen, dass wir immer auf den Resetknopf drücken können.

Dieses immer, was ich in meinem Satz gerade verwendet habe, das gibt die Lupe bisher nicht her.

Ich kann mir eine Menge von Labels hernehmen, L in unserer Standard-Mutation, und hier verallgemeinerten Operator einführen, wo ich bisher nur Box A halte, hat er jetzt Box L hinschreiben, hat er das mit eingeführt.

Das hier kann ich definieren als Konjunktion über alle Aktionen in L von Box A phi.

Das heißt, ich verlange mit allen Aktionen aus L, erweiche ich über nur phi, Dual, also Diamond L phi, eine große Dysjunktion,

wiederum über alle A aus L, der Diamond Pha phi, das heißt also Diamond L phi bedeutet, ich habe eine Aktion aus L verfügbar, mit der ich keinen Zustand erreiche, der 4.

Wenn ich das schreibe, dann fällt eine ganze Menge der Gesamtregel dazu.

Da würde ich also verlangen, nicht nur, dass ich jetzt den Reset-Knopf drücken kann, denn nur das mag diese Formel, sondern ich würde zum Beispiel verlangen, dass wenn ich irgendeine Aktion brüche,

ich auf jeden Fall in einem Zustand lande, wo ich wieder den Reset-Knopf drücken kann. Fine, aber das sagt mir dann wieder nicht, was danach passiert, vielleicht bin ich dann ja, wenn ich noch einen Schritt mache, in einem Zustand, in dem der Reset-Knopf blockiert ist.

Gut, dann sage ich halt, wenn ich immer wieder eine Aktion mache und dann noch eine Aktion mache, dann will ich in einem Zustand sein, wo ich noch den Reset-Knopf drücken kann.

Naja, man sieht, dass das irgendwie nicht auf Dauer zielführend ist. Ich kann jetzt noch beliebig oft eben Ackd dahinschreiben, Box Ackd, aber wirklich Sicherheit des Systems werde ich damit nie spezifiziert kriegen,

wenn ich das 20 Mal ineinander hinschreibe, dann habe ich die Sicherheit des Systems für maximal 20 Schritte spezifiziert.

So, man sieht so eine Art Dekosion. Was man möchte ist sowas hier vielleicht, ich nenne eine Eigenschaft spezifizieren namens Safe und offenbar beinhaltet diese Eigenschaft unter anderem,

dass ich gerade jetzt den Reset-Knopf drücken kann, aber ich will das auch noch dann können, wenn eine weitere Aktion passiert, das heißt,

ich sage, egal wo ich dann im nächsten Schritt hin komme, soll das immer noch gelten. Dann muss jetzt also wieder Reset True und so weiter kommen, aber das kennen wir ja schon.

Das heißt, man versucht hier wieder Safe hinzuschreiben, also wo wir dann hinkommen, ist das immer noch sicher.

Ist das jetzt schon eine Spezifikation von Safe? Ist damit klar, was Safe heißt?

Na ja, wenn Safe jetzt nie erfüllt wird, dann hilft uns ja gar nichts.

Wenn Safe jetzt zum Beispiel, also eine Möglichkeit zu erfüllen wäre, also Safe ist einfach nie wahr, was für ein System wäre das tatsächlich eine Lösung dieser Gleichung?

Was wäre das eigentlich?

Zum Beispiel, also ein System, wo einfach nie Reset zugelassen ist, ist genau das Gegenteil von dem, was wir wollen.

In dem System wäre kein Zustand leer, aber in einem solchen System würde das ja auch sein, wie wir intendieren.

Also in einem System, wo ich überhaupt nicht auf den Reset-Knopf drücken kann, ist also sicher, dass Safe gleich leer ist, die Lösung, die wir da haben wollen, ist unsicher.

Genauer gesagt, kein sicheres Zustand. Okay, sagen wir mal, wir werden ein System, wo wir überall den Reset-Knopf drücken können, wäre dann immer auch mehr eine Lösung?

Im Prinzip schon, oder? Aber die Kondition wird dann auf der rechten Seite falsch.

Ja, vorsichtig, das ist nicht ganz voraussetzungsfrei.

Also hier steckt, also im Prinzip, das Vox Act, ja wohl gleich falsch sein müsste. Ist das immer so?

Ja, aber das muss sein, weil wir haben ja spezifiziert, dass wir Reset haben, also haben wir insbesondere immer mindestens die Reset-Aktion.

Ja, stimmt, das heißt, in diesem Fall, Reset gehört jetzt nicht extra zu, weil ich es einfach zugeben musste, vergessen. In der Tat, das ist dann voraussetzungsfrei. Also wenn wir voraussetzen, dass das System überall Reset sagen kann, dann ist leer in der Tat eine Lösung davon.

Okay, aber das ist also offenbar nicht das, was wir wollen. So, jetzt haben wir schon, also das da, ja, das ist ja, wenn man sich dann gewöhnt hat, in solchen Gruppen zu denken, eine Fixpunktplatte.

Ja, ich sage, Safe ist vielleicht irgendein komplexer Ausflug angewendet, auch Safe ist ein Fixpunktplatt. Okay, ja, also gerade gesehen, leer ist eine Lösung, die wir nicht wollen, also suchen wir anscheinend nicht den kleinsten Fixpunkt dieses Ausflugs.

Hier suchen wir also vielleicht, ja, wo kann man jetzt noch nicht ganz überlegen, also wenn es nicht der kleinste ist, ist es ja vielleicht der größte.

Ja, was ist der größte Fixpunkt dieser Gleiche?

Wir hocken alle Zustände, also dazu, wie wir unsere gewollten Ergebnisse beschreiben.

Also in einem System, das können wir mal überprüfen, sind in einem System, wo also alle Zustände schlechthin immer den Reset draufdrücken können. Ist da die Menge aller Zustände, ist das da ein Fixpunkt von dieser Gleichung?