Automata on infinite words and games:

Abstract

Η θεωρία των αυτομάτων που αναγνωρίσουν άπειρες λέξεις (ω-words) και των παιγνίων άπειρης διάρκειας έχει τα τελευταία χρόνια παράξει πλούσιο ερευνητικό υλικό το οποίο βρίσκει εφαρμογή σε ποικίλους επιστημονικούς κλάδους. Η πιο σημαντική εφαρμογή του ερευνητικού αυτού έργου έχει επιτευχθεί στον έλεγχο και στην επαλήθευση μοντέλων που έχουν να κάνουν με την αυτοματοποιημένη σύνθεση συστημάτων υλικού (hardware) και λογισμικού (software). Στη παρούσα διατριβή παρουσιάζουμε μέρος αυτού του ερευνητικού υλικού ξεκινώντας από μια επισκόπηση της βασική θεωρίας γύρω από τη θεωρία των αυτομάτων και των παιγνίων (Κεφάλαια 1 & 2). Στη συνέχεια (Κεφάλαια 3 & 4) παρουσιάζονται αλγόριθμοι και θεωρητικά αποτελέσματα που εφαρμόζονται στη θεωρία παιγνίων και τα οποία αναμένεται να παίξουν σημαντικό ρόλο στη παραγωγή υλικού και λογισμικού τα επόμενα χρόνια. Στη παρούσα διατριβή, η οποία με εξαίρεση μια υλοποίηση ενός αλγορίθμου είναι επί της ουσίας μια επισκόπηση του πρόσφατου ερευνητικού έργου, παρουσιάζουμε αυτόματα τα οποία αναγνωρίζουν λέξεις απείρου μήκους (ω-αυτόματα) και ορίζουμε τις ακόλουθες συνθήκες αποδοχής (acceptance conditions) άπειρων λέξεων: Βüchi, Muller, Rabin και parity καθώς επίσης ορίζουμε και τα μη ντετερμινιστικά αυτόματα για τις παραπάνω συνθήκες αποδοχής. Έπειτα, παρουσιάζουμε τους τρόπους μετασχηματισμού από έναν τύπο αυτομάτων σε άλλον και καταλήγουμε στο ότι όλα τα μη ντετερμινιστικά αυτόματα είναι ισοδύναμα, αναγνωρίζουν δηλαδή την ίδια κλάση ω-γλωσσών. Έπειτα μελετάμε τα αντίστοιχα ντετερμινιστικά μοντέλα για τους παραπάνω τύπους αυτομάτων. Αποδεικνύεται επίσης ότι τα ντετερμινιστικά Βüchi αυτόματα δεν είναι ισοδύναμα με τα υπόλοιπα καθώς είναι αδύνατο να αναγνωρίσουν ακόμα και απλές ω-γλώσσες, γλώσσες δηλαδή που περιέχουν άπειρες λέξεις. Μετατρέπουμε ντετερμινιστικά Muller σε Rabin και parity αυτόματα και δείχνουμε ότι τα ντετερμινιστικά Muller, Rabin και parity αυτόματα αναγνωρίζουν την ίδια κλάση ω-γλωσσών η οποία μάλιστα είναι κλειστή ως προς το συμπλήρωμα. Στη συνέχεια παρουσιάζουμε τη θεωρία γύρω από τα παίγνια άπειρης διάρκειας και εξηγούμε έννοιες όπως αυτή της στρατηγικής (strategy) και της συνθήκης νίκης (winning condition). Έννοιες όπως αυτές των στρατηγικών χωρίς χρήση μνήμης (memoryless strategies) και του καθορισμού αποτελέσματος (determinacy) εισάγονται επίσης και μας βοηθούν στο να επιλύουμε παίγνια με απλές συνθήκες νίκης. Τέλος, παρουσιάζουμε κάποια πρόσφατα θεωρητικά και αλγοριθμικά αποτελέσματα (παράλληλα με μια υλοποίηση ενός αλγορίθμου) που έχουν να κάνουν με parity και mean-payoff parity παίγνια. Πιο συγκεκριμένα, περιγράφουμε τον τρόπο καθορισμού αποτελέσματος με χρήση στρατηγικής χωρίς χρήση μνήμης σε parity παίγνια καθώς επίσης και κάποιους αλγόριθμους όπως αυτόν για το πρόβλημα του υπολογισμού τιμών (value problem), μεταξύ άλλων, για mean-payoff parity παίγνια.