Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909598939611136 |
|---|---|
| author | Iosif, Radu Sangnier, Arnaud Villani, Neven |
| author_facet | Iosif, Radu Sangnier, Arnaud Villani, Neven |
| contents | We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars at the cost of introducing extra edges for routing messages. This transformation is motivated by the existence of several parametric verification techniques for families of networks specified by HR grammars, or similar inductive formalisms. Our reduction enables applying the verification techniques for HR systems to systems with dense architectures, such as user-specified cliques and multi-partite graphs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_01269 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars Iosif, Radu Sangnier, Arnaud Villani, Neven Formal Languages and Automata Theory We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars at the cost of introducing extra edges for routing messages. This transformation is motivated by the existence of several parametric verification techniques for families of networks specified by HR grammars, or similar inductive formalisms. Our reduction enables applying the verification techniques for HR systems to systems with dense architectures, such as user-specified cliques and multi-partite graphs. |
| title | Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2505.01269 |