Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2401.03711 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929202334269440 |
|---|---|
| author | Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le |
| author_facet | Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le |
| contents | We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_03711 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le Logic in Computer Science We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions. |
| title | Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.03711 |