We talk about the problem of bounding transition systems which occurs in planning and model checking. It consists of answering the question how long transition sequences fulfilling certain criteria can be at maximum. The approach of compositional bounding splits a transition system into smaller parts, which then are bounded using base case functions, and composed to compute a total bound of the system. We use the recurrence diameter and the sublist diameter as base case functions. They are both properties of transition systems but impose bounds of different tightness on them. For the recurrence diameter, we give a SAT encoding and for the sublist diameter we give a QBF encoding. Both encodings are implemented and evaluated in Standard ML.     «

We talk about the problem of bounding transition systems which occurs in planning and model checking. It consists of answering the question how long transition sequences fulfilling certain criteria can be at maximum. The approach of compositional bounding splits a transition system into smaller parts, which then are bounded using base case functions, and composed to compute a total bound of the system. We use the recurrence diameter and the sublist diameter as base case functions. They are both...     »

Wir behandeln das Problem der Beschränkung von Transitionssystemen, das bei Planung und Model Checking auftritt. Es geht um die Frage, wie lang Transitionssequenzen, die bestimmte Kriterien erfüllen, maximal sein können. Der Ansatz des kompositionellen Beschränkens zerlegt ein Transitionssystem in kleinere Teile, die dann mit Hilfe von Basisfallfunktionen beschränkt und zusammengesetzt werden, um eine obere Schranke für das gesamte System zu berechnen. Wir verwenden den Recurrence-Durchmesser und den Sublist-Durchmesser als Basisfallfunktionen. Beide beschreiben Eigenschaften von Transitionssystemen, liefern jedoch unterschiedlich enge Schranken. Für den Recurrence-Durchmesser geben wir eine Kodierung in SAT an und für den Sublist-Durchmesser eine Kodierung in QBF. Beide Kodierungen sind in Standard ML implementiert und ausgewertet.     «

Wir behandeln das Problem der Beschränkung von Transitionssystemen, das bei Planung und Model Checking auftritt. Es geht um die Frage, wie lang Transitionssequenzen, die bestimmte Kriterien erfüllen, maximal sein können. Der Ansatz des kompositionellen Beschränkens zerlegt ein Transitionssystem in kleinere Teile, die dann mit Hilfe von Basisfallfunktionen beschränkt und zusammengesetzt werden, um eine obere Schranke für das gesamte System zu berechnen. Wir verwenden den Recurrence-Durchmesser u...     »