Weighted computability with discounting:
Creators: name: Μανδραλή, Ελένη Γ.
Publisher: name: Aristotle University of Thessaloniki
Year: 2013
Subjects: Γραμμική Χρονική Λογική με βάρη
Λογική Πρώτης Τάξης με βάρη
star-free σειρές
counter-free αυτόματα με βάρη
Weighted linear temporal logic
Weighted first-order logic
Weighted counter-free automata
star-free series

description: Στην παρούσα διατριβή εισάγουμε τις έννοιες της Γραμμικής Χρονικής Λογικής (Linear Temporal Logic, εν συντομία LTL) με βάρη και discounting από τον ημιδακτύλιο max-plus, της πρώτης τάξης λογικής (First-Order Logic, εν συντομία FO logic) με βάρη και discounting από τον max-plus, των ω-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 αυτομάτων, δείχνοντας έτσι την ευρωστία της θεωρίας μας. Η παραπάνω έρευνα κινητροδοτείται από το συνεχιζόμενα αυξανόμενο ενδιαφέρον για θεώρηση θεμελιωδών αρχών που διέπουν μαθηματικά αντικείμενα της Θεωρητικής Πληροφορικής, τα οποία μπορούν να χρησιμοποιηθούν στον ορισμό εργαλείων για ποσοτική ανάλυση των διαφόρων συστημάτων.
description: In this thesis we deal with the notions of weighted Linear Temporal Logic (LTL for short), weighted First-Order Logic (FO for short), ω-star-free series and weighted counter-free Büchi automata over the max-plus semiring with discounting, and establish the expressive equivalence of (fragments of) LTL-definability, FO-definability, star-freeness and counter-freeness for series over infinite words. We additionally define weighted generalized Büchi automata with discounting and ε-transitions, and prove these models to be equivalent to weighted Büchi automata with discounting, which were already introduced in the literature. We present an effective translation, of a syntactic fragment of the weighted LTL to weighted generalized Büchi automata with ε-transitions. Furthermore, we introduce a weighted LTL, a weighted FO, ω-star-free series and weighted counter-free Büchi automata over additively idempotent and zero-divisor free complete semirings. Using the same arguments, as for the max-plus semiring we establish the equivalence of (fragments of) LTL-definability, FO-definability, star-freeness and counter-freeness, showing in this way the robustness of our theory. Our motivation lies in the last years' increasing interest in lifting fundamental results from classical to quantitative models. This is driven by the need to develop model checking tools incorporating quantitative features. This need, but also the deep theoretical interest, led several researchers to consider and investigate quantitative versions of logics.