Counting and Sampling Traces in Regular Languages

In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet Σ and an independence relation I ⊆ Σ × Σ. The computational problems we address take as input a regular language 𝐿 over Σ, presented as a finite automaton with 𝑚 states, together with a natural number 𝑛 (presented in unary). For the counting problem, the output is the number of Mazurkiewicz traces (induced by I) that intersect the 𝑛 th slice 𝐿 𝑛 = 𝐿 ∩ Σ 𝑛 of 𝐿, i.e., traces that have at least one linearization in 𝐿 𝑛 . For the sampling problem, the output is a trace drawn from a distribution that is approximately uniform over all such traces. These problems are motivated by applications such as bounded model checking based on partial-order reduction, where an a priori estimate of the size of the state space can significantly improve usability, as well as testing approaches for concurrent programs that use partial-order-aware random sampling, where uniform exploration is desirable for effective bug detection.

We first show that the counting problem is #P-hard even when the automaton accepting the language 𝐿 is deterministic, which is in sharp contrast to the corresponding problem for counting the words of a DFA, which is solvable in polynomial time. We then show that the counting problem remains in the class #P for both NFAs and DFAs, independent of whether 𝐿 is trace-closed. Finally, our main contributions are a fully polynomial-time randomized approximation scheme (FPRAS) that, with high probability, estimates the desired count within a specified accuracy parameter, and a fully polynomial-time almost uniform sampler (FPAUS) that generates traces while ensuring that the distribution induced on them is approximately uniform with high probability. CCS Concepts: • Theory of computation → Regular languages; Concurrency; • Mathematics of computing → Probabilistic algorithms; • Software and its engineering → Software verification and validation.