Automata on infinite words and games:
Creators: name: Ορλης, Χρήστος Ευστρατίου
Publisher: name: Aristotle University of Thessaloniki
Year: 2013
Subjects: ω-Αυτόματα
Άπειρης διάρκειας παίγνια
Καθορισμός αποτελεσμάτων σε parity παίγνια
Αλγόριθμοι για min-payoff parity παίγνια
Έλεγχος και επαλήθευση μοντέλων
Infinite duration games
Determinacy of parity games
Algorithms for mean-payoff parity games
Verification

description: Η θεωρία των αυτομάτων που αναγνωρίσουν άπειρες λέξεις (ω-words) και των παιγνίων άπειρης διάρκειας έχει τα τελευταία χρόνια παράξει πλούσιο ερευνητικό υλικό το οποίο βρίσκει εφαρμογή σε ποικίλους επιστημονικούς κλάδους. Η πιο σημαντική εφαρμογή του ερευνητικού αυτού έργου έχει επιτευχθεί στον έλεγχο και στην επαλήθευση μοντέλων που έχουν να κάνουν με την αυτοματοποιημένη σύνθεση συστημάτων υλικού (hardware) και λογισμικού (software). Στη παρούσα διατριβή παρουσιάζουμε μέρος αυτού του ερευνητικού υλικού ξεκινώντας από μια επισκόπηση της βασική θεωρίας γύρω από τη θεωρία των αυτομάτων και των παιγνίων (Κεφάλαια 1 &amp; 2). Στη συνέχεια (Κεφάλαια 3 &amp; 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 παίγνια.
description: The theory of automata, logics, and infinite games has meanwhile produced a large number of deep and mathematically appealing results. More important, this theory is intimately connected with the development of algorithms for the automatic verification and synthesis of hardware and software systems. In this thesis we present part of the research that has been done in this scientific area the last years. We introduce automata on in finite words (ω-automata) and define the following acceptance conditions: Βüchi acceptance, Muller acceptance, Rabin Acceptance, the parity condition and the respective nondeterministic automata. Then we show how to transform these automata from one form to another and we conclude that all nondeterministic automata are equivalent in expressive power. Next, we study deterministic models of such automata. Deterministic Βüchi automata are too weak for recognizing even very simple -languages. We transform deterministic Muller into deterministic Rabin and parity automata and show that deterministic Muller, Rabin and parity automata recognize the same class of ω-languages which is closed under complementation. Then, we introduce the underlying theory around infinite games and we explain what a strategy and a winning condition is. The notions of forgetful, memoryless strategies and determinacy are also introduced and help us solve games with simple winning conditions. Finally, we present some recent theoretical and algorithmic results (along with efficient implementations) regarding parity games and mean-payoff parity games. More specifically, we discuss about the memoryless determinacy of parity games and about some problems that arise with mean-payoff parity games such as the one of computing the values of a game or the problem of deciding whether, given a state of the game arena, the value of this state exceeds a predefined number.