0-1 Laws for LTL and CTL over Random Transition Systems

This paper examines how 0-1 and convergence laws affect model checking benchmarks, where a formula’s truth in a random model becomes nearly independent of the model or follows a specific probability. We investigate these behaviours for Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) in random Kripke structures defined based on Erdős-Rényi random models. For structures with multiple initial states, both LTL and CTL have a 0-1 law. The probability of satisfying an LTL formula converges to 1 or 0 as the model size grows, depending on whether the formula is a tautology or not. In contrast, structures with a single initial state exhibit a convergence law. We also establish that computing asymptotic probabilities for LTL is computationally hard (PSPACE-complete for multiple initial states and PSPACE-hard for one initial state), whereas efficient polynomial-time algorithms exist for CTL. These findings underscore a key limitation: random Kripke structures with multiple initial states are often ineffective as benchmarks because formulae tend to be almost always true or false, irrespective of the model. This renders them unsuitable for evaluating model checking algorithms. Structures with one initial state, however, demonstrate more varied and meaningful behaviour due to convergence laws, where probabilities depend on the model’s properties, making them more promising candidates for constructing reliable benchmarks to assess model checking tools.