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.

翻译：具有庞大状态空间的高度并发系统模型，例如模拟生物和化学系统的化学反应网络（CRNs），对前沿的形式化分析工具构成了严峻挑战。尽管已提出多种符号化方法，但对建模为连续时间马尔可夫链（CTMCs）的CRNs进行瞬态概率分析，仍需显式的状态表示。为此，当前的前沿方法使用哈希映射，其具有常数的平均时间复杂度和线性的内存复杂度。然而，对于具有巨大状态空间的模型，哈希映射常常受到严重的内存限制。为解决此问题，我们提出使用前缀树来存储大型、高度并发模型（尤其是CRNs）的状态，以节省内存。我们提供了理论分析和基准测试，证明对于极大的状态空间，前缀树优于哈希映射。此外，我们提出使用有界模型检验（BMC）预处理步骤来施加变量顺序，以进一步改善内存使用，并提供了初步评估表明其有效性。我们指出，虽然我们的工作主要受CRNs带来的挑战所驱动，但其可推广至所有CTMC模型。