Compositional Abstraction for Timed Systems with Broadcast Synchronization
Hanyue Chen, Miaomiao Zhang, Frits Vaandrager
TL;DR
This work tackles state-space explosion in model checking timed systems by introducing a simulation-based compositional abstraction framework capable of handling broadcast synchronization, binary synchronization, shared variables, and committed locations, while remaining UPPAAL-compatible. It defines timed transition systems with broadcast actions (TTSB) and develops a commutative, associative parallel composition, along with a restriction operator, enabling robust compositional semantics for NTAs. The authors prove the equivalence between non-compositional UPPAAL-like semantics and the proposed compositional semantics, and establish a timed step simulation preorder that is a precongruence for parallel composition, ensuring safe abstractions. They apply the framework to producer-consumer and clock synchronization case studies, showing substantial verification efficiency gains over monolithic methods. The results offer a principled path to scalable, modular verification of complex timed distributed systems featuring broadcast communications, with potential extensions to urgent channels and automatic abstraction refinement in future work.
Abstract
Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for modeling non-blocking one-to-many communication in multi-component systems. Consequently, they also lack a parallel composition operator that simultaneously supports broadcast synchronization, binary synchronization, shared variables, and committed locations. To address this, we propose a simulation-based compositional abstraction framework for timed systems, which supports these modeling concepts and is compatible with the popular UPPAAL model checker. Our framework is general, with the only additional restriction being that the timed automata are prohibited from updating shared variables when receiving broadcast signals. Through two case studies, our framework demonstrates superior verification efficiency compared to traditional monolithic methods.