Towards realistic large random models of labeled transition systems and their 0-1 laws
Logic in Computer Science
Summary
The authors study how to better understand typical behaviors of labeled transition systems (LTSs), which are used in automated software verification called model checking. They create a probabilistic model of large LTSs using ideas from random graph theory and set realistic parameters based on data. Analyzing this model with popular logical languages (LTL and CTL), they find that as systems get very large, the chances that certain properties hold settle down to fixed probabilities or only 0 or 1. They also look at how hard it is to figure out these probabilities and provide algorithms to do so. This work helps build a theoretical foundation for making model checking more scalable and predictable.
Authors
Milan Lopuhaä-Zwakenberg
Abstract
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