{"id":"arxiv/2607.15029","url":"https://arxiv.org/abs/2607.15029","tags":["cs.LO","math.CO","math.PR"],"score":0,"title":"Towards realistic large random models of labeled transition systems and their 0-1 laws","domain":"cs.LO","source":"arxiv","authors":["Milan Lopuhaä-Zwakenberg"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-16","reactions":{}}