Comparative evaluation of TLA+ and R-CHECK specifications

Abstract

Diese Arbeit präsentiert eine vergleichende Evaluierung zweier formaler Modellierungsframeworks - TLA+ und R-CHECK - mit besonderem Fokus auf kommunikationszentrierte und rekonfigurierbare Multi-Agenten-Systeme. Der Vergleich erfolgt in zwei Richtungen. Erstens untersuchen wir aktuelle TLA+-Fallstudien sowie öffentlich verfügbare Beispiele, um die Verfügbarkeit kommunikationszentrierter MAS zu bewerten, und übertragen mehrere repräsentative TLA+-Modelle nach R-CHECK, um die Ausdrucksstärke von R-CHECK zu evaluieren und die wesentlichen Modellierungsentscheidungen, den erforderlichen Aufwand sowie die semantischen Verschiebungen zu dokumentieren, die bei der Übersetzung auftreten. Zweitens rekonstruieren wir ausgewählte R-CHECK-Funktionalitäten in TLA+, um den zusätzlichen Modellierungsaufwand auf Seiten von TLA+ zu bewerten.Die Ergebnisse zeigen, dass beide Frameworks hinreichend ausdrucksstark sind, um die untersuchten Systeme zu modellieren, dass sie sich jedoch deutlich im Modellierungsstil unterscheiden. TLA+ folgt einer Globalzustandsperspektive auf das System, während R-CHECK den Zustand innerhalb der Agenten kapselt und native Unterstützung für die Modellierung von Kommunikation und dynamischer Konnektivität bietet. Dadurch ermöglicht R-CHECK einen direkteren Modellierungsstil für kommunikationszentrierte und rekonfigurierbare Multi-Agenten-Systeme, während TLA+ in der Regel eine explizitere Kodierung von Konzepten auf der Interaktionsebene erfordert.

This thesis presents a comparative evaluation of two formal modeling frameworks -TLA+ and R-CHECK - with a focus on communication-centric and reconfigurable multi-agent systems. The comparison is performed in two directions. First, we survey recent TLA+ case studies and publicly available examples to assess the availability of communication-centric MAS, and we port several representative TLA+ models to R-CHECK to evaluate the expressiveness of R-CHECK and to document the main modeling decisions, required effort, and semantic shifts that arise during translation. Second, we reconstruct selected R-CHECK features in TLA+ to evaluate the additional modeling machinery required on the TLA+ side.The results show that both frameworks are expressive enough to model the studied systems, but that they differ significantly in modeling style. TLA+ follows a global-state view of the system, whereas R-CHECK encapsulates state inside agents and provides native support for expressing communication and dynamic connectivity. As a result, R-CHECK offers a more direct modeling style for communication-centric and reconfigurable multi-agent systems, while TLA+ typically requires more explicit encoding of interaction-level concepts.