University of Twente Student Theses
As of Friday, 8 August 2025, the current Student Theses repository is no longer available for thesis uploads. A new Student Theses repository will be available starting Friday, 15 August 2025.
Convergence in Model Checking of Random Kripke Structures
Timofeev Fornasov, Denis (2025) Convergence in Model Checking of Random Kripke Structures.
|
PDF
2MB |
| Abstract: | Randomly generated Kripke structures (graphs with states, initial states and directed edges) are used in model checkers to evaluate benchmarks, this consists of checking the truth of a temporal logic formula, specifically for this research, a Computation Tree Logic (CTL) formula, for the given structure. It has been shown by previous research that, as these graphs grow in size (node/state count), the probability of truth of any given CTL formula converges to a fixed value. This paper focuses on a gap in the current research, which is determining how fast this convergence occurs. The paper demonstrates how the convergence happens very quickly, at graph sizes not exceeding a few hundred nodes even for very complex CTL formulae. This greatly impacts model checking because graph sizes of tens thousands of nodes are typically used. Since it has been shown how to calculate the convergence probabilities by previous research, and we now know that these probabilities are converged to very quickly, this phenomenon can be exploited by model checkers by probabilistically guessing whether a given formula holds for a model instead of actually verifying whether it does. The paper also shows that the convergence happens exponentially, and the pattern of how graph generation parameters (probability of edges occurring, probability of states being labeled as initial) also affect the rate of convergence. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/107456 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page