Towards realistic large random models of labeled transition systems and their 0-1 laws
For the model checking community, this work provides a theoretical foundation for understanding typical LTS behavior, which can inform the development of heuristics for scalable verification.
The paper introduces a probabilistic model of large labeled transition systems (LTSs) based on random graph theory, calibrated with empirical data from the Model Checking Contest. It proves that under LTL and CTL, the model exhibits either a convergence law or a 0-1 law as the system size grows to infinity, and provides algorithms for determining the limits.
Model checking is the automated verification of properties (specified in some modal logic) in labeled transition systems (LTSs); it is an essential tool in ensuring software systems function as intended. State spaces of software grow exponentially, and heuristics are needed to ensure model checking remains feasible in real-world applications. Heuristics, in turn, require a good understanding on the typical behaviour of LTSs. In this paper, we use random graph theory to create a probabilistic model of large LTSs. From a theoretical analysis of the creation of large LTSs, backed by empirical data from the Model Checking Contest, we endow these models with realistic parameter values. Then, we analyze the asymptotic behaviour of this model under LTL and CTL, two modal logics popular in model checking. We show that, depending on the precise model, as the size grows to infinity we either have a convergence law (for every formula, the probability that it holds converges to a limit) or a 0-1 law (...and this limit is 0 or 1). We also discuss the theoretical complexity of determining these limits, and give algorithms for doing so. These results are the starting point towards a deep theoretical understanding of typical LTS behaviour, and highlight the promising applicability of random graph theory to model checking. \keywords{Model checking \and Random graphs \and 0-1 laws