Algorithms for Model Checking of Random Transition Systems

We present our recent work in the intersection of two significant fields in graph theory: random graphs and model checking. We randomly generate a Kripke structure $\mathbb{K} {n, {p}} $ on $n$ states based on a tuple of probabilities $\boldsymbol{p}$ and investigate the probability that $\mathbb{K} {n, \boldsymbol{p}} \models \varphi$ as $n$ tends to infinity for any LTL or CTL formula $\varphi$. We show several important results: For an LTL or a CTL formula $\varphi$, $\lim_{n \rightarrow \infty} {\bf P}(\mathbb{K}_{n, \boldsymbol{p}} \models \varphi)$ is either $0$ or $1$, known as a 0-1 law. For an LTL formula $\varphi$, the asymptotic probability of $\mathbb{K}_{n, \boldsymbol{p}} \models \varphi$ is $1$ if and only if $\varphi$ is a tautology. The corresponding decision problem is PSPACE-complete. We establish a polynomial-time algorithm to decide whether $\lim_{n \rightarrow \infty} {\bf P}(\mathbb{K}_{n, \boldsymbol{p}} \models \varphi)$ is $0$ or $1$ for any CTL formula $\varphi$. Result 1 for CTL can be directly derived from a corresponding statement for FO(IFP) [1, Corollary 3. 2]. Notably, the algorithm presented in [1, Corollary 4. 2] operates in exponential time. In contrast, our Result 3 offers a substantial improvement over this by providing a more efficient solution. Here are the practical implications of our work. One way to test a newly developed model checker is to feed it some randomly generated Kripke structures. These results suggest that using random structures as inputs for a model checker may not be necessary as almost all inputs yield identical outcomes. Consequently, employing random models to evaluate a newly developed model checker proves to be of limited utility. [1] Andreas Blass, Yuri Gurevich, and Dexter Kozen. A zero-one law for logic with a fixed-point operator. Information and Control, 67(1–3): 70–90, October–December 1985.

Authors

• Yanni Dong

Keywords

No keywords are indexed for this paper.