Reversible Computation in Petri Nets
Ημερομηνία
2020-12Advisor
Philippou, AnnaΕκδότης
Πανεπιστήμιο Κύπρου, Σχολή Θετικών και Εφαρμοσμένων Επιστημών / University of Cyprus, Faculty of Pure and Applied SciencesPlace of publication
ΚύπροςCyprus
Google Scholar check
Keyword(s):
Metadata
Εμφάνιση πλήρους εγγραφήςΕπιτομή
Ο αναστρέψιμος υπολογισμός είναι μια μη συμβατική μορφή υπολογισμού που επεκτείνει τον τυπικό τρόπο υπολογισμού με τη δυνατότητα αντίστροφης εκτέλεσηs λειτουργιών. Η αναστρεψιμότητα προσέλκυσε πρόσφατα αυξανόμενη προσοχή σε διάφορες ερευνητικές κοινότητες καθώς από τη μία υπόσχεται υπολογισμούς χαμηλής ισχύος και, από την άλλη, είναι εφαρμόσιμη σε μια ποικιλία εφαρμογών.
Η διερεύνηση της αναστρεψιμότητας μέσω τυπικών μοντέλων καθορίζει τα θεωρητικά θεμέλια για το τι είναι η αναστρεψιμότητα, ποιο σκοπό εξυπηρετεί, και πως ωφελεί τα φυσικά και τεχνητά συστήματα. Ως εκ τούτου, προτείνουμε μια αναστρέψιμη προσέγγιση για τα δίκτυα Πέτρι, εισάγοντας μηχανισμούς και σχετική λειτουργική σημασιολογία για την αντιμετώπιση των προκλήσεων που έχουν οι κύριες μορφές αναστρεψιμότητας.
Τα δίκτυα Πέτρι είναι μια μαθηματική γλώσσα για μοντελοποίηση και συλλογισμό κατανεμημένων συστημάτων. Η πρόταση μας αφορά μία παραλλαγή των δικτύων Πέτρι, που ονομάζεται Αναστρέψιμα Δίκτυα Πέτρι, όπου τα διακριτικά ενός δικτύου ξεχωρίζουν μεταξύ τους με μοναδικές ταυτότητες. Δείχνουμε τη δυνατότητα εφαρμογής της προσέγγισής μας σε ένα μοντέλο μεταβολικής διαδρομής και ένα σύστημα επεξεργασίας συναλλαγών όπου και τα δύο εκδηλώνουν αναστρέψιμη συμπεριφορά.
Μια άμεση επέκταση του αρχικού μοντέλου συμπεριλαμβάνει την παροχή πολλαπλών διακριτικών που εκπροσωπούν τον ίδιο τύπο. Μία τέτοια επέκταση σε ένα μοντέλο όπως τα δίκτυα Πέτρι, έχει ως αποτέλεσμα αντίστροφες συγκρούσεις όπου ένα διακριτικό μπορεί να έχει τοποθετηθεί σε μία θέση από διαφορετικές μεταβάσεις. Προτείνουμε λοιπόν μια επέκταση των αναστρέψιμων δικτύων Πέτρι που επιτρέπει πολλαπλά διακριτικά του ίδιου τύπου σε ένα μοντέλο, ενώ παράλληλα διασφαλίζεται ο ντετερμινισμός κατά την αντιστροφή. Συγκεκριμένα, στην προσέγγιση την οποία διερευνούμε, διαφορετικά διακριτικά που βρίσκονται στην ίδια θέση μπορούν να διακριθούν με βάση την πορεία που έχουν ακολουθήσει στο δίκτυο. Αποδεικνύουμε ότι η εκφραστική ισχύς των αναστρέψιμων δικτύων Πέτρι με πολλαπλά διακριτικά είναι ισοδύναμη με εκείνη των αναστρέψιμων δικτύων Πέτρι με μοναδικά διακριτικά. Προτείνουμε επίσης την αντίθετη προσέγγιση, η οποία θεωρεί ότι όλα τα διακριτικά ενός συγκεκριμένου τύπου είναι πανομοιότυπα, αγνοώντας την πορεία που ακολούθησαν κατά την εκτέλεση του δικτύου. Δείχνουμε την ευρωστία αυτής της προσέγγισης ως τεχνική μοντελοποίησης συστημάτων που αφορούν πόρους μέσω ενός παραδείγματος από τη βιοχημεία, γνωστό ως αυτοπροτόλυση του νερού.
Και τα δύο προτεινόμενα μοντέλα αναστρέψιμων δικτύων Πέτρι (με μοναδικά ή πολλαπλά διακριτικά) επιτρέπουν την αντιστροφή μεταβάσεων χωρίς περιορισμούς ως προς το πότε και αν θα αντιστραφεί η εκτέλεση ή όχι. Με στόχο να περιορίσουμε την αναστρεψιμότητα, επεκτείνουμε τη σημασιολογία μας συσχετίζοντας τις μεταβάσεις με συνθήκες των οποίων η ικανοποίηση επιτρέπει την εκτέλεση μεταβάσεων προς τα εμπρός/πίσω.
Καταλήγοντας, για να διευκολύνουμε την ανάλυση της συμπεριφοράς μοντέλων αναστρέψιμου υπολογισμού διατυπώνουμε στο πλαίσιο μας βασικές ιδιότητες όπως η ασφάλεια και η προσβασημότητα όταν εφαρμόζονται διαφορετικές στρατηγικές αναστρεψιμότητας. Απεικονίζουμε το πλαίσιο μαζί με τις σχετικές ιδιότητες με ένα μοντέλο ενός καινοτόμου, κατανεμημένου αλγορίθμου που επιλέγει κεραίες σε κατανεμημένες σειρές κεραιών. Reversible computation is an unconventional form of computing that extends the standard forward-only mode of computation with the ability to execute a sequence of operations in reverse at any point during computation. Reversibility has recently been attracting increasing attention in various research communities, as on the one hand it promises low-power computation, and on the other hand it is inherent or of interest in a variety of applications.
Exploring reversibility through formal models formulates the theoretical foundations of what reversibility is, what purpose it serves, and how it benefits natural and artificial systems. As such, in this thesis we propose a reversible approach to Petri nets by introducing machinery and associated operational semantics to tackle the challenges of the main forms of reversibility. Petri nets are a mathematical language for modelling and reasoning about distributed systems. Our proposal concerns a variation of cyclic Petri nets, called Reversing Petri Nets (RPNs) where tokens are persistent and distinguished from each other by an identity. We demonstrate the applicability of our approach with a model of the ERK signalling pathway and an example of a transaction-processing system both featuring reversible behaviour.
An immediate extension of the original model includes allowing multiple tokens of the same base/type to occur in a model. The addition of token multiplicity into a model like Petri nets results in various backward conflicts where a token can be generated in a place because of different transition firings. We therefore propose an extension of reversing Petri nets that allows multiple tokens of the same base/type to occur in a model while still ensuring backward determinism. Specifically, we explore the individual token interpretation where one distinguishes different tokens residing in the same place by keeping track of where they come from. We prove that the expressive power of RPNs with multi tokens is equivalent to that of RPNs with single tokens, and we measure the expressiveness in terms of Labelled Transition Systems (LTSs) up to isomorphism of reachable parts that can be denoted by nets of the respective RPN models. We also propose the collective token interpretation, as the opposite approach to token ambiguity, which considers all tokens of a certain type to be identical, disregarding their history during execution. We show the robustness of this approach as a modelling technique for resource-aware systems by modelling an example from biochemistry, known as the autoprotolysis of water.
Both of the proposed models of RPNs (with single or multi tokens) implement the notion of uncontrolled reversibility, meaning that it specifies how to reverse an execution and allows to do so freely, yet it places no restrictions as to when and whether to prefer backward execution over forward execution or vice versa. In this respect, a further aim is to control reversibility by extending our formal semantics where transitions are associated with conditions whose satisfaction allows the execution of transitions in the forward/reversed direction.
Finally, in order to facilitate the analysis of the behaviour of reversible models, we formulate the basic properties of our framework such as safety, reachability, precedence and exception when different notions and strategies of reversibility are applied. We illustrate the framework along with the associated properties with a model of a novel, distributed algorithm for antenna selection in distributed antenna arrays.