Weighted computability with discounting

Abstract

Στην παρούσα διατριβή εισάγουμε τις έννοιες της Γραμμικής Χρονικής Λογικής (Linear TimeLogic, εν συντομία LTL) με βάρη και discounting από τον ημιδακτύλιο max-plus, της πρώτηςτάξης λογικής (First-Order Logic, εν συντομία FO logic) με βάρη και discounting από τον maxplus,των ω-star-free σειρών και των counter-free Büchi αυτομάτων με βάρη και συμπεριφοράπου υπολογίζεται με χρήση των παραμέτρων discounting. Προσδιορίζουμε ίσεςκλάσεις/υποκλάσεις των LTL ορίσιμων σειρών, FO ορίσιμων σειρών, ω-star-free σειρών καισυμπεριφορών των counter-free Büchi αυτομάτων. Περαιτέρω, εισαγάγουμε το μοντέλο τωνgeneralized Büchi αυτομάτων με ε-μεταβάσεις και βάρη, αλλά και αυτό των Büchi αυτομάτωνμε ε-μεταβάσεις και βάρη. Ορίζουμε τη discounted συμπεριφορά των εν λόγω μοντέλων καιαποδεικνύουμε ότι είναι εκφραστικά ισοδύναμα με τα Büchi αυτόματα με βάρη και discountedσυμπεριφορά. Δείχνουμε επίσης ότι από κάθε τύπο ενός συντακτικού φράγματος της LTL μεβάρη μπορούμε να κατασκευάσουμε ένα generalized Büchi αυτόματο με βάρη που νααναγνωρίζει την ερμηνεία του τύπου. Ακόμη, κάθε σειρά αναγνωρίσιμη από ένα Büchiαυτόματο με βάρη και discounting είναι η εικόνα μιας ορίσιμης σειράς, από ένα τύπο τουπαραπάνω συντακτικού φράγματος, μέσω ενός αυστηρά αλφαβητικού επιμορφισμού. Τέλος,ορίζουμε την LTL με βάρη, την FO λογική με βάρη, ω-star-free σειρές και counter-free Büchiαυτόματα με βάρη από idempotent και χωρίς διαιρέτες του μηδενός ημιδακτύλιους, πουικανοποιούν συγκεκριμένα αξιώματα πληρότητας. Χρησιμοποιώντας τις ίδιες τεχνικές, με αυτέςπου χρησιμοποιούμε για τον ημιδακτύλιο max-plus με discounting, προσδιορίζουμε ίσεςκλάσεις/υποκλάσεις των LTL ορίσιμων σειρών, FO ορίσιμων σειρών, ω-star-free σειρών καισυμπεριφορών των counter-free Büchi αυτομάτων, δείχνοντας έτσι την ευρωστία της θεωρίαςμας. Η παραπάνω έρευνα κινητροδοτείται από το συνεχιζόμενα αυξανόμενο ενδιαφέρον γιαθεώρηση θεμελιωδών αρχών που διέπουν μαθηματικά αντικείμενα της ΘεωρητικήςΠληροφορικής, τα οποία μπορούν να χρησιμοποιηθούν στον ορισμό εργαλείων για ποσοτικήανάλυση των διαφόρων συστημάτων. Παρακάτω παρουσιάζουμε με περισσότερες λεπτομέρειεςτην υπάρχουσα βιβλιογραφία, το κίνητρο της συγκεκριμένης έρευνας και το περιεχόμενο τηςδιατριβής. Η χρονική λογική ορίστηκε από τον Prior το 1957 ως ένας λογικός φορμαλισμός ικανός νααναλύσει χρονικές ακολουθίες [60]. Η χρονική λογική του Prior είναι μία προτασιακή λογικήπου έχει επεκταθεί με δύο χρονικούς τελεστές F (κάποια στιγμή στο μέλλον) και P (κάποιαστιγμή στο παρελθόν). Το 1977, ο Pnueli στην [59], θεώρησε την LTL ως μία προτασιακή λογικήεμπλουτισμένη με δύο μελλοντικούς χρονικούς τελεστές «next» (επόμενο) και «until» (μέχρι),και την πρότεινε ως ένα εργαλείο κατάλληλο για να επιχειρηματολογήσουμε σε θέματα πουαφορούν την εκτέλεση προγραμμάτων. Αυτή η θεώρηση άνοιξε το δρόμο για την χρήση τηςLTL στο έλεγχο ορθότητας προγραμμάτων [βλ. 71], με πρακτικές εφαρμογές στη βιομηχανία[βλ. 4, 48, 71]. Ένας από τους τρόπους να πραγματοποιήσουμε έλεγχο μοντέλου είναι με τηχρήση αυτομάτων και έχει προταθεί από τους Vardi και Wolper [72, 73, 74]. Ο πυρήνας τηςπροσέγγισης αυτής βασίζεται στο γεγονός ότι κάθε τύπος της LTL μπορεί να αναπαρασταθεί απόένα μη-προσδιοριστό Büchi αυτόματο. Ένα γνωστό παράδειγμα υλοποίησης της παραπάνωπροσέγγισης είναι ο model checker SPIN που κατασκευάστηκε από τον Holzmann [40].Εκτός από τις πολύ σημαντικές εφαρμογές, τα αποτελέσματα που αφορούν στηνεκφραστική δύναμη της LTL θεωρούνται θεμελιώδη στον κλάδο της ΘεωρητικήςΠληροφορικής. Πιο συγκεκριμένα, είναι γνωστό ότι η κλάση των LTL ορίσιμων γλωσσώνταυτίζεται με την κλάση των FO ορίσιμων γλωσσών, καθώς επίσης με τις κλάσεις των star-free,των απεριοδικών, και των counter-free γλωσσών. Το αποτέλεσμα αυτό ισχύει για γλώσσεςπεπερασμένων και άπειρων λέξεων, και θεμελιώθηκε μέσω των σημαντικών ερευνητικώνσυνεισφορών των Kamp [41], Gabbay, Pnueli, Shelah, και Stavi [35], McNaughton και Papert[54], Ladner [49], Thomas [66, 67], Schützenberger [63], και Perrin [55].Είναι επόμενο πως η γενίκευση του προαναφερθέντος αποτελέσματος στο πλαίσιο τωνσειρών αποτελεί ένα σημαντικό βήμα για την κατανόηση των μαθηματικών ιδιοτήτων γλωσσώνπροδιαγραφών (specification languages) με ποσοτικά στοιχεία (π.χ. LTL με βάρη, FO λογική μεβάρη). Πρόσφατα, οι Droste και Vogler στην [24], απέδειξαν για σειρές πεπερασμένων, αλλάκαι άπειρων, λέξεων με τιμές από φραγμένα lattices, την εκφραστική ισοδυναμία της LTLορισιμότητας, FO ορισιμότητας, των star-free εκφράσεων και της απεριοδικότητας. Η δομή πουχρησιμοποιήθηκε στην συγκεκριμένη εργασία για την επιλογή των βαρών επιτρέπειεκλεπτυσμένες και σύντομες αποδείξεις, ωστόσο περιορίζει σε πεπερασμένου πλήθους τιμές τηνεικόνα των απεριοδικών σειρών. H μελέτη των εν λόγω εννοιών στα πλαίσια του ημιδακτύλιουmax-plus παρουσιάζει ιδιαίτερο ενδιαφέρον λόγω των σημαντικών πρακτικών εφαρμογών τουmax-plus στο δυναμικό προγραμματισμό και στα discrete event systems [1, 39]. Η χρήσηπαραμέτρων discounting εξασφαλίζει τη σύγκλιση άπειρων αθροισμάτων από τον max-plus,αλλά έχει και μία ουσιώδη εννοιολογική ερμηνεία. Συγκεκριμένα, όπως έχει εύστοχα διατυπωθείστην [6], η μέθοδος του discounting εκφράζει με απτό τρόπο το γεγονός ότι οι διαφόρων ειδώνανταμοιβές είναι προτιμότερο να λαμβάνονται άμεσα, παρά αργότερα στο μέλλον, καθώς και τογεγονός ότι τα μελλοντικά προβλήματα έχουν μικρότερη αξία από αυτά του παρόντος. Ηθεώρηση αυτή είναι ιδιαίτερα διαδεδομένη στα οικονομικά μαθηματικά [33]. Επίσης συναντάταιστη θεωρία παιγνίων [65], στις Μαρκοβιανές διαδικασίες λήψης αποφάσεων [31], στη θεωρίααυτομάτων [6, 9, 22, 23, 42, 51], στις θεωρίες εξισωσιμότητας [34], και στον έλεγχο μοντέλων[13, 14].