Alexander Tepaev successfully defended his Master’s thesis (supervised by me and prof. Ezio Bartocci): “Comparative evaluation of TLA+ and R-CHECK specifications”

Full text of the thesis here.

Abstract:

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.