Bei der Untersuchung von Zustandsräumen nebenläufiger und reaktiver Systeme tritt das bekannte Problem der Zustandsraum-Explosion zutage. Zahlreiche Methoden sind in den letzten Jahren entwickelt und in Werkzeugen implementiert worden, um über geschickte Codierungen des Zustandsraumes dennoch eine Exploration zu ermöglichen, z.B. BDDs, Kronecker-Algebren, das Ausnutzen von Symmetrien oder Netzentfaltungen. Die (maximale) Entfaltung eines beschränkten Petri-Netzes ist eine halb- geordnete Darstellung, in der in einem einzigen (im allgemeinen unendlichen) Objekt alle möglichen Abläufe des modellierten Systems repräsentiert werden. Für Fragen wie Erreichbarkeit oder Verklemmung ist bereits ein gewisses endliches Anfangsstück der maximalen Entfaltung ausreichend. Dieses Präfix enthält, in einer kompakten Repräsentation, Informationen über alle erreichbaren Zustände. McMillan hat einen Algorithmus zur Konstruktion eines endlichen Anfangsstücks der Netzentfaltung beschrieben, das groß genug ist, daß darin alle erreichbaren Markierungen enthalten sind. Die Arbeit beschreibt einige Verbesserungen dieses Algorithmus, die unter anderem garantieren, daß die Größe des generierten Präfixes die Zahl der erreichbaren Markierungen (bis auf eine Konstante) nicht übersteigt. Den Schwerpunkt hierbei bilden Betrachtungen zur effizienten Realisierung des Verfahrens, die eine Untersuchung von Systemen mit Zustandsräumen in der Größenordnung mehrerer Zehnerpotenzen in überschaubarer Zeit gestattet. Die dieser Implementierung zugrundeliegenden Datenstrukturen, Funktionen und Heuristiken werden beschrieben. In einem weiteren Schwerpunkt wird aufgezeigt, wie mit Hilfe der Entfaltungstechnik Eigenschaften von Programmen, die in einer parallelen Hochsprache spezifiziert sind, untersucht werden können. Syntax und Semantik dieser Sprache, DB(PN)^2, werden entwickelt, deren Datentypen einen (potentiell) unendlichen Wertebereich aufweisen dürfen. Die anschließenden Betrachtungen beschreiben einen Algorithmus, der zu einem in dieser Sprache geschriebenen Programm ein endliches Präfix der Entfaltung konstruiert. Die Präfix-Generierung ist zentrales Modul einer Verifikationsumgebung zur Analyse nebenläufiger Systeme. Das konstruierte Präfix dient beispielsweise als Eingabe verschiedener nachgeschalteter Model-Checker basierend auf unterschiedlichen temporalen Logiken. Das Zusammenspiel dieser einzelnen Komponenten wird erläutert. Implementierungsaspekte und experimentelle Ergebnisse einer konkreten, effizienten Umsetzung der vorgestellten Algorithmen runden die Arbeit ab.     «

Bei der Untersuchung von Zustandsräumen nebenläufiger und reaktiver Systeme tritt das bekannte Problem der Zustandsraum-Explosion zutage. Zahlreiche Methoden sind in den letzten Jahren entwickelt und in Werkzeugen implementiert worden, um über geschickte Codierungen des Zustandsraumes dennoch eine Exploration zu ermöglichen, z.B. BDDs, Kronecker-Algebren, das Ausnutzen von Symmetrien oder Netzentfaltungen. Die (maximale) Entfaltung eines beschränkten Petri-Netzes ist eine halb- geordnete Darstel...     »

The investigation of state spaces of concurrent and reactive systems raises the known problem of the state space explosion. In recent years, many methods were developed and have been implemented in various tools which make it possible to explore the state space, for example, BDDs, Kronecker algebras, usage of symmetries, or net unfoldings. The (maximal) unfolding of a bounded Petri net is a partially ordered representation that describes all possible executions of a system in one single object. Properties like reachability or deadlocks can already be answered by using a special finite prefix of that maximal unfolding. McMillan described an algorithm to construct a finite prefix of an unfolding that is large enough such that it already contains all reachable markings of a given system. The thesis describes some improvements of that algorithm, for example, it can be guaranteed that the size of the prefix never is larger (up to a constant factor) than the number of reachable markings. The main emphasis is put here on considerations for an efficient implementation of the procedure that allow the investigation of state spaces of several magnitudes in size in a reasonable time. The relevant data structures, functions and heuristics are explained in detail. Another section describes how properties of programs given in a special high-level language can be efficiently examined using net unfoldings. Syntax and semantics of this language called DB(PN)^2 (short for 'Distributed Basic Petri Net Programming Notation') are developed, whose data types can have a (potentially) infinite range. An algorithm for the construction of a finite prefix out of this language is derived. The prefix generation is the central module in a verification environment designed for the analysis of concurrent systems. The computed prefix serves as an input for various model checkers that are based on temporal logics. The interplay of these components is described. Implementational aspects and experimental results of a concrete efficient realisation of the described algorithms conclude the thesis.     «

The investigation of state spaces of concurrent and reactive systems raises the known problem of the state space explosion. In recent years, many methods were developed and have been implemented in various tools which make it possible to explore the state space, for example, BDDs, Kronecker algebras, usage of symmetries, or net unfoldings. The (maximal) unfolding of a bounded Petri net is a partially ordered representation that describes all possible executions of a system in one single object....     »