Symbolic Model Checking in External Memory
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_ | 1866916740024238080 |
|---|---|
| author | Sølvsten, Steffan Christ van de Pol, Jaco |
| author_facet | Sølvsten, Steffan Christ van de Pol, Jaco |
| contents | We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47%. For larger instances, the computation time is mostly unaffected as it is dominated by the existential quantification.
Adiar's relational product is about one order of magnitude slower than conventional depth-first BDD implementations. Yet, its I/O-efficiency allows its running time to be virtually independent of the amount of internal memory. This allows it to compute on BDDs with much less internal memory and potentially to solve model checking tasks beyond the reach of conventional implementations.
Compared to the only other external memory BDD package, CAL, Adiar is several orders of magnitude faster when computing on larger instances. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_11229 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Symbolic Model Checking in External Memory Sølvsten, Steffan Christ van de Pol, Jaco Data Structures and Algorithms Logic in Computer Science 68W30 (primary) 68Q60, 68R07 (secondary) E.1; F.2.2; I.1.2 We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47%. For larger instances, the computation time is mostly unaffected as it is dominated by the existential quantification. Adiar's relational product is about one order of magnitude slower than conventional depth-first BDD implementations. Yet, its I/O-efficiency allows its running time to be virtually independent of the amount of internal memory. This allows it to compute on BDDs with much less internal memory and potentially to solve model checking tasks beyond the reach of conventional implementations. Compared to the only other external memory BDD package, CAL, Adiar is several orders of magnitude faster when computing on larger instances. |
| title | Symbolic Model Checking in External Memory |
| topic | Data Structures and Algorithms Logic in Computer Science 68W30 (primary) 68Q60, 68R07 (secondary) E.1; F.2.2; I.1.2 |
| url | https://arxiv.org/abs/2505.11229 |