Bridging the Gap Between Logic and Probabilistic Model Checking

Fast development of hardware/software design requires more versatile and powerful verification methods to help engineers understand, verify, and debug their systems. The scope of system verification now is not limited to finding functional errors at the logic level, but also includes analyzing and predicting the bottlenecks in performance and dependability. Model checking, which was originally proposed to verify discrete-state systems, has been further extended to the verification of probabilistic systems. Many techniques from other communities, such as Markov chain analysis, are involved in the model checking process. Traditional and new verification techniques must be integrated into a platform that can handle both the logic and probabilistic aspects of a given model.Symbolic model checking using decision diagrams has achieved great success in verifying many practical software and hardware systems, and is still the primary approach to logic verification. Recent research shows that decision diagrams can be successfully employed in probabilistic model checking. This thesis is devoted to future improving the capability of decision diagram techniques in model checking. Specifically, this thesis explores the application of a family of decision diagrams, including multi-way decision diagrams and edge-valued multi-way decision diagrams, to several topics in both classic and probabilistic model checking.My thesis consists of two parts of work: In the first part, I extend the existing saturation algorithm, which was originally proposed for state-space generation, to CTL model checking, strongly-connected component enumeration, and shortest witness generation for various properties. The second part of the thesis focuses on probabilistic model checking using decision diagrams. I propose a new and more efficient algorithm to carry out the Gauss-Seidel iterative method, which is a key step in probabilistic model checking. This technique can be applied to both steady-state solution of continuous-time Markov chains and CSL model checking. Then, I introduce a new bounding semantics of CSL to tackle truncation errors in numerical analysis and correctly evaluate nested CSL formulas.The proposed techniques have been integrated into the SMART tool developed in our lab. Experimental results demonstrate that SMART is a promising platform to handle both logic and quantitative verification for many practical systems