Zeitliche Logik

Die zeitliche Logik ist ein Zweig der mathematischen Logik und insbesondere der Modallogik , die auf verschiedene Weise formalisiert wird. Das gemeinsame Merkmal dieser Formalisierungen liegt in der Hinzufügung von Modalitäten (mit anderen Worten von „Prädikatentransformatoren“), die mit der Zeit verbunden sind; Eine typische Formel der Modallogik ist beispielsweise die Formel , die lautet: "Die Formel ist erfüllt, bis die Formel erfüllt ist". Dies bedeutet, dass versucht werden soll, sicherzustellen, dass eine bestimmte Eigenschaft (hier ) für die gesamte zuvor ausgeführte Zeit erfüllt ist eine andere Formel (hier) ist erfüllt . ${\ displaystyle \ phi \ mathrm {U} \ psi}$ $\ phi$ $\ psi$ $\ phi$ $\ psi$

Aus semantischer Sicht bedeutet dies, dass der Begriff der Wahrheit in diesen Logiken die Entwicklung der Welt berücksichtigt. Das heißt, ein Satz kann an einem Punkt erfüllt sein und später nicht mehr.

Es wurden verschiedene Formalisierungen der zeitlichen Logik beschrieben, wobei verschiedene grundlegende Modalitäten berücksichtigt wurden.

Zeitliche Logik wird häufig in der formalen Verifikation verwendet , wo die grundlegende Technik im Wesentlichen die Modellprüfung ist . Man kann zum Beispiel ausdrücken, dass ein gefährliches Ereignis erst dann eintreten darf, wenn eine bestimmte Sicherheitsbedingung erfüllt ist.

Definition

In diesem Artikel wird nur die Berechnung zeitlicher Sätze vorgestellt, dh eine Berechnung zeitlicher Sätze, die durch zeitliche Modalitäten ergänzt werden und dennoch als "zeitliche Logik" bezeichnet werden.

Diese Logiken werden auf einer Reihe von Atomsätzen P oder Satzvariablen definiert. Diese atomaren Aussagen sind durch eine bestimmte Anzahl von logischen Verknüpfungen kombiniert mit den üblichen Anschlüssen: und , oder , nicht , Implikation , wie auch andere Betreiber genannt Modalitäten. Die zeitliche Logik ist daher eine modale Logik. Im Fall der linearen zeitlichen Logik (LTL) fügen wir die folgenden Modalitäten hinzu

X : morgen oder unmittelbar danach (zu unterscheiden von egal in der klassischen Logik auch X) (der Buchstabe X kommt aus dem Englischen ne x t : "next")
F : 1 Tag (der Buchstabe F kommt aus dem englischen f ndlich , „schließlich“)
G : immer (der Buchstabe G kommt aus dem Englischen g lobally : "global")
U : bis (der Buchstabe U aus dem Englischen kommt u ntil von derselben Bedeutung)
R : r elease (wörtlich "freigeben")

Eine klassische Satzlogikformel wie die Formel (a und b) oder c in der Menge der Sätze P = { a , b , c } ordnet jeder Teilmenge von P einen wahren oder falschen Wahrheitswert zu . Durch diese Beispielformel macht die Teilmenge { a } (wobei a wahr ist und b und c falsch sind) die Formel falsch, die Teilmenge { b , c } macht sie wahr.

Eine zeitliche Logikformel kombiniert einen Wahrheitswert nicht jeden Teil P , aber abhängig von der Art der Logik, wobei jede Sequenz von Teilmengen von P oder jede Welle auf den Abschnitte von P . Eine in der Aktion definierte Logik wird als linear bezeichnet , während eine in Bäumen definierte Formel als Verzweigungslogik oder logische Verzweigungen bezeichnet wird .

Nehmen wir den Fall der linearen Logik. Eine solche Logik kombiniert daher einen Wahrheitswert, wahr oder falsch, jede Suite, da jede ein Teil von P ist . Bezeichnen Sie mit M eine solche Formel, wir haben: $V = (V_ {1}, V_ {2}, \ ldots)$ $V_i$

Intuitiv, wenn die Sequenz V die zeitliche Entwicklung der verschiedenen Sätze von P darstellt , dann:

X ( f ) ist jetzt wahr, wenn f im nächsten Schritt wahr ist;
F ( f ) ist jetzt wahr, wenn f mindestens einen späteren Schritt einschließlich jetzt wahr ist;
G ( f ) ist jetzt wahr, wenn f bei allen nachfolgenden Schritten wahr ist, einschließlich jetzt;
f 1 U f 2 ist wahr, wenn einerseits f 2 später oder jetzt wahr ist und andererseits f 1 wahr ist (einschließlich), bis f 2 wahr ist;
f 1 R f 2 ist wahr, wenn f 2 wahr ist (einschließlich), bis f 1 wahr ist, oder wenn f 2 die ganze Zeit wahr ist.

Es kann angemerkt werden, dass die Modalitäten U und R eine der anderen sind: ${\ displaystyle \ left \ {{\ begin {align} \ varphi \ mathrm {U} \ psi \ equiv \ lnot (\ lnot \ varphi \ mathrm {R} \ lnot \ psi) \\\ varphi \ mathrm {R} \ psi \ equiv \ lnot (\ lnot \ varphi \ mathrm {U} \ lnot \ psi) \ end {align}} \ right.}$

Unterschiedliche Logik

Es gibt verschiedene zeitliche Logiken, darunter:

CTL * , eine baumbasierte Logik;
Computation Tree Logic ( CTL), eine in CTL * enthaltene Baumlogik;
Linear Time Logic (LTL), eine in CTL * enthaltene lineare Logik;
Metric Interval Temporal Logic (MITL), die die kontinuierliche Zeit berücksichtigt und einen Booleschen Wert zurückgibt;
Temporal Logic Signal (STL), das die kontinuierliche Zeit berücksichtigt und einen realen Wert zurückgibt
Zeitliche Logik, um in Zeitintervallen zu argumentieren. Wir können die Abschlussarbeit von B. Moszkowski, die von Halpern und Shoham entwickelte Logik sowie die Ergebnisse von Y. Venema zitieren.

Anmerkungen und Referenzen

(in) 0. Maler und D. Nickovic , "Überwachung der zeitlichen Eigenschaften kontinuierlicher Signale" , in Y. Lakhnech und S. Yovine, Formale Techniken, Modellierung und Analyse zeitgesteuerter und fehlertoleranter Systeme , vol. 3253, Springer Berlin Heidelberg,2004( ISBN 978-3-540-23167-7 , DOI 10.1007 / 978-3-540-30206-3_12 ).
Benjamin Charles Moszkowski , " Argumentation über digitale Schaltungen ", Stanford University (Dissertation) , Stanford University,1983( Online lesen , zugegriffen 1 st Juli 2019 )
Joseph Y. Halpern und Yoav Shoham , " A Propositional Modal Logic of Time Intervals ", J. ACM , vol. 38, n o 4,Oktober 1991, p. 935-962 ( ISSN 0004-5411 , DOI 10,1145 / 115.234,115351 , online lesen , zugegriffen 1 st Juli 2019 )
(in) Yde Venema , " Ausdruckskraft und Vollständigkeit der Jahresintervall-Zeitlogik. ” , Notre Dame Journal of Formal Logic , vol. 31, n o 4,September 1990, p. 529-547 ( ISSN 0029-4527 und 1939 bis 0726 , DOI 10,1305 / ndjfl / 1093635589 , online lesen , zugegriffen 1 st Juli 2019 )

Zum Thema passende Artikel