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.