Infinite State Model Checking by Learning Transitive Relations
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913083911307264 |
|---|---|
| author | Frohn, Florian Giesl, Jürgen |
| author_facet | Frohn, Florian Giesl, Jürgen |
| contents | We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_04761 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Infinite State Model Checking by Learning Transitive Relations Frohn, Florian Giesl, Jürgen Logic in Computer Science We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art. |
| title | Infinite State Model Checking by Learning Transitive Relations |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2502.04761 |