We consider the parametric reachability problem ( \(\textsf{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 \(\textsf{PRP}\) problem for VR grammars can be effectively reduced to the \(\textsf{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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars

  • Radu Iosif,
  • Arnaud Sangnier,
  • Neven Villani

摘要

We consider the parametric reachability problem ( \(\textsf{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 \(\textsf{PRP}\) problem for VR grammars can be effectively reduced to the \(\textsf{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.