Ein stetig wachsender Anteil des Aufwands zum Entwurf digitaler Schaltungen entfällt auf die funktionale Verifikation. Der Verifikationsraum als Menge aller möglichen Kombinationen von Attributen einer Komponente, d. h. der Parameter und Eingangsdaten, ist oftmals sehr groß, wodurch die Verifikation aller Kombinationen unpraktikabel wird. Deshalb verwenden moderne Methoden der funktionalen Verifikation die zufallsgesteuerte Erzeugung von Stimuli in Verbindung mit manuell definierten Spezialfällen, sog. Corner Cases, um eine möglichst hohe funktionale Abdeckung in der angestrebten Verteilung zu erzielen. Als großer Nachteil diese Ansätze führen steigende Abdeckungsanforderungen zu exponentiell ansteigenden Laufzeiten. Um diesen Nachteil auszugleichen, wurden Generatoren propagiert, die nur solche Kombinationen erzeugen, die nicht bereits abgedeckt worden sind. Leider können die dabei verwendeten Verfahren das Problem nicht zufriedenstellend lösen, da auch sie im Allgemeinen zufällige Kombinationen erzeugen, um in einem zweiten Schritt zu prüfen, ob diese bereits abgedeckt sind. Im vorliegenden Beitrag werden Entscheidungsdiagramme zur Repräsentation aller zulässigen Kombinationen innerhalb des Verifikationsraums verwendet. Mit Hilfe dieses analytischen Modells kann jede beliebige Anzahl von Kombinationen in linearer Zeit erzeugt werden. Wird die vorgestellte Methode auf die Zufallserzeugung zur funktionalen Verifikation angewendet, kann diese um Größenordnungen beschleunigt werden.

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.

Ein stetig wachsender Anteil des Aufwands zum Entwurf digitaler Schaltungen entfällt auf die funktionale Verifikation. Der Verifikationsraum als Menge aller möglichen Kombinationen von Attributen einer Komponente, d. h. der Parameter und Eingangsdaten, ist oftmals sehr groß, wodurch die Verifikation aller Kombinationen unpraktikabel wird. Deshalb verwenden moderne Methoden der funktionalen Verifikation die zufallsgesteuerte Erzeugung von Stimuli in Verbindung mit manuell definierten Spezialfällen, sog. Corner Cases, um eine möglichst hohe funktionale Abdeckung in der angestrebten Verteilung zu erzielen. Als großer Nachteil diese Ansätze führen steigende Abdeckungsanforderungen zu exponentiell ansteigenden Laufzeiten. Um diesen Nachteil auszugleichen, wurden Generatoren propagiert, die nur solche Kombinationen erzeugen, die nicht bereits abgedeckt worden sind. Leider können die dabei verwendeten Verfahren das Problem nicht zufriedenstellend lösen, da auch sie im Allgemeinen zufällige Kombinationen erzeugen, um in einem zweiten Schritt zu prüfen, ob diese bereits abgedeckt sind. Im vorliegenden Beitrag werden Entscheidungsdiagramme zur Repräsentation aller zulässigen Kombinationen innerhalb des Verifikationsraums verwendet. Mit Hilfe dieses analytischen Modells kann jede beliebige Anzahl von Kombinationen in linearer Zeit erzeugt werden. Wird die vorgestellte Methode auf die Zufallserzeugung zur funktionalen Verifikation angewendet, kann diese um Größenordnungen beschleunigt werden.

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.

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.