This Small Grant for Exploratory Research (SGER) award is to explore foundational research to study logical, timing, and probabilistic properties of a discrete state model, which is quite challenging because it is a strictly symbolic approach that combines algorithms from diverse areas, ranging from logical verification to numerical analysis and statistics. The work could lead to radically new approaches for modeling and analyzing today?s increasingly complex computer-based systems, with broader impacts from efficient techniques for achieving higher software reliability.