Counting Abstraction for the Verification of Structured Parameterized Networks
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_ | 1866909503605178368 |
|---|---|
| author | Bozga, Marius Iosif, Radu Sangnier, Arnaud Villani, Neven |
| author_facet | Bozga, Marius Iosif, Radu Sangnier, Arnaud Villani, Neven |
| contents | We consider the verification of parameterized networks of replicated
processes whose architecture is described by hyperedge-replacement
graph grammars. Due to the undecidability of verification problems
such as reachability or coverability of a given configuration, in
which we count the number of replicas in each local state, we
develop two orthogonal verification techniques. We present a
counting abstraction able to produce, from a graph grammar
describing a parameterized system, a finite set of Petri nets that
over-approximate the behaviors of the original system. The counting
abstraction is implemented in a prototype tool, evalutated on a
non-trivial set of test cases. Moreover, we identify a decidable
fragment, for which the coverability problem is in 2EXPTIME
and PSPACE-hard. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_15391 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Counting Abstraction for the Verification of Structured Parameterized Networks Bozga, Marius Iosif, Radu Sangnier, Arnaud Villani, Neven Formal Languages and Automata Theory We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars. Due to the undecidability of verification problems such as reachability or coverability of a given configuration, in which we count the number of replicas in each local state, we develop two orthogonal verification techniques. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evalutated on a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in 2EXPTIME and PSPACE-hard. |
| title | Counting Abstraction for the Verification of Structured Parameterized Networks |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2502.15391 |