Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2306.01466 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917388068323328 |
|---|---|
| author | Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le |
| author_facet | Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le |
| contents | We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems.
Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_01466 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | On the Complexity of Proving Polyhedral Reductions Amat, Nicolas Zilio, Silvano Dal Botlan, Didier Le Logic in Computer Science We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples. |
| title | On the Complexity of Proving Polyhedral Reductions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.01466 |