Technische Zusammenfassung: Erweiterung von QuAK durch verschachtelte quantitative Automaten

Problemstellung

Quantitative Automaten (QAs) erweitern endliche $\omega$-Automaten um gewichtete Übergänge, um quantitative Systemeigenschaften wie durchschnittliche Auslastung oder Spitzen-Speichernutzung zu spezifizieren. Standard-QAs sind jedoch durch endliche Gewichtsmengen begrenzt, was sie daran hindert, Eigenschaften auszudrücken, die unbeschränkte Werte erfordern, wie etwa die durchschnittliche Antwortzeit. In solchen Szenarien kann die Verzögerung zwischen einer Anfrage und einer Zusage beliebig groß sein, eine Einschränkung, die durch endliche Übergangsgewichte nicht erfasst werden kann.

Während verschachtelte quantitative Automaten (NQAs) theoretisch eingeführt wurden, um dieses Problem zu lösen, indem ein übergeordneter Automat kindliche Automaten erzeugt, die unbeschränkte Werte über endliche Infixe berechnen, fehlten NQAs historisch praktische Werkzeugunterstützung. Bestehende Entscheidungsverfahren für NQAs blieben theoretisch, wodurch eine Lücke zwischen Entscheidbarkeitsresultaten und automatisierter Verifikation entstand.

Methodik

Die Autoren schließen diese Lücke, indem sie QuAK (Quantitative Automata Kit), ein Softwarewerkzeug zur QA-Analyse, um die Unterstützung für NQAs erweitern. Die Kernmethodik stützt sich auf Flattening-Verfahren, die NQA-Instanzen auf Standard-QA-Instanzen reduzieren. Diese Reduktion bewahrt die Antworten auf Schwellenwert-Entscheidungsprobleme (Leerheit und Universalität), ohne notwendigerweise semantische Äquivalenz zwischen der Eingabe-NQA und der Ausgabe-QA zu erhalten.

Die in C++ implementierte Flattening-Pipeline verarbeitet folgende algorithmische Strategien basierend auf der Kombination von übergeordneten Aggregatoren ($f$) und kindlichen Aggregatoren ($g$):

1. Reguläre Kinder ($g \in \{Min, Max, SumB\}$): Da die Menge der möglichen Rückgabewerte endlich ist, errät das Werkzeug den Rückgabewert des Kindes und verifiziert ihn mittels eines obligationsbasierten Ansatzes. Dies beinhaltet die parallele Verfolgung möglicher Kinderkonfigurationen und das Beschneiden jener, die keinen Endzustand mit dem geratenen Wert erreichen können.
2. Schwellenwertbasierte Begrenzung ($f \in \{Sup, LimSup, Inf, LimInf\}, g \in \{Sum+, Sum-\}$): Für diese Fälle werden kindliche Rückgabewerte, die einen bestimmten Schwellenwert $\lambda$ überschreiten, abgeschnitten. Dies reduziert das Problem auf den beschränkten $SumB$-Fall und ermöglicht die Konstruktion regulärer Kinder.
3. Extremale Eltern mit monotonen Kindern: Für die Leerheitsprüfung mit extremalen Eltern ($Sup, LimSup, Inf, LimInf$) und monotonen Kindern vermeidet das Werkzeug die Berechnung exakter Rückgabewerte. Stattdessen reduziert es jeden Kindaufruf auf ein binäres Schwellenwertergebnis (kann das Kind einen Wert $\ge \lambda$ zurückgeben?). Dies ermöglicht spezialisierte „Raten-und-Verifizieren"-Verfahren, die nur den notwendigen Schwellenwertstatus verfolgen und den Zustandsraum im Vergleich zu allgemeinen Reduktionen erheblich reduzieren.
4. Limit-Durchschnitt mit unbeschränkten Kindern:
   • Für $(LimSupAvg, Sum+)$ prüft das Werkzeug zunächst, ob kindliche Rückgabewerte unbeschränkt wachsen können. Wenn ja, gilt Leerheit trivial; andernfalls wird auf den beschränkten $SumB$-Fall reduziert.
   • Für $(LimInfAvg, Sum-)$ und $(LimSupAvg, Sum-)$ verwendet das Werkzeug eine Synchronisationskonstruktion, bei der alle aktiven Kinder gleichzeitig fortschreiten und eine beschränkte Multimenge aktiver Kinderzustände verfolgen.
5. Eliminierung stiller Gewichte: Der Flattening-Prozess erzeugt QAs mit stillen Gewichten (Übergänge, die kein Kind aufrufen). Diese werden durch Ersetzen durch neutrale Gewichte (z. B. $-\infty$ für $Sup$) oder mittels Pfadkompressionskonstruktionen für Limit-Durchschnittsziele eliminiert.
6. Antikettenbasierte Universalität: Um Universalität zu entscheiden, führt das Werkzeug eine On-the-Fly-Suche nach Gegenbeispielwörtern durch und nutzt Antiketten, um den Explorationsraum zu beschneiden. Kontexte werden mit Wertzusammenfassungen angereichert, um quantitative Schranken neben der Erreichbarkeit zu behandeln.

Hauptbeiträge

1. Werkzeugimplementierung: Die erste praktische Implementierung von NQA-Analysealgorithmen, die das QuAK-Framework erweitert.
2. Umfassende Flattening-Suite: Implementierung von Flattening-Verfahren für alle Kombinationen von übergeordneten und kindlichen Aggregatoren, bei denen Leerheit und Universalität als entscheidbar bekannt sind. Dies umfasst übergeordnete Funktionen $\{Sup, Inf, LimSup, LimInf, LimSupAvg, LimInfAvg\}$ und kindliche Funktionen $\{Min, Max, SumB, Sum+, Sum-\}$.
3. Modulare Architektur: Eine Pipeline, die NQAs in QAs mit stillen Gewichten übersetzt, die anschließend von den bestehenden Entscheidungsverfahren von QuAK für Leerheit, Inklusion und Sicherheits-Lebendigkeits-Analyse verarbeitet werden.
4. Experimentelle Evaluation: Das Werkzeug wurde an zwei Benchmark-Familien evaluiert:
   • Antwortzeit: Parametrisierte NQAs ($A_{n,k}$), die Anfrage-Zusage-Protokolle mit begrenzten ausstehenden Anfragen ($n$) und Antwortzeiten ($k$) modellieren.
   • Ressourcenverbrauch: Parametrisierte NQAs ($B_{n,k}$), die Systeme mit dynamisch gestarteten/terminierten Prozessen und Ressourcenzugriffsmustern modellieren.

Ergebnisse

Die experimentelle Evaluation demonstriert die Wirksamkeit und Skalierbarkeit von QuAK über verschiedene NQA-Typen hinweg:

• Antwortzeit-Benchmarks:
  • Für die Leerheit von $(Sup, Sum+)$ skaliert das Werkzeug gut; die Laufzeit zeigt eine nahezu quadratische Abhängigkeit von der Antwortzeitgrenze $k$ und eine schwache Abhängigkeit von der Anzahl der ausstehenden Anfragen $n$.
  • Für die Leerheit von $(LimSupAvg, Sum+)$ und die Universalität von $(Sup, SumB)$ wächst die Laufzeit mit beiden Parametern schneller an. Universalität ist durchgehend teurer aufgrund der Notwendigkeit von PSpace-Verfahren zur Handhabung von Nichtdeterminismus im geflattenen Automaten.
• Ressourcenverbrauch-Benchmarks:
  • Die Leerheitsprüfung für $(Sup, Max)$ zeigt eine schnelle Explosion in beiden Parametern ($n$ und $k$) aufgrund der kombinatorischen Explosion der von aktiven Kindern verfolgten Ressourceteilmengen.
  • Der Fall $(LimSupAvg, Max)$ ist erheblich schwieriger, da er die Bewahrung exakter Rückgabewerte für alle aktiven Kinder erfordert, was zu einem Speicheraufbrauch bei kleineren Parameterwerten führt als im Supremum-Fall.

Die Ergebnisse bestätigen, dass, obwohl explizites Flattening große Zustandsräume verursachen kann – insbesondere wenn viele Kinderinstanzen gleichzeitig aktiv sind oder Kinderkonfigurationen dicht sind – das Werkzeug entscheidbare Instanzen komplexer quantitativer Eigenschaften erfolgreich handhabt.

Bedeutung

Die Arbeit beansprucht, die Lücke zwischen der theoretischen Entscheidbarkeit von NQAs und der praktischen Verifikation zu schließen. Durch die Erweiterung von QuAK ermöglichen die Autoren die automatisierte Verifikation quantitativer Eigenschaften, wie der durchschnittlichen Antwortzeit, die in NQAs ausdrückbar, aber in Standard-QAs nicht darstellbar sind. Die Arbeit legt eine Grundlage für die Analyse von Systemen mit dynamisch erzeugten Aufgaben und unbeschränkten Kosten und bietet einen praktischen Rahmen für die Protokoll-Latenzanalyse, die Überwachung von Service-Level-Antwortzeiten und die Ressourcenverbrauchsanalyse. Die Autoren weisen darauf hin, dass die aktuelle Implementierung auf einer expliziten Zustandskonstruktion basiert, zukünftige Arbeiten jedoch symbolische Darstellungen erforschen könnten, um die Zustandsraumbombardierung zu mildern.