Quantitative modelling of parametric component-based systems
Creators: name: Πίττου, Μαρία Ε.
Publisher: name: Aristotle University of Thessaloniki
Year: 2023
Subjects: Μοντελοποίηση συστημάτων
Μοντελοποίηση αρχιτεκτονικών
Παραμετρικές αρχιτεκτονικές
Αλληλεπιδράσεις με διάταξη
Αλληλεπιδράσεις με αναδρομή
Αβεβαιότητα αρχιτεκτονικών
Συστήματα βασισμένα σε συνιστώσες
Παραμετρικά συστήματα βασισμένα σε συνιστώσες
Επεκταμένες λογικές αλληλεπιδράσεων
Επεκταμένες λογικές αλληλεπιδράσεων με βάρη
Ασαφείς επεκταμένες λογικές αλληλεπιδράσεων

description: Στη παρούσα διδακτορική διατριβή, μελετάμε το πρόβλημα της μοντελοποίησης για παραμετρικά συστήματα βασισμένα σε συνιστώσες. Αρχικά εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων και μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων για την περιγραφή των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Οι συγκεκριμένες λογικές επιτυγχάνουν να κωδικοποιήσουν τη διάταξη των αλληλεπιδράσεων καθώς και την αναδρομική εμφάνιση τους, όπως επιβάλλεται από την εκάστοτε αρχιτεκτονική. Έπειτα, μοντελοποιούμε τις συνιστώσες ενός συστήματος με τα συστήματα μεταβάσεων με ετικέτες. Έτσι, ένα σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια αρχιτεκτονική, και ένα παραμετρικό σύστημα που βασίζεται σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική αρχιτεκτονική. Έπειτα, μοντελοποιούμε διάφορες αρχιτεκτονικές και παραμετρικές αρχιτεκτονικές με την επεκταμένη προτασιακή και την πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων, αντίστοιχα. Για τις προτάσεις της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων αποδεικνύουμε την αποφασισιμότητα για το πρόβλημα της ισοδυναμίας και της εγκυρότητας τους σε διπλά εκθετικό χρόνο, ενώ η αποφασισιμότητα για το πρόβλημα της ικανοποιησιμότητας τους αποδεικνύεται σε εκθετικό χρόνο. Έπειτα, εισάγουμε μια επεκταμένη προτασιακή λογική αλληλεπιδράσεων με βάρη και μια πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων με βάρη, με τιμές από αντιμεταθετικούς ημιδακτύλιους, για την μοντελοποίηση των ποσοτικών χαρακτηριστικών των αρχιτεκτονικών και των παραμετρικών αρχιτεκτονικών, αντίστοιχα. Μία ποσοτική συνιστώσα, δηλαδή μία συνιστώσα με βάρη, περιγράφεται ως ένα ζεύγος από μία συνιστώσα και μία απεικόνιση βαρών. Συνεπώς, ένα ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών με βάρη και μια αρχιτεκτονική με βάρη, και ένα παραμετρικό ποσοτικό σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών με βάρη και μια παραμετρική αρχιτεκτονική με βάρη. Έπειτα, οι παραπάνω λογικές με βάρη εφαρμόζονται αντίστοιχα για τη μοντελοποίηση διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών στο ποσοτικό πλαίσιο, λαμβάνοντας υπόψη αν υπάρχει διάταξη και αναδρομή στις αλληλεπιδράσεις τους. Αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας των προτάσεων της πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων με βάρη είναι αποφασίσιμο σε διπλά εκθετικό χρόνο για το σύνολο (των υπο-ημιδακτυλίων) των skew fields. Έπειτα, εισάγουμε μια ασαφή επεκταμένη προτασιακή λογική αλληλεπιδράσεων και μια ασαφή πρώτης-τάξης επεκταμένη λογική αλληλεπιδράσεων για τη μοντελοποίηση της αβεβαιότητας στις αρχιτεκτονικές και στις παραμετρικές αρχιτεκτονικές, αντίστοιχα. Το πεδίο τιμών ασάφειας είναι μια De Morgan άλγεβρα. Έτσι, ένα ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα πεπερασμένο σύνολο συνιστωσών και μια ασαφή αρχιτεκτονική, και ένα παραμετρικό ασαφές σύστημα βασισμένο σε συνιστώσες ορίζεται ως ένα ζεύγος από ένα σύνολο παραμετρικών συνιστωσών και μια παραμετρική ασαφή αρχιτεκτονική. Οι παραπάνω ασαφείς λογικές εφαρμόζονται για τη περιγραφή της αβεβαιότητας διαφόρων αρχιτεκτονικών και παραμετρικών αρχιτεκτονικών, αντίστοιχα, λαμβάνοντας υπόψη την διάταξη και την αναδρομική εμφάνιση των ασαφών αλληλεπιδράσεων τους. Τέλος, αποδεικνύουμε ότι το πρόβλημα της ισοδυναμίας για μία μεγάλη κλάση των προτάσεων της ασαφούς πρώτης-τάξης επεκταμένης λογικής αλληλεπιδράσεων είναι αποφασίσιμο σε διπλά εκθετικό χρόνο. Για κάθε τέτοια πρόταση, αποδεικνύουμε επιπλέον πως αν η De Morgan άλγεβρα είναι ολικά διατεταγμένη τότε μπορούμε να υπολογίσουμε σε εκθετικό χρόνο το σύνολο των λέξεων των παραμετρικών ασαφών αλληλεπιδράσεων που διασφαλίζουν την αξιοπιστία της πρότασης σύμφωνα με ένα συγκεκριμένο όριο.
description: language for parametric architectures. These logics achieve to encode the order of the interactions and their recursive appearance, as it is imposed by each architecture. Then we model components with labelled transition systems, and in turn we define a component-based system as a pair of a finite set of components and an architecture, while a parametric component-based system is defined as a pair of a set of parametric components and a parametric architecture. Moreover, we show that the extended propositional interaction logic and its first-order level can sufficiently describe several well-known architectures applied in component-based systems and parametric component-based systems, respectively. Then, for the sentences of first-order extended interaction logic we prove the decidability of the equivalence and validity problem in doubly exponential time as well as the decidability of the satisfiability problem in exponential time. In the sequel, we introduce a weighted extended propositional interaction logic over commutative semirings and a weighted first-order extended interaction logic over commutative semirings for describing the non-functional aspects of architectures and parametric architectures, respectively. Then we describe a weighted component by a pair of a component and a weighted mapping. In turn, we define a weighted component-based system as a pair of a finite set of weighted components and a weighted architecture, and a parametric weighted component-based system as a pair of a set of parametric weighted components and a parametric weighted architecture. The two weighted logics serve for modelling several architectures and parametric architectures, respectively, in the weighted setup, by respecting the order and recursion in their interactions. Also, we prove that the equivalence problem for the sentences of weighted first-order extended interaction logic is decidable in doubly exponential time over the class (of subsemirings) of skew fields. In turn, we introduce a fuzzy extended propositional interaction logic and a fuzzy first-order extended interaction logic over De Morgan algebras in order to model uncertainty in architectures and parametric architectures, respectively. Then we define a fuzzy component-based system as a pair of a finite set of components and a fuzzy architecture, and a parametric fuzzy component-based system as a pair of a set of parametric components and a parametric fuzzy architecture. Moreover, we apply fuzzy extended propositional interaction logic and fuzzy first-order extended interaction logic for modelling the uncertainty in several architectures and parametric architectures, respectively, by respecting the order restrictions and the recursive appearance of their fuzzy interactions. Finally, we prove that the equivalence problem for a large class of sentences of fuzzy first-order extended interaction logic is decidable in doubly exponential time. For any such sentence over a totally ordered De Morgan algebra, we further prove that we can compute in exponential time the set of sequences of parametric fuzzy interactions which ensure the trustworthiness of the sentence according to a particular threshold.