Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915686855475200 |
|---|---|
| author | Taylor, Landon Jeppson, Joshua Irfan, Ahmed Buecherl, Lukas Myers, Chris Zhang, Zhen |
| author_facet | Taylor, Landon Jeppson, Joshua Irfan, Ahmed Buecherl, Lukas Myers, Chris Zhang, Zhen |
| contents | Highly-concurrent system models with vast state spaces like Chemical Reaction Networks (CRNs) that model biological and chemical systems pose a formidable challenge to cutting-edge formal analysis tools. Although many symbolic approaches have been presented, transient probability analysis of CRNs, modeled as Continuous-Time Markov Chains (CTMCs), requires explicit state representation. For that purpose, current cutting-edge methods use hash maps, which boast constant average time complexity and linear memory complexity. However, hash maps often suffer from severe memory limitations on models with immense state spaces. To address this, we propose using prefix trees to store states for large, highly concurrent models (particularly CRNs) for memory savings. We present theoretical analyses and benchmarks demonstrating the favorability of prefix trees over hash maps for very large state spaces. Additionally, we propose using a Bounded Model Checking (BMC) pre-processing step to impose a variable ordering to further improve memory usage along with preliminary evaluations suggesting its effectiveness. We remark that while our work is motivated primarily by the challenges posed by CRNs, it is generalizable to all CTMC models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_17892 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models Taylor, Landon Jeppson, Joshua Irfan, Ahmed Buecherl, Lukas Myers, Chris Zhang, Zhen Data Structures and Algorithms Formal Languages and Automata Theory Highly-concurrent system models with vast state spaces like Chemical Reaction Networks (CRNs) that model biological and chemical systems pose a formidable challenge to cutting-edge formal analysis tools. Although many symbolic approaches have been presented, transient probability analysis of CRNs, modeled as Continuous-Time Markov Chains (CTMCs), requires explicit state representation. For that purpose, current cutting-edge methods use hash maps, which boast constant average time complexity and linear memory complexity. However, hash maps often suffer from severe memory limitations on models with immense state spaces. To address this, we propose using prefix trees to store states for large, highly concurrent models (particularly CRNs) for memory savings. We present theoretical analyses and benchmarks demonstrating the favorability of prefix trees over hash maps for very large state spaces. Additionally, we propose using a Bounded Model Checking (BMC) pre-processing step to impose a variable ordering to further improve memory usage along with preliminary evaluations suggesting its effectiveness. We remark that while our work is motivated primarily by the challenges posed by CRNs, it is generalizable to all CTMC models. |
| title | Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models |
| topic | Data Structures and Algorithms Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2512.17892 |