SHF: Small: A Hierarchical Symbolic Framework to Verify Logic, Timing, and Probabilistic Properties of Computing Systems

开发了一个用于分析计算机系统的逻辑、时序和概率特性的符号框架，该框架使用用于存储和操作大型数据结构的决策图。决策图在验证方面非常有效，但在其他环境中还没有太多地挖掘它们的潜力。该框架包括马尔可夫模型的符号解，它基于有效的边值决策图类来表示速率矩阵，当精确的数值研究不可行时，使用欠逼近和过逼近来获得界，依赖于逻辑级别的状态聚集或部分探索，在数值级别计算概率界，以及在层次子模型之间交换数值。该框架还通过探索符号编码、层次组成和界限的限制和潜力，包括将传统离散事件模拟与符号算法相结合的混合技术，解决了事件计时的非马尔可夫设置、一般分布和不确定区间范围。研究成果将为研究人员和工程师提供研究比目前可能的更大和更一般的系统模型的逻辑、计时和概率属性的能力，从而对计算机科学和工程的多个领域产生积极影响。在这个项目中开发的软件包将是学生和实践者需要对计算机系统的逻辑和时序行为进行建模、验证或分析的极好的动手工具。

A symbolic framework for the analysis of logic, timing, and probabilistic properties of computer systems is developed, using decision diagrams for the storage and manipulation of large data structures. Decision diagrams have been enormously effective in verification, but their potential has not been explored much in other settings. The framework includes symbolic solutions for Markov models based on efficient classes of edge-valued decision diagrams to represent rate matrices, using under- and over-approximations to obtain bounds when an exact numerical study is infeasible, relying on aggregation or partial exploration of states at the logic level, computing probability bounds at the numerical level, and exchanging numerical values between hierarchical submodels. The framework also addresses non-Markov settings, general distributions, and nondeterministic interval ranges for the timing of events by exploring the limits and potentials of symbolic encodings, hierarchical composition, and bounds, including hybrid techniques that integrate traditional discrete-event simulation with symbolic algorithms.The research results will positively affect several areas of computer science and engineering, by providing researchers and engineers with the ability to study the logic, timing, and probabilistic properties of much larger and more general system models than currently possible. The software packages developed during this project will be an excellent hands-on tool for students and practitioners in need to model, verify, or analyze the logic and timing behavior of computer systems.