Academic literature on the topic 'Binäres Entscheidungsdiagramm'

Equivalence checking ist in der Industrie die zur Zeit am meisten eingesetzte formale Verifikationstechnik. Während viele konventionelle Verfahren der formalen Verifikation auf binären Entscheidungsdiagrammen und einer geeigneten funktionalen Repräsentation der Schaltung beruhen, kommen im Bereich des Equivalence Checkings vorwiegend sogenannte strukturelle Verfahren zum Einsatz. In diesem Artikel werden die grundlegenden Konzepte dieser Verfahren vorgestellt und gezeigt, wie strukturelle Eigenschaften einer Schaltung ausgenutzt werden können, um den Rechenaufwand bei der Lösung formaler Verifikationsprobleme drastisch zu reduzieren.

Seit langem ist die Intelligenz des Menschen für viele Forscher und Philosophen ein faszinierendes Forschungsobjekt. Mit dem Aufkommen der Computertechnik erscheint nun zum ersten mal der Traum, einige dieser typisch menschlichen Fähigkeiten nicht nur zu verstehen, sondern nachbauen oder in Teilgebieten gar übertreffen zu können, als realistisch. Ein wichtiger Teil dieses mit "Künstliche Intelligenz" überschriebenen Forschungsgebietes ist das Schließen über Aktionen und Veränderung. Hier wird versucht, die menschliche Fähigkeit, die Effekte seiner Aktionen vorauszusehen und Pläne zum Erreichen von Zielen zu schmieden, nachzubilden. Ein aktives Forschungsgebiet in diesem Rahmen ist der Fluentkalkül, ein Formalismus zur Modellierung von Aktionen und Veränderung. Er stellt Mittel bereit, in der ein automatischer Agent seine Umgebung und die Effekte seiner Aktionen im Rahmen der mathematischen Logik darstellen kann, um mit Hilfe von logischem Schließen sein Verhalten zu planen. Obwohl zum Fluentkalkül viele Arbeiten existieren, die dessen Anwendungsbereiche und Semantik erweitern, gibt es doch noch relativ wenige Arbeiten zum effizienten Schlussfolgern. Dies ist ein Hauptaugenmerk der vorliegenden Arbeit. Es wird ein Algorithmus geschaffen, der Erkenntnisse aus effizienten Verfahren zum Modelchecking mit Binären Entscheidungsdiagrammen (BDDs) sinngemäß überträgt und für ein Fragment des Fluentkalkül erweitert. Damit können nun auch Planungsprobleme von Fluentkalkül-Planern gelöst werden, die der realisierten symbolischen Breitensuche besser zugänglich sind, als der bisher aussschliesslich verwendeten heuristischen Tiefensuche. Um eine leichtere Vergleichbarkeit Fluentkalkül-basierter Planungsverfahren mit anderen Planungsalgorithmen zu ermöglichen, wurde eine Übersetzung des ADL-Fragments der Planungsdomänenbeschreibungssprache PDDL in den Fluentkalkül geschaffen. Damit können zahlreiche Planungsprobleme aus der Literatur und Planungsdomänenbibliotheken auch mit Fluentkalkül-Planern bearbeitet werden. Die Übersetzung kann zugleich als formale Semantik des nur informal spezifizierten PDDL dienen.

Seit langem ist die Intelligenz des Menschen für viele Forscher und Philosophen ein faszinierendes Forschungsobjekt. Mit dem Aufkommen der Computertechnik erscheint nun zum ersten mal der Traum, einige dieser typisch menschlichen Fähigkeiten nicht nur zu verstehen, sondern nachbauen oder in Teilgebieten gar übertreffen zu können, als realistisch. Ein wichtiger Teil dieses mit "Künstliche Intelligenz" überschriebenen Forschungsgebietes ist das Schließen über Aktionen und Veränderung. Hier wird versucht, die menschliche Fähigkeit, die Effekte seiner Aktionen vorauszusehen und Pläne zum Erreichen von Zielen zu schmieden, nachzubilden. Ein aktives Forschungsgebiet in diesem Rahmen ist der Fluentkalkül, ein Formalismus zur Modellierung von Aktionen und Veränderung. Er stellt Mittel bereit, in der ein automatischer Agent seine Umgebung und die Effekte seiner Aktionen im Rahmen der mathematischen Logik darstellen kann, um mit Hilfe von logischem Schließen sein Verhalten zu planen. Obwohl zum Fluentkalkül viele Arbeiten existieren, die dessen Anwendungsbereiche und Semantik erweitern, gibt es doch noch relativ wenige Arbeiten zum effizienten Schlussfolgern. Dies ist ein Hauptaugenmerk der vorliegenden Arbeit. Es wird ein Algorithmus geschaffen, der Erkenntnisse aus effizienten Verfahren zum Modelchecking mit Binären Entscheidungsdiagrammen (BDDs) sinngemäß überträgt und für ein Fragment des Fluentkalkül erweitert. Damit können nun auch Planungsprobleme von Fluentkalkül-Planern gelöst werden, die der realisierten symbolischen Breitensuche besser zugänglich sind, als der bisher aussschliesslich verwendeten heuristischen Tiefensuche. Um eine leichtere Vergleichbarkeit Fluentkalkül-basierter Planungsverfahren mit anderen Planungsalgorithmen zu ermöglichen, wurde eine Übersetzung des ADL-Fragments der Planungsdomänenbeschreibungssprache PDDL in den Fluentkalkül geschaffen. Damit können zahlreiche Planungsprobleme aus der Literatur und Planungsdomänenbibliotheken auch mit Fluentkalkül-Planern bearbeitet werden. Die Übersetzung kann zugleich als formale Semantik des nur informal spezifizierten PDDL dienen.

Binary Decision Diagrams (BDDs) sind eine Datenstruktur für Boolesche Funktionen, die auch unter dem Namen branching program bekannt ist. In ordered binary decision diagrams (OBDDs) müssen die Tests einer festen Variablenordnung genügen. In free binary decision diagrams (FBDDs) darf jede Variable höchstens einmal getestet werden. Die Effizienz neuer Varianten des BDD-Konzepts wird gewöhnlich anhand spektakulärer (worst-case) Beispiele aufgezeigt. Wir verfolgen einen anderen Ansatz und vergleichen die Darstellungsgrößen für fast alle Booleschen Funktionen. Während I. Wegener bewiesen hat, daß für die `meisten' n die erwartete OBDD-Größe einer zufälligen Booleschen Funktion von n Variablen gleich der worst-case Größe bis auf Terme kleinerer Ordnung ist, zeigen wir daß dies nicht der Fall ist für n innerhalb von Intervallen konstanter Länge um die Werte n = 2h + h. Ferner gibt es Bereiche von n, in denen minimale FBDDs fast immer um mindestens einen konstanten Faktor kleiner sind als minimale OBDDs. Unsere Hauptsätze ha ben doppelt exponentielle Wahrschein- lichkeitsschranken (in n). Außerdem untersuchen wir die Entwicklung zufälliger OBDDs und ihrer worst-case Größe und decken dabei ein oszillierendes Verhalten auf, das erklärt, warum gewisse Aussagen im allgemeinen nicht verstärkt werden können.
Binary Decision Diagrams (BDDs) are a data structure for Boolean functions which are also known as branching programs. In ordered binary decision diagrams (OBDDs), the tests have to obey a fixed variable ordering. In free binary decision diagrams (FBDDs), each variable can be tested at most once. The efficiency of new variants of the BDD concept is usually demonstrated with spectacular (worst-case) examples. We pursue another approach and compare the representation sizes of almost all Boolean functions. Whereas I. Wegener proved that for `most' values of n the expected OBDD size of a random Boolean function of n variables is equal to the worst-case size up to terms of lower order, we show that this is not the case for n within intervals of constant length around the values n = 2h + h. Furthermore, ranges of n exist for which minimal FBDDs are almost always at least a constant factor smaller than minimal OBDDs. Our main theorems have doubly exponentially small probability bounds (in n). We also investigate the evolution of random OBDDs and their worst-case size, revealing an oscillating behaviour that explains why certain results cannot be improved in general.

Sound criteria for partial order reduction for probabilistic concurrent systems have been presented in the literature. Their realization relies on a depth-first search-based approach for generating the reduced model. The drawback of this dynamic approach is that it can hardly be combined with other techniques to tackle the state explosion problem, e.g., symbolic probabilistic model checking with multi-terminal variants of binary decision diagrams. Following the approach presented by Kurshan et al. for non-probabilistic systems, we study partial order reduction techniques for probabilistic concurrent systems that can be realized by a static analysis. The idea is to inject the reduction criteria into the control flow graphs of the processes of the system to be analyzed. We provide the theoretical foundations of static partial order reduction for probabilistic concurrent systems and present algorithms to realize them. Finally, we report on some experimental results.

Sound criteria for partial order reduction for probabilistic concurrent systems have been presented in the literature. Their realization relies on a depth-first search-based approach for generating the reduced model. The drawback of this dynamic approach is that it can hardly be combined with other techniques to tackle the state explosion problem, e.g., symbolic probabilistic model checking with multi-terminal variants of binary decision diagrams. Following the approach presented by Kurshan et al. for non-probabilistic systems, we study partial order reduction techniques for probabilistic concurrent systems that can be realized by a static analysis. The idea is to inject the reduction criteria into the control flow graphs of the processes of the system to be analyzed. We provide the theoretical foundations of static partial order reduction for probabilistic concurrent systems and present algorithms to realize them. Finally, we report on some experimental results.