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.
