💻 computer science

Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

Die Autoren entwickeln ein einheitliches Framework für verhaltensbasierte Distanzen und zugehörige Logiken, das die polynomielle Extraktion unterscheidender Formeln für verschiedene quantitative Systeme, einschließlich Markov-Ketten, ermöglicht.

Ursprüngliche Autoren: Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora

Veröffentlicht 2026-02-13

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stell dir vor, du hast zwei Roboter, die sich fast genau gleich verhalten. Sie laufen durch ein Labyrinth, machen fast die gleichen Schritte und treffen fast die gleichen Entscheidungen. Aber sind sie exakt gleich? Oder gibt es winzige Unterschiede, die sie doch zu zwei verschiedenen Maschinen machen?

In der Welt der Informatik und Mathematik gibt es zwei Arten, solche Systeme zu vergleichen:

Der strenge Richter (Äquivalenz): Er sagt nur „Ja" oder „Nein". Sind die Roboter identisch? Wenn ja, sind sie gleich. Wenn nein, sind sie komplett unterschiedlich. Das ist oft zu grob.
Der feinfühlige Messer (Distanz): Er sagt: „Roboter A ist zu 98 % wie Roboter B, aber bei Schritt 5 weichen sie um 2 % ab." Das ist viel genauer.

Dieser Artikel von Jonas Forster und seinem Team beschäftigt sich mit dem zweiten Ansatz. Sie wollen nicht nur messen, wie unterschiedlich zwei Systeme sind, sondern auch beweisen, warum sie unterschiedlich sind. Sie wollen ein „Gedächtnis" oder eine „Beschwerde" (eine Formel) erstellen, die genau den Punkt findet, an dem die beiden Roboter sich trennen.

Hier ist die einfache Erklärung ihrer Arbeit, gespickt mit ein paar Metaphern:

1. Das Problem: Der „Toleranz-Test"

Stell dir vor, du hast zwei Wettervorhersage-Apps. Beide sagen: „Morgen regnet es mit 80 % Wahrscheinlichkeit."

App A sagt: 80 %.
App B sagt: 79 %.

Für einen strengen Richter sind sie unterschiedlich. Aber für einen Menschen ist der Unterschied winzig. Die Autoren nennen das $\epsilon$ -Ähnlichkeit (sprich: Epsilon-Ähnlichkeit). Das bedeutet: „Solange der Unterschied kleiner als ein gewisses Maß $\epsilon$ (z. B. 1 %) ist, sind die Apps für uns gleichwertig."

Das Problem ist: Wie berechnet man diesen Unterschied effizient? Und wie findet man eine Formel, die beweist: „Schau her, hier unterscheiden sich die Apps um mehr als 1 %"?

2. Die Lösung: Ein neues Regelwerk (Der Rahmen)

Die Autoren haben ein universelles Regelwerk entwickelt, das auf fast alle Arten von Systemen passt (ob es nun Roboter, Wetter-Apps oder Finanzmodelle sind).

Stell dir vor, sie haben einen Baukasten entwickelt.

Die Bausteine: Das sind die „Modalitäten". Das sind Werkzeuge, um Fragen zu stellen. Bei einer Wetter-App wäre das Werkzeug: „Wie hoch ist die Wahrscheinlichkeit für Regen?"
Die Magie: Normalerweise sagen diese Werkzeuge nur „Ja" oder „Nein". Die Autoren haben diese Werkzeuge so umgebaut, dass sie nun Zahlen liefern (z. B. „79,5 %").

Sie nennen diese umgebauten Werkzeuge „Sugeno-Modalitäten". Das klingt kompliziert, ist aber im Grunde wie ein Filter, der aus einer einfachen Ja/Nein-Frage eine genaue Messung macht.

3. Das Spiel: Der „Spoiler" und der „Duplicator"

Um herauszufinden, ob zwei Systeme unterschiedlich sind, spielen die Autoren ein imaginäres Spiel zwischen zwei Figuren:

Der Duplicator (Der Nachahmer): Er behauptet: „Die beiden Systeme sind fast gleich!"
Der Spoiler (Der Störfaktor): Er versucht, einen Beweis zu finden, dass sie nicht gleich sind.

Das Spiel läuft so ab:

Der Spoiler zeigt auf einen Unterschied: „Schau, bei App A ist die Regenwahrscheinlichkeit für Stadt X höher als bei App B!"
Der Duplicator muss nun beweisen, dass es trotzdem eine Verbindung gibt, die den Unterschied erklärt.
Wenn der Duplicator keine Antwort hat, hat der Spoiler gewonnen.

Das Geniale an dieser Arbeit: Die Autoren haben einen Algorithmus (einen Rezeptplan) entwickelt, der das Spiel für den Spoiler gewinnt und dabei sofort die Beweis-Formel schreibt.

4. Der große Durchbruch: Schnelle Beweise

Früher dauerte es oft ewig, bis man einen solchen Beweis fand, besonders wenn die Systeme komplex waren. Die Formeln wurden riesig wie ein unendlicher Baum.

Die Autoren zeigen jedoch:

Man kann diese Beweise schnell finden (in „polynomieller Zeit" – das bedeutet, es geht schnell, auch bei großen Systemen).
Die Beweise sind kompakt. Stell dir vor, statt einen riesigen Baum zu zeichnen, zeichnen sie einen effizienten Diagramm-Plan (einen „DAG"), bei dem gleiche Teile nur einmal gezeichnet werden.

5. Warum ist das wichtig? (Die Anwendung)

Warum sollten wir uns dafür interessieren?

Sicherheit: Wenn du ein autonomes Auto programmierst, willst du wissen: „Wenn ich das System leicht ändere (z. B. durch einen Software-Update), verhält es sich noch sicher genug?" Die Autoren können dir eine Formel geben, die genau sagt: „Hier ist der Unterschied zu groß, das ist unsicher!"
Künstliche Intelligenz: In der KI werden oft Modelle trainiert. Wenn zwei Modelle fast gleich sind, aber eines etwas schneller, kann man dieses Wissen nutzen, um bessere Modelle zu bauen.
Datenschutz: Wenn man Daten verschleiert (z. B. in der Medizin), muss man sicherstellen, dass die verschleierten Daten nicht zu sehr von den echten abweichen. Diese Methode hilft, die Grenze genau zu messen.

Zusammenfassung in einem Satz

Die Autoren haben eine universelle, schnelle Methode entwickelt, um nicht nur zu messen, wie unterschiedlich zwei komplexe Systeme sind, sondern auch, um sofort einen kompakten mathematischen Beweis zu liefern, der genau erklärt, wo und warum diese Unterschiede auftreten – selbst wenn man nur eine kleine Toleranzgrenze zulässt.

Es ist, als hätten sie ein Werkzeug erfunden, das nicht nur sagt „Diese beiden Uhren gehen unterschiedlich", sondern sofort ein Zertifikat ausstellt, das besagt: „Uhre A hat bei Sekunde 5 eine Verzögerung von 0,02 Sekunden gegenüber Uhr B, und hier ist der exakte Weg, wie man das nachweisen kann."

1. Problemstellung

In der Analyse quantitativer Systeme (z. B. probabilistische, gewichtete oder nicht-deterministische Systeme) bieten Verhaltensdistanzen (behavioural distances) oft eine feinere und stabilere Vergleichsmethode als klassische, binäre Verhaltensäquivalenzen. Während Äquivalenzen nur zwischen „gleich" und „ungleich" unterscheiden, quantifizieren Distanzen den Grad der Ähnlichkeit.

Ein zentrales Problem in diesem Bereich ist die algorithmische Charakterisierung dieser Distanzen durch logische Formeln. Insbesondere geht es darum, unterscheidende Formeln (distinguishing formulae) zu berechnen, die beweisen, dass zwei Zustände eines Systems eine bestimmte Distanz überschreiten. Bisherige Ansätze waren oft auf spezifische Systemtypen (wie Markov-Ketten) beschränkt oder lieferten keine effizienten Algorithmen für die Berechnung dieser Formeln (oft exponentieller Aufwand).

Das Paper adressiert die Frage, wie man ein einheitliches Framework für schwellenwertbasierte Verhaltensdistanzen (threshold-based behavioural distances) entwickeln kann, das auf dem Konzept von $\varepsilon$ -Bisimulationen basiert, und wie man daraus effizient (polynomiell) unterscheidende Formeln in dedizierten modalen Logiken extrahieren kann.

2. Methodik und Framework

Die Autoren nutzen den Ansatz der universellen Koalgebra (universal coalgebra), um verschiedene Systemtypen (Markov-Ketten, metrische Übergangssysteme, fuzzy Systeme) in einem einheitlichen mathematischen Rahmen zu beschreiben.

2-to-V Prädikatenliftings: Das Framework startet mit der Wahl einer Menge von 2-to-V Prädikatenliftings. Diese heben zweiwertige Prädikate (Teilmengen) auf quantitative Prädikate (Werte im Einheitsintervall $V = [0,1]$ ) über dem Bild des Funktors $F$ (der den Systemtyp definiert) an. Ein klassisches Beispiel ist der Wahrscheinlichkeitsoperator, der einer Menge die Wahrscheinlichkeit zuordnet.
$\varepsilon$ -(Bi-)Simulation: Basierend auf diesen Liftings wird eine $\varepsilon$ -Simulation definiert. Zwei Zustände sind $\varepsilon$ -similiar, wenn sich ihre Verhaltensweisen unter allen Modaliäten um höchstens $\varepsilon$ unterscheiden. Die induzierte Distanz $d_\Lambda$ ist das Infimum aller $\varepsilon$ , für die eine solche Simulation existiert.
Lax Extensions: Die Autoren zeigen, dass diese Distanzen äquivalent durch eine quantitative lax extension $L_\Lambda$ charakterisiert werden können, die direkt aus den 2-to-V Liftings abgeleitet wird.
Sugeno-Modaliäten: Um eine quantitative Logik zu konstruieren, transformieren die Autoren die 2-to-V Liftings in V-to-V Liftings mittels Sugeno-Integration. Diese neuen Modaliäten werden als Sugeno-Modaliäten bezeichnet.
Codensity-Spiele: Zur Berechnung der Formeln wird ein Spoiler-Duplicator-Spiel (Codensity-Spiel) eingeführt. Der Spoiler versucht, eine Distanz größer als $\varepsilon$ nachzuweisen, indem er Prädikate wählt, die die Simulation brechen. Die Gewinnstrategien des Spoilers dienen als Grundlage für die Konstruktion der Formeln.

3. Schlüsselbeiträge

Das Paper liefert vier Hauptbeiträge:

Äquivalenz von Distanzdefinitionen: Es wird bewiesen, dass die durch $\varepsilon$ -(Bi-)Simulationen definierte Verhaltensdistanz exakt mit der durch die quantitative lax extension $L_\Lambda$ induzierten Distanz übereinstimmt (Satz 3.9). Dies verallgemeinert bekannte Ergebnisse, z. B. die Charakterisierung der $\varepsilon$ -Distanz auf Markov-Ketten durch die Lévy-Prokhorov-Metrik.
Konstruktion der Sugeno-Logik: Aus den 2-to-V Liftings werden quantitative Sugeno-Modaliäten abgeleitet. Es wird gezeigt, dass die durch diese Modaliäten induzierte quantitative Logik die schwellenwertbasierte Verhaltensdistanz auf endlich verzweigenden Systemen charakterisiert (Satz 6.10). Im probabilistischen Fall entspricht dies der bekannten „generally"-Modality.
Zweiwertige Logik mit $\varepsilon$ -Erfüllung: Es wird eine zweiwertige modale Logik eingeführt, die ein Erfüllungskonzept „bis zu $\varepsilon$ " ( $\varepsilon$ -satisfaction) besitzt. Diese Logik charakterisiert ebenfalls die Verhaltensdistanz (Satz 5.8). Für Markov-Ketten ergibt dies die bekannte Logik von Desharnais et al., nun aber auf endlich verzweigende Systeme beschränkt und erweitert.
Polynomielle Extraktion von Formeln: Der wichtigste algorithmische Beitrag ist die Entwicklung von Algorithmen (Algorithm 1 und 2), die aus Gewinnstrategien des Spoilers im Codensity-Spiel unterscheidende Formeln extrahieren.
- Die extrahierten Formeln haben eine polynomielle DAG-Größe (Directed Acyclic Graph), was effizienter ist als die oft exponentielle Baumgröße.
- Unter milden Annahmen (Polynomielle Lösbarkeit der Liftings) laufen die Algorithmen in polynomieller Zeit.

4. Ergebnisse und Beispiele

Die generischen Ergebnisse werden auf mehrere bekannte und neue Fälle angewendet:

Markov-Ketten (Lévy-Prokhorov-Distanz):
- Es wird gezeigt, dass die Lévy-Prokhorov-Distanz durch die Sugeno-Modality (die „generally"-Modality) charakterisiert wird.
- Neu: Polynomielle Berechnung von unterscheidenden Formeln (sowohl zweiwertig als auch quantitativ) für die Lévy-Prokhorov-Distanz auf Markov-Ketten. Dies ist ein signifikanter Fortschritt gegenüber früheren Arbeiten, die keine effizienten Algorithmen für die Formelgröße lieferten.
Generative Probabilistische Transitionssysteme: Verallgemeinerung der obigen Ergebnisse auf Systeme mit Labels.
Fuzzy Transitionssysteme: Die Sugeno-Modality entspricht hier dem klassischen „fuzzy diamond". Die Ergebnisse liefern neue charakteristische Logiken und polynomielle Extraktionsalgorithmen für diese Systeme.
Metrische Transitionssysteme: Die Framework-Resultate bestätigen und erweitern bekannte Ergebnisse für metrische Systeme, einschließlich der polynomiellen Extraktion von Formeln.

Ein wichtiger Unterschied zu anderen Distanzen (wie der Kantorovich-Distanz, die auf Erwartungswerten basiert) ist, dass das Framework speziell auf Schwellenwerte (Thresholds) ausgelegt ist. Die Kantorovich-Distanz wird explizit als nicht durch dieses Framework abgedeckt erwähnt, obwohl es Überschneidungen bei der Charakterisierung gibt.

5. Bedeutung und Fazit

Die Arbeit stellt einen bedeutenden theoretischen und algorithmischen Durchbruch dar:

Einheitlichkeit: Sie bietet das erste einheitliche Framework, das verschiedene Arten von schwellenwertbasierten Distanzen (probabilistisch, fuzzy, metrisch) unter einem Dach vereint.
Effizienz: Der Nachweis der polynomiellen Berechenbarkeit von unterscheidenden Formeln ist entscheidend für die praktische Anwendbarkeit. Bisher waren solche Berechnungen oft als exponentiell bekannt oder nicht effizient implementierbar.
Verbindung von Logik und Metrik: Die Arbeit schließt die Lücke zwischen der semantischen Definition von Distanzen (via Simulationen) und ihrer logischen Charakterisierung (via Modallogik), indem sie zeigt, dass die logische Distanz exakt der Verhaltensdistanz entspricht und dass diese Distanz effizient durch Formeln nachgewiesen werden kann.
Neue Erkenntnisse: Viele der spezifischen Ergebnisse für Markov-Ketten, fuzzy Systeme und metrische Systeme sind neu, insbesondere im Hinblick auf die Komplexität der Formelgenerierung.

Zusammenfassend liefert das Paper ein robustes Werkzeug für die quantitative Verifikation und den Vergleich von Systemen, das sowohl theoretisch fundiert als auch algorithmisch effizient ist.