Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models

TL;DR

This paper introduces prefix trees as a memory-efficient alternative to hash maps for storing states in large-scale continuous-time stochastic models like CRNs, supported by theoretical analysis and benchmarks.

Contribution

It proposes using prefix trees for state storage in CTMCs, demonstrating memory savings and improved efficiency over hash maps, with additional pre-processing techniques for further optimization.

Findings

Prefix trees reduce memory usage in large CTMC models.

Benchmarks show prefix trees outperform hash maps in large state spaces.

Preliminary results indicate BMC pre-processing enhances memory efficiency.

Abstract

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.