h1

000052467 001__ 52467
000052467 005__ 20230404110706.0
000052467 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-9383
000052467 0247_ $$2Laufende Nummer$$a25825
000052467 0247_ $$2HBZ$$aHT014154952
000052467 0247_ $$2OPUS$$a938
000052467 037__ $$aRWTH-CONV-114688
000052467 041__ $$aEnglish
000052467 082__ $$a004
000052467 1001_ $$0P:(DE-82)043055$$aNowack, Antje$$b0$$eAuthor
000052467 245__ $$aAbstract state machines: verification problems and computational power$$cvorgelegt von Antje Nowack$$honline, print
000052467 260__ $$aAachen$$bPublikationsserver der RWTH Aachen University$$c2004
000052467 300__ $$aIV, 181 S.
000052467 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000052467 3367_ $$02$$2EndNote$$aThesis
000052467 3367_ $$2DRIVER$$adoctoralThesis
000052467 3367_ $$2BibTeX$$aPHDTHESIS
000052467 3367_ $$2DataCite$$aOutput Types/Dissertation
000052467 3367_ $$2ORCID$$aDISSERTATION
000052467 502__ $$aAachen, Techn. Hochsch., Diss., 2004$$gFak01$$o2004-07-21
000052467 5203_ $$aAbstract State Machines (ASMs) bilden die Basis einer Methode zur Software-Spezifikation, welche Vorteile informaler Methoden (Verstaendlichkeit und Ausfuehrbarkeit der Spezifikation) mit Vorteilen formaler Methoden (Genauigkeit sowie Anwendbarkeit mathematischer Methoden und Ergebnisse) vereint. Anwendungen dieser Methode motivieren zahlreiche Berechnungs- und Entscheidungsprobleme. Die hohe Ausdrucksstaerke ist einer der Vorteile der ASMs, jedoch fuehrt sie fast unmittelbar zu Unentscheidbarkeits- bzw. Nichtberechenbarkeitsergebnissen im uneingeschraenkten Fall. Folglich gelangt man recht schnell zu der Frage, ob es ausdrucksstarke Klassen von ASMs gibt, fuer welche Enscheidbarkeits- und Berechenbarkeitsergebnisse bewiesen werden koennen. Im ersten Teil dieser Arbeit wird eine solche Klasse eingefuehrt. Diese ASMs werden bewachte ASMs genannt. Die Idee aehnelt derjenigen des bewachten Fragments der Logik erster Stufe, fuer welches Erfuellbarkeit entscheidbar ist. Weiterhin wird die Ausdrucksstaerke dieser Klasse analysiert und bewiesen, dass sie ausdrucksstaerker ist als Datalog LITE und als das bewachte Fragment der Fixpunktlogik erster Stufe. Im zweiten Teil der Arbeit wird die Entscheidbarkeit des allgemeiner Verifikationsprobleme betrachtet. Dies entspricht der Frage, ob alle Berechnungen einer ASM eine Eigenschaft erfuellen. Aufgrund der Unentscheidbarkeit im allgemeinen Fall, muessen die ASMs und die Eigenschaften eingeschraenkt werden, um Entscheidbarkeit zu erhalten. Bewachte ASMs bilden die Basis einer entscheidbaren Instanz des allgemeinen Verifikationsproblems. An diese Betrachtungen schliesst sich die Frage an nach der Moeglichkeit, die Beschraenkungen der ASMs abzuschwaechen, falls das Ziel nicht in der automatischen Verifikation sondern in Konzepten besteht, die Verifikation, Debugging, Testen unterstuetzen. Eine solches Konzept ist Slicing fuer ASMs, welches im dritten Teil dieser Arbeit eingefuehrt wird. Die Idee entspricht derjenigen des Program Slicing, dessen Ziel ist, diejenigen Anweisungen eines Programms zu bestimmen, welche sein Verhalten an einer gegebenen Stelle beeinflussen. Diese Anweisungen bilden wiederum ein syntaktisch korrektes Programm, welches Slice genannt wird. Bisherige Arbeiten haben Programmiersprachen betrachtet, deren Konzept sich grundsaetzlich von ASMs unterscheidet. Obwohl das Konzept des Program Slicing nicht direkt auf ASMs erweitert werden kann, laesst sich ein entsprechendes Konzept fuer ASMs finden. Ein solcher Ansatz wird hier vorgestellt. Obwohl ein minimaler Slice im Allgemeinen nicht berechenbar ist, wird bewiesen, dass ein minimaler Slice fuer bewachte ASMs berechenbar ist. Dieses Ergebnis kann auf mehrere Arten erweitert werden. Einige Erweiterungen auf groessere Klassen von ASMs sowie weitere Varianten des Slicing-Begriffs werden vorgestellt. Im vierten Teil dieser Arbeit wird die Betrachtungsweise der ASMs etwas veraendert. ASMs werden nicht nur als Spezifikationsformalismus gesehen sondern als Berechnungsmodell. Die ASM-These besagt, dass jeder Algorithmus, gleich welcher Art, schrittweise und auf seinem natuerlichen Abstraktionsniveau durch eine ASM simuliert werden kann. Diese These wurde fuer sequentielle und parallele synchrone Algorithmen von grundlegenden Prinzipien abgeleitet. Das Hauptergebnis dieses Teils ist, dass die ASM-These auch fuer Quanten-Algorithmen gilt.$$lger
000052467 520__ $$aAbstract State Machines (ASMs) provide the basis of a a formal method combining advantages of informal methods (understandability, executability) and advantages of formal methods (precision and applicability of mathematical methods and results). Applications of this method motivate numerous computability and decidability problems. The high expressive power is one of the advantages of ASMs but it leads rather directly to undecidability respectively uncomputability results in the unrestricted case. Consequently, we arrive rather early at the question whether there exist expressive classes of ASMs for which we can prove decidability and computability results. In the first part of this thesis, we introduce such a class called guarded ASMs. The idea is similar to the one of the guarded fragment of first-order logic for which satisfiability is decidable. We analyze the expressive power of this class and prove that it is (strictly) stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. In the second part of this thesis, we study the decidability of general verification problems for ASMs corresponding to the question whether all computations of an ASM satisfy a property (usually expressed in some temporal logic). Because of undecidability in the general case, we have to restrict the ASMs and the properties in order to obtain decidability results. Guarded ASMs provide the basis of a decidable instance of the general verification problem. It is rather straightforward to ask for the possibility to weaken the restrictions on the ASMs if we do not aim automatic verification but concepts supporting verification, debugging and testing. One such possibility is the concept of slicing ASMS which we introduce in the third part of this work. The idea is analogous to the one of program slicing aiming to extract statements from a program that are relevant for its behavior at a given point of interest. These statements form again a syntactically correct program called a slice. Previous work has focused on programming languages that differ substantially from ASMs. Although the concept of program slicing does not directly extend to ASMs, it is possible to find an analogous concept for ASMs. We present such an approach. In spite of the fact that a minimal slice is not computable in the general case, we prove that a minimal slice is computable for guarded ASMs. This basic result can be extended in several ways. We present some extensions to larger classes of ASMs and other variants for the notion of slicing. In the fourth part of this thesis, we change our point of view. We do not merely consider ASMs as a specification formalism but as a computation model. The ASM thesis says that every algorithm, of any kind, can be modeled step by step and on its natural abstraction level by an ASM. The thesis has been derived from basic principles for sequential algorithms, and for parallel synchronous algorithms. The main result of this part is that the ASM thesis also holds for quantum algorithms.$$leng
000052467 591__ $$aGermany
000052467 653_7 $$aInformatik
000052467 653_7 $$2eng$$aAbstract State Machines
000052467 653_7 $$2eng$$aASMs
000052467 653_7 $$2eng$$averification
000052467 653_7 $$2eng$$aslicing
000052467 653_7 $$2eng$$aquantum algorithms
000052467 650_7 $$2SWD$$aAbstrakte Zustandsmaschine
000052467 650_7 $$2SWD$$aVerifikation
000052467 650_7 $$2SWD$$aFormale Methode
000052467 650_7 $$2SWD$$aEntscheidbarkeit
000052467 650_7 $$2SWD$$aBerechenbarkeit
000052467 650_7 $$2SWD$$aProgram Slicing
000052467 7001_ $$0P:(DE-82)IDM00039$$aGrädel, Erich$$b1$$eThesis advisor
000052467 8564_ $$uhttps://publications.rwth-aachen.de/record/52467/files/Nowack_Antje.pdf
000052467 8564_ $$uhttps://publications.rwth-aachen.de/record/52467/files/52467_kardex.pdf$$yInternal catalog entry
000052467 909CO $$ooai:publications.rwth-aachen.de:52467$$pdnbdelivery$$pVDB$$pdriver$$purn$$popen_access$$popenaire
000052467 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000052467 9201_ $$0I:(DE-82)100000_20140620$$k100000$$lFakultät für Mathematik, Informatik und Naturwissenschaften$$x0
000052467 961__ $$c2014-05-23$$x2004-10-20$$z2012-02-20
000052467 970__ $$aHT014154952
000052467 980__ $$aphd
000052467 980__ $$aI:(DE-82)100000_20140620
000052467 980__ $$aVDB
000052467 980__ $$aUNRESTRICTED
000052467 980__ $$aConvertedRecord
000052467 9801_ $$aFullTexts
000052467 980__ $$aFullTexts