Eine Möglichkeit, LTL (Variante) auszudrücken, um zu erzwingen, dass ein Datenstrom einer linearen Zeitlogik entspricht

Question

Lineare Zeitlogik (LTL) wird verwendet für Systemüberprüfung.In meinem Fall investiere ich etwas Zeit, um die Machbarkeit der Verwendung von LTL dieses Mal zu prüfen, um eine Einschränkung für einen Datenstrom durchzusetzen.Genug der Allgemeingültigkeiten, nehmen wir ein einfaches Beispiel:

Der Betreiber BIS im Ausdruck u Until v bedeutet in LTL Ereignis u bis v, es ist eine allgemeine Formel, die eine unendliche Zahl von Signalspuren befriedigen könnte.Sehen Sie sich die Definition hier an:Seite 4

wie:

u,u,u,v,v,v,...
u,u,u,u,u,u,...
u,v,v,v,v,v,...

In meinem Fall möchte ich einem System, das einen Datenstrom empfängt, LTL-ähnliche Formeln aufzwingen.Nehmen wir wieder den gleichen Operator Until.

Nehmen wir an, wir haben zwei Eingangssignale, eines für die Konstante u und eines für die Konstante v.

u,u,u,u,u,u,...
 , , , ,v,v,...

Der Stream-Prozessor, der diese Eingaben entgegennimmt, würde, wenn es sich um einen „UNTIL*“-Knoten handelt, Folgendes ausgeben:

u,u,u,u,v,v,...

Der Grund, warum ich differenziere BIS mit einem Sternchen ist der springende Punkt der Frage: „u UNTIL* v“ ist nur wahr, wenn v als Ausgabe genommen wird, sobald es im zweiten Stream erscheint. Es handelt sich um eine einzelne Spur, die „u UNTIL* v“ angesichts unserer Anforderungen erfüllt Eingangssignale. Wie kann man diese Einschränkung ausdrücken?!LTL scheint für diesen „Mechanismus zur Durchsetzung von Einschränkungen“ sehr allgemein zu sein.

Notiz:Bitte haben Sie Verständnis, ich bin weder Informatiker noch Mathematiker, sondern ein durchschnittlicher Programmierer, der versucht, neue Dinge zu lernen.

Answer 1

Das ist eine interessante Frage.

Es handelt sich nicht direkt um eine LTL-Frage (Linear Temporal Logic), sondern vielmehr um die Frage, ob es einen Algorithmus oder ein Tool gibt, das einen Eingabestrom aufnimmt und ihn auf eine etwas minimale Weise modifiziert, um eine bestimmte LTL-Eigenschaft zu erfüllen.

Ob dies möglich ist oder bereits geschehen ist, hängt davon ab, welche Änderungen am Stream genau zulässig sind.In Ihrem Beispiel mischen Sie gewissermaßen zwei Streams neu.Beachten Sie, dass LTL über Alphabete definiert ist, in denen jedes Zeichen mehrere Aussagen haben kann, die zu diesem Zeitpunkt WAHR sind.In Ihrem Beispiel hätten Sie also einfach den U- und den V-Strom mischen können, um Folgendes zu erhalten:

u,u,u,u,{u,v},{u,v},....

Dies hätte auch die LTL-Formel erfüllt.Wenn Sie beim Remixen so vorgehen, dass der Satz im Ausgabestream immer eine Teilmenge der im Eingabestream festgelegten Sätze ist, können Sie ihn verwenden reaktive Synthese um einen Wandler zu erhalten, der das Mischen/Fixieren des Stroms übernimmt.Dies funktioniert jedoch nur, wenn es für jeden Ausgabestream tatsächlich eine Möglichkeit gibt, den Mix durchzuführen.

Wenn es eine quantitative Vorstellung von Mischen/Fixieren gibt, dann könnte die quantitative Synthese ein Forschungsgebiet sein, das zu einigen Ergebnissen führen könnte.Sie benötigen jedoch eine Beschreibung des genauen Optimierungskriteriums für die Stream-Modifikation, um festzustellen, ob eines der Ergebnisse aus diesem Bereich anwendbar ist.