Quantitative modelling of parametric component-based systems
Authors: Πίττου Μαρία 
Published: February 2024

Η μοντελοποίηση πολύπλοκων συστημάτων συνήθως επιτυγχάνεται με μεθόδους βασισμένες σε συνιστώσες στις οποίες η κατασκευή ενός συστήματος προκύπτει από τον σχεδιασμό και την σύνθεση πολλαπλών συνιστωσών του ίδιου ή διαφορετικού τύπου, οι οποίες αλληλεπιδρούν μεταξύ τους. Ωστόσο, πολλά από αυτά τα συστήματα είναι παραμετρικά δηλαδή λειτουργούν ανεξάρτητα από το πλήθος των αντιγράφων των συνιστωσών κάθε τύπου που τα απαρτίζουν. Τα παραμετρικά συστήματα αποτελούν μια ευρεία κατηγορία συστημάτων βασισμένα σε συνιστώσες και προκύπτουν από ένα πεπερασμένο αριθμό τύπων συνιστωσών όπου κάθε τύπος συνιστώσας έχει άγνωστο πλήθος αντιγράφων. Η μοντελοποίηση τέτοιων συστημάτων απαιτεί τη φορμαλιστική περιγραφή των κανόνων που αφορούν τις συνδέσεις μεταξύ των συνιστωσών τους. Τέτοιοι κανόνες επικοινωνίας μπορούν να περιγραφούν μέσω της έννοιας της αρχιτεκτονικής η οποία χαρακτηρίζει τη τοπολογία και τις επιτρεπτές αλληλεπιδράσεις μεταξύ των συνιστωσών ενός συστήματος. Ο ορθός χαρακτηρισμός των αρχιτεκτονικών εξασφαλίζει ότι το σύστημα ικανοποιεί τις περισσότερες προδιαγραφές λειτουργίας του, από κατασκευή. Για να επιτευχθεί μια καλά θεμελιωμένη μοντελοποίηση των αρχιτεκτονικών θα πρέπει να περιγραφούν τα ποιοτικά χαρακτηριστικά τους, αλλά και τα ποσοτικά τους χαρακτηριστικά όταν απαιτούνται. Από την άλλη, ο χαρακτηρισμός των αρχιτεκτονικών γίνεται στα αρχικά στάδια της κατασκευής των συστημάτων και ως εκ τούτου είναι σημαντική η περιγραφή της αβεβαιότητας και της έλλειψης πληροφοριών που οφείλονται στις αλληλεπιδράσεις των συνιστωσών. Στη παρούσα διδακτορική διατριβή, μελετάμε το πρόβλημα της μοντελοποίησης για παραμετρικά συστήματα βασισμένα σε συνιστώσες. Για αυτό, μοντελοποιούμε τις αρχιτεκτονικές τέτοιων συστημάτων στο ποιοτικό, το ποσοτικό και το ασαφές πλαίσιο, με τη χρήση λογικών, ώστε να περιγράψουμε τις αλληλεπιδράσεις των συνιστωσών, τα βάρη αυτών και την αβεβαιότητα αυτών, αντίστοιχα. Έπειτα, και στα τρία πλαίσια μοντελοποιούμε ένα σύστημα ως ένα ζεύγος από ένα σύνολο συνιστωσών και μια αρχιτεκτονική. Το ποιοτικό και ασαφές πλαίσιο υπάγονται στο γενικότερο ποσοτικό πλαίσιο μοντελοποίησης. Αρχικά εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων και στη συνέχεια μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων για την φορμαλιστική περιγραφή των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Οι συγκεκριμένες λογικές επιτυγχάνουν να κωδικοποιήσουν την σειρά εμφάνισης των επιτρεπτών αλληλεπιδράσεων καθώς και την αναδρομική εμφάνιση τους, όπως επιβάλλεται από την εκάστοτε αρχιτεκτονική. Έπειτα, μοντελοποιούμε τις συνιστώσες ενός συστήματος με τα λεγόμενα συστήματα μεταβάσεων με ετικέτες. Έτσι, ένα σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια αρχιτεκτονική, και ένα παραμετρικό σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική αρχιτεκτονική. Στη συνέχεια, παρουσιάζουμε διάφορες αρχιτεκτονικές και παραμετρικές αρχιτεκτονικές οι οποίες μοντελοποιούνται επιτυχώς με την επεκταμένη προτασιακή και την πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων, αντίστοιχα. Επιπλέον, για τις προτάσεις της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων αποδεικνύουμε την αποφασισιμότητα για το πρόβλημα της ισοδυναμίας και της εγκυρότητας τους σε διπλά εκθετικό χρόνο, ενώ η αποφασισιμότητα για το πρόβλημα της ικανοποιησιμότητας τους αποδεικνύεται σε εκθετικό χρόνο. Στη συνέχεια, επαληθεύουμε την ευρωστία της συγκεκριμένης μεθόδου μοντελοποίησης καθώς την επεκτείνουμε στο ποσοτικό πλαίσιο. Συγκεκριμένα, εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων με βάρη και μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων με βάρη, με τιμές από αντιμεταθετικούς ημιδακτύλιους, για την μοντελοποίηση των ποσοτικών χαρακτηριστικών των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Έπειτα, μια ποσοτική συνιστώσα, δηλαδή μία συνιστώσα με βάρη περιγράφεται ως ένα ζεύγος από μία συνιστώσα και μία απεικόνιση βαρών. Συνεπώς, ένα ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών με βάρη και μια αρχιτεκτονική με βάρη, και ένα παραμετρικό ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών με βάρη και μια παραμετρική αρχιτεκτονική με βάρη. Στη συνέχεια, οι δύο παραπάνω λογικές με βάρη εφαρμόζονται για τη μοντελοποίηση διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών, αντίστοιχα, στο ποσοτικό πλαίσιο, λαμβάνοντας υπόψη αν υπάρχει διάταξη και αναδρομή στις αλληλεπιδράσεις τους. Επιπροσθέτως, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των προτάσεων της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων με βάρη είναι αποφασίσιμο σε διπλά εκθετικό χρόνο για ένα ευρύ σύνολο ημιδακτυλίων, και συγκεκριμένα για το σύνολο (των υπο-ημιδακτυλίων) των skew fields. Έπειτα, εισάγουμε μια ασαφή επεκταμένη προτασιακή λογική αλληλεπιδράσεων και μια ασαφή πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων με σκοπό τη μοντελοποίηση της αβεβαιότητας στις αρχιτεκτονικές και στις παραμετρικές αρχιτεκτονικές, αντίστοιχα. Το πεδίο τιμών ασάφειας είναι μια De Morgan άλγεβρα. Στη συνέχεια, ένα ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια ασαφή αρχιτεκτονική, και ένα παραμετρικό ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική ασαφή αρχιτεκτονική. Έπειτα, οι δύο παραπάνω ασαφείς λογικές εφαρμόζονται επιτυχώς για τη περιγραφή, στο ασαφές πλαίσιο, διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών, αντίστοιχα, λαμβάνοντας υπόψη την διάταξη και την αναδρομική εμφάνιση των ασαφών αλληλεπιδράσεων τους, όπως επιβάλλεται από την εκάστοτε αρχιτεκτονική. Τέλος, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας για μία μεγάλη κλάση των προτάσεων της ασαφούς πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων είναι αποφασίσιμο σε διπλά εκθετικό χρόνο. Για κάθε τέτοια πρόταση, αποδεικνύουμε επιπλέον πως αν η De Morgan άλγεβρα είναι ολικά διατεταγμένη τότε μπορούμε να υπολογίσουμε σε εκθετικό χρόνο το σύνολο των λέξεων των παραμετρικών ασαφών αλληλεπιδράσεων που διασφαλίζουν την αξιοπιστία της πρότασης σύμφωνα με ένα συγκεκριμένο όριο.