Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2411.17250 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929718186475520 |
|---|---|
| author | Blondin, Michael Cadilhac, Michaël Cui, Xin-Yi Czerner, Philipp Esparza, Javier Schulz, Jakob |
| author_facet | Blondin, Michael Cadilhac, Michaël Cui, Xin-Yi Czerner, Philipp Esparza, Javier Schulz, Jakob |
| contents | Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_17250 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Weakly acyclic diagrams: A data structure for infinite-state symbolic verification Blondin, Michael Cadilhac, Michaël Cui, Xin-Yi Czerner, Philipp Esparza, Javier Schulz, Jakob Logic in Computer Science Data Structures and Algorithms F.4.3; E.1 Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems. |
| title | Weakly acyclic diagrams: A data structure for infinite-state symbolic verification |
| topic | Logic in Computer Science Data Structures and Algorithms F.4.3; E.1 |
| url | https://arxiv.org/abs/2411.17250 |