Trimmed abstract: “…To this end, we analyze the feasibility of algorithms in model checking and start with the algorithms related to LTL model checking. We handle the state space generation, counterexample generation and the on-the-fly strong connected components (SCC) detection process, to build approaches which optimize the original algorithm via parallelization in different platforms. Then we work on the problem related to probabilistic model checking – the computation of the reachability probabilities, which is also an important subroutine for determining approximately optimal policies of the typical probabilistic model – Markov decision processes (MDPs). We present a GPU-accelerated value iteration to compute the reachability probabilities of MDPs. Our parallelization of the algorithms achieves expected performance improvement.”

…it is promising to extend our research from algorithm level to the application level. Our work has contains the extension of the existing PAT model checker with the concurrent LTL model checking algorithm. We aim at developing a new application which can both cover the model checking techniques, and contribute to the latest realistic problems which has not been covered by the applications mentioned above. To this end, quantum communication attracts our attention and is suitable to be the application domain. To the best of our knowledge, there is no tool support for the formal verification of quantum communication systems, including both the general model checking and the automatic quantum bisimilarity checking. Thus, we design and implement a tool-Qubet1.0, a model checking, bisimulation checking and emulation tool for quantum communication systems. Based on this essential tool, our algorithms-level parallelization is integrated with promising results.”