Compositional Abstraction for Timed Systems with Broadcast Synchronization
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918024140816384 |
|---|---|
| author | Chen, Hanyue Zhang, Miaomiao Vaandrager, Frits |
| author_facet | Chen, Hanyue Zhang, Miaomiao Vaandrager, Frits |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_12436 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Compositional Abstraction for Timed Systems with Broadcast Synchronization Chen, Hanyue Zhang, Miaomiao Vaandrager, Frits Formal Languages and Automata Theory 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. |
| title | Compositional Abstraction for Timed Systems with Broadcast Synchronization |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2505.12436 |