Branch-Well-Structured Transition Systems and Extensions
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929449953394688 |
|---|---|
| author | Bollig, Benedikt Finkel, Alain Suresh, Amrita |
| author_facet | Bollig, Benedikt Finkel, Alain Suresh, Amrita |
| contents | We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2211_15913 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Branch-Well-Structured Transition Systems and Extensions Bollig, Benedikt Finkel, Alain Suresh, Amrita Logic in Computer Science We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem. |
| title | Branch-Well-Structured Transition Systems and Extensions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2211.15913 |