Γραμμική χρονική λογική: Διαφορά μεταξύ των αναθεωρήσεων

Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
μ Ρομπότ: Μεταφέρω 4 σύνδεσμους interwiki, που τώρα παρέχονται από τα Wikidata στο d:Q1536492
μ Αντικατάσταση παρωχημένης σύνταξης latex (mw:Extension:Math/Roadmap)
Γραμμή 5:
 
== Σύνταξη ==
Η LTL αποτελείται από ένα σύνολο από προτασιακές μεταβλητές <math>p_1, p_2, \dots</math>, τους γνωστούς λογικούς συνδέσμους <math>\neg,\orlor,\andland,\rightarrow</math> και τους ακόλουθους χρονικούς τροπικούς τελεστές:
 
*'''X''' για το "επόμενο" (ή '''N''')
Γραμμή 65:
== Ισοδυναμίες ==
 
<math>X ( \phi \orlor \psi ) \equiv X \phi \orlor X \psi</math>
 
<math>X ( \phi \andland \psi ) \equiv X \phi \andland X \psi</math>
 
<math>X \neg \phi \equiv \neg X \phi</math>
Γραμμή 73:
<math>X ( \phi U \psi ) \equiv ( X \phi ) U ( X \psi )</math>
 
<math>F ( \phi \orlor \psi ) \equiv F \phi \orlor F \psi</math>
 
<math>\neg F \phi \equiv G \neg \phi</math>
 
<math>G ( \phi \andland \psi ) \equiv G \phi \andland G \psi</math>
 
<math>\neg G \phi \equiv F \neg \phi</math>
 
<math>( \phi \andland \psi ) U \rho \equiv ( \phi U \rho ) \andland ( \psi U \rho )</math>
 
<math>\rho U ( \phi \orlor \psi ) \equiv ( \rho U \phi ) \orlor ( \rho U \psi )</math>
 
<math>F \phi \equiv F F \phi</math>
Γραμμή 91:
<math>\phi U \psi \equiv \phi U ( \phi U \psi )</math>
 
<math>F \phi \equiv \phi \orlor X F \phi</math>
 
<math>G \phi \equiv \phi \andland X G \phi</math>
 
<math>\phi U \psi \equiv \psi \orlor ( \phi \andland X ( \phi U \psi ) )</math>
 
<math>\phi W \psi \equiv \psi \orlor ( \phi \andland X ( \phi W \psi ) )</math>
 
<math>\phi R \psi \equiv ( \phi \andland \psi ) \orlor ( \psi \andland X ( \phi R \psi ) )</math>
 
== Ειδικοί σύνδεσμοι==