Χρονική λογική

Στη λογική, ο όρος χρονική λογική (Αγγλικά: temporal logic) χρησιμοποιείται για να περιγράψει κάθε σύστημα κανόνων και συμβολισμού για την αναπαράσταση και συλλογιστική προτάσεων που χρησιμοποιούν το χρόνο. Κάποιες φορές χρησιμοποιείται σαν αναφορά στην tense logic, ένα σύστημα βασισμένο στην τροπική λογική που δημιουργήθηκε από τον Άρθουρ Πράιορ κατά τη δεκαετία του 1960. Η ανάπτυξη της χρονικής λογικής συνεχίστηκε από τους επιστήμονες της επιστήμης των υπολογιστών, ειδικά από τον Αμιρ Πνουέλι και τους επιστήμονες της λογικής.

Αν και η λογική του Αριστοτέλη ασχολείται σχεδόν εξ ολοκλήρου με τον κατηγορηματικό συλλογισμό, υπάρχουν σημεία στο έργο του που μπορούν σήμερα να φανούν σαν πρώιμα σημεία της χρονικής λογικής και μπορεί να σημαίνουν ότι υπήρξε μια πρώιμη, ημιτελής μορφή της δυαδικής τροπικής χρονικής λογικής πρώτης τάξης. Το πρώτο τυπικό σύστημα χρονικής τροπικής λογικής δημιουργήθηκε από τον Αβικέννα, η λογική του οποίου^[1] αναπτύχθηκε στη συνέχεια από τον Najm al-Dīn al-Qazwīnī al-Kātibī και έγινε το κυρίαρχο σύστημα της Ισλαμικής λογικής μέχρι πρόσφατα.^[2]^[3] Η λογική του Αβικέννα επηρέασε επίσης αρκετούς από τους πρώτους Ευρωπαίους επιστήμονες της λογικής, όπως ο Albertus Magnus^[4] και ο Ουλιέλμος του Όκαμ.^[5]^[6] Ανάμεσα στις θεωρίες της κλασικής λογικής, η λογική που χρησιμοποιεί τον υπαρξιακό ποσοδείκτη ή τον καθολικό ποσοδείκτη, ονομάζεται κατηγορηματική λογική. Κάθε λογική που θεωρεί το χρόνο σαν μια ακολουθία από καταστάσεις είναι χρονική λογική, και κάθε λογική που χρησιμοποιεί μόνο δύο τιμές αληθείας είναι δυαδική λογική.

Έστω η πρόταση: "Πεινάω". Αν και η σημασία της είναι σταθερή στο χρόνο, η τιμή αληθείας της μπορεί να διαφέρει στο χρόνο. Κάποιες φορές η πρόταση είναι αληθής, κάποιες φορές είναι ψευδής, αλλά η πρόταση δεν είναι ποτέ αληθής και ψευδής ταυτόχρονα. Σε μια χρονική λογική, οι προτάσεις μπορούν να έχουν μια τιμή αληθείας που να διαφέρει ανάλογα με τη χρονική στιγμή. Αντίθετα, οι άχρονες λογικές μπορούν να χειριστούν μόνο προτάσεις, η τιμή αληθείας των οποίων είναι σταθερή στο χρόνο. Αυτός ο χειρισμός των τιμών αληθείας στο χρόνο διαφοροποιεί τη χρονική λογική από την υπολογιστική λογική ρημάτων (computational verb logic).

Σε μια χρονική λογική μπορούν επομένως να εκφραστούν προτάσεις όπως: "Πεινάω πάντα", "Τελικά θα πεινάσω", ή "Θα πεινάω μέχρι να φάω κάτι".

Η χρονική λογική έχει βρει σημαντικές εφαρμογές στην τυπική επαλήθευση, όπου χρησιμοποιείται για να ορίζονται απαιτήσεις συστημάτων υλικού ή λογισμικού. Για παράδειγμα, μπορεί κανείς να θέλει να εκφράσει ότι οποτεδήποτε γίνεται μια αίτηση, τελικά θα δοθεί πρόσβαση σε έναν πόρο, αλλά ποτέ δε θα δοθεί πρόσβαση σε δύο αιτούντες ταυτόχρονα. Μια τέτοια πρόταση εκφράζεται σε μια χρονική λογική με βολικό τρόπο.

Η χρονική λογική έχει πάντα τη δυνατότητα να εκφράζει συλλογισμούς για μια χρονική γραμμή. Οι αποκαλούμενες λογικές γραμμικού χρόνου μπορούν να περιγράφουν μόνο αυτούς τους συλλογισμούς. Οι διακλαδιζόμενες λογικές, από την άλλη πλευρά, μπορούν να χειριστούν πολλαπλές χρονικές γραμμές, κάτι που προϋποθέτει ένα περιβάλλον που να μπορεί να συμπεριφέρεται απρόσμενα. Για να συνεχιστεί το παραπάνω παράδειγμα, σε μια διακλαδιζόμενη λογική μπορεί να εκφραστεί η πρόταση "υπάρχει η πιθανότητα ότι θα πεινάω για πάντα". Μπορεί επίσης να εκφραστεί η πρόταση "υπάρχει η πιθανότητα τελικά να μην πεινάω πια". Αν δεν είναι γνωστό αν το υποκείμενο θα φάει ή όχι τελικά, και οι δύο προτάσεις είναι αληθείς.

Δύο από τις πρώτες λογικές του είδους για τυπική επαλήθευση ήταν η Γραμμική Χρονική Λογική (μια γραμμική λογική του χρόνου από τους Αμίρ Πνουέλι και Ζοχάρ Μάνα) και η λογική υπολογιστικού δένδρου, μια διακλαδιζόμενη λογική από τους Έντμουντ Κλαρκ και Άλεν Έμερσον. Αν και η δεύτερη από αυτές είναι πιο αποδοτική από την πρώτη, αυτό δεν ισχύει γενικά για τις διακλαδιζόμενες και τις γραμμικές λογικές γενικά. Οι Έμερσον και Λάι έδειξαν ότι κάθε γραμμική λογική μπορεί να επεκταθεί σε μια γραμμική λογική που μπορεί να αποκριθεί με την ίδια πολυπλοκότητα.

Χρονικοί τελεστές

Η χρονική λογική έχει δύο είδη τελεστών: τους λογικούς τελεστές και τους τροπικούς τελεστές [1]. Οι λογικοί τελεστές είναι οι συνηθισμένοι αληθο-συναρτησιακοί τελεστές ( $\neg ,\lor ,\land ,\rightarrow$ ). Οι τροπικοί τελεστές που χρησιμοποιούνται στη Γραμμική Χρονική Λογική και στη Λογική Υπολογιστικού Δένδρου ορίζονται ως εξής.

Κείμενο	Σύμβολο	Ορισμός	Επεξήγηση	Διάγραμμα
Δυαδικοί τελεστές
$\phi$ U $\psi$	$\phi ~{\mathcal {U}}~\psi$	${\begin{matrix}(B\,{\mathcal {U}}\,C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}$	Until, "Μέχρι": η $\psi$ ισχύει τώρα ή στο μέλλον και η $\phi$ πρέπει να ισχύει μέχρι εκείνη τη στιγμή. Σε αυτήν τη στιμή η $\phi$ δε χρειάζεται να ισχύει πια.
$\phi$ R $\psi$	$\phi ~{\mathcal {R}}~\psi$	${\begin{matrix}(B\,{\mathcal {R}}\,C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}$	Release, "Απελευθέρωση": η $\phi$ απελευθερώνει την $\psi$ αν η $\psi$ είναι αληθής μέχρι την πρώτη στιγμή που η $\phi$ είναι αληθής (ή για πάντα αν δεν υπάρχει τέτοια στιγμή).
Μοναδιαίοι τελεστές
N $\phi$	$\circ \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Next, "Επόμενο": η $\phi$ πρέπει να ισχύει στην επόμενη κατάσταση. (Χρησιμοποιείται με την ίδια σημασία και ο X.)
F $\phi$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	Future, "Μέλλον": η $\phi$ πρέπει τελικά να ισχύσει (κάπου στο υπόλοιπο τμήμα του μονοπατιού).
G $\phi$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally, "Καθολικά": η $\phi$ πρέπει να ισχύει σε όλο το υπόλοιπο μονοπάτι.
A $\phi$		${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$	All, "Όλα": η $\phi$ πρέπει να ισχύει σε όλα τα μονοπάτια που αρχίζουν από την τρέχουσα κατάσταση.
E $\phi$		${\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}$	Exists, "Υπάρχει": υπάρχει τουλάχιστον ένα μονοπάτι που αρχίζει από την τρέχουσα κατάσταση, στο οποίο να ισχύει η $\phi$ .

Εναλλακτικοί συμβολισμοί:

ο τελεστής R κάποιες φορές συμβολίζεται με V
ο τελεστής W είναι ο τελεστής αδύναμο μέχρι (weak until): η $fWg$ είναι ισοδύναμη με την $fUg\lor Gf$

Οι μοναδιαίοι τελεστές είναι καλά ορισμένες προτάσεις όταν η B( $\phi$ ) είναι καλά ορισμένη. Οι δυαδικοί τελεστές είναι καλά ορισμένες προτάσεις όταν η B( $\phi$ ) και η C( $\phi$ ) είναι καλά ορισμένες.

Σε κάποιες λογικές, κάποιοι τελεστές δε μπορούν να εκφραστούν. Για παράδειγμα, ο τελεστής N δε μπορεί να εκφραστεί στη Χρονική Λογική των Ενεργειών.

Χρονικές λογικές

Κάποιες χρονικές λογικές είναι:

η χρονική λογική διαστημάτων (Interval temporal logic, ITL)
ο μ λογισμός, που περιλαμβάνει ένα υποσύνολο
- η λογική Hennessy-Milner (HML)
- η CTL*, που περιλαμβάνει σαν υποσύνολο
  - τη λογική υπολογιστικού δένδρου (Computational tree logic, CTL)
  - τη γραμμική χρονική λογική (Linear temporal logic, LTL)

Δείτε επίσης

Παραπομπές

↑ History of logic: Arabic logic, Encyclopædia Britannica.
↑ TONY STREET (2000), «TOWARD A HISTORY OF SYLLOGISTIC AFTER AVICENNA: NOTES ON RESCHER'S STUDIES ON ARABIC MODAL LOGIC», Journal of Islamic Studies (Oxford University Press) 11 (2): 209–228
↑ Tony Street (1 Ιανουαρίου 2005). «Logic». Στο: Peter Adamson· Richard C. Taylor. The Cambridge Companion to Arabic Philosophy. Cambridge University Press. σελίδες 247& 250. ISBN 9780521520690.
↑ Richard F. Washell (1973), "Logic, Language, and Albert the Great", Journal of the History of Ideas 34 (3), p. 445-450 [445].
↑ Kneale p. 229
↑ Kneale: σελ. 266; Όκαμ: Summa Logicae i. 14; Αβικέννας: Avicennae Opera Βενετία 1508 f87rb

Αναφορές

Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
E. A. Emerson and C. Lei, modalities for model checking: branching time logic strikes back, in Science of Computer Programming 8, p 275-306, 1987.
E.A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990

Εξωτερικοί σύνδεσμοι

ΕΠΛ 12: Λογική στην Πληροφορική, περιέχει υλικό για τη χρονική λογική.
Τυπικές Μέθοδοι Ανάλυσης Συστημάτων, Π. Κατσαρός, Αριστοτέλειο Πανεπιστήμιο Θεσσαλονίκης
Stanford Encyclopedia of Philosophy: "Temporal Logic" -- του Anthony Galton. (Αγγλικά)

[Britannica-1] History of logic: Arabic logic, Encyclopædia Britannica.

[2] TONY STREET (2000), «TOWARD A HISTORY OF SYLLOGISTIC AFTER AVICENNA: NOTES ON RESCHER'S STUDIES ON ARABIC MODAL LOGIC», Journal of Islamic Studies (Oxford University Press) 11 (2): 209–228

[3] Tony Street (1 Ιανουαρίου 2005). «Logic». Στο: Peter Adamson· Richard C. Taylor. The Cambridge Companion to Arabic Philosophy. Cambridge University Press. σελίδες 247& 250. ISBN 9780521520690.

[4] Richard F. Washell (1973), "Logic, Language, and Albert the Great", Journal of the History of Ideas 34 (3), p. 445-450 [445].

[5] Kneale p. 229

[6] Kneale: σελ. 266; Όκαμ: Summa Logicae i. 14; Αβικέννας: Avicennae Opera Βενετία 1508 f87rb

[1]

[2]

[3]

[4]

[5]

[6]