Counting and Sampling Traces in Regular Languages

TL;DR

This paper develops algorithms for approximately counting and sampling Mazurkiewicz traces in regular languages, which are useful for model checking and testing concurrent programs, despite the counting problem being computationally hard.

Contribution

It introduces a fully polynomial randomized approximation scheme and an almost uniform sampler for Mazurkiewicz traces, advancing computational methods in concurrency analysis.

Findings

Counting Mazurkiewicz traces is #P-hard for deterministic automata.

The counting problem is in #P for NFAs and DFAs.

The paper provides an FPRAS and an FPAUS for trace counting and sampling.

Abstract

In this work, we study the problems of counting and sampling Mazurkiewicz traces that a regular language touches. Fix an alphabet $\Sigma$ and an independence relation $\mathbb{I} \subseteq \Sigma \times \Sigma$. The input consists of a regular language $L \subseteq \Sigma^*$, given by a finite automaton with $m$ states, and a natural number $n$ (in unary). For the counting problem, the goal is to compute the number of Mazurkiewicz traces (induced by $\mathbb{I}$) that intersect the $n^\text{th}$ slice $L_n = L \cap \Sigma^n$, i.e., traces that admit at least one linearization in $L_n$. For the sampling problem, the goal is to output a trace drawn from a distribution that is approximately uniform over all such traces. These tasks are motivated by bounded model checking with partial-order reduction, where an \emph{a priori} estimate of the reduced state space is valuable, and by testing methods for concurrent programs that use partial-order-aware random exploration. We first show that the counting problem is #P-hard even when $L$ is accepted by a deterministic automaton, in sharp contrast to counting words of a DFA, which is polynomial-time solvable. We then prove that the problem lies in #P for both NFAs and DFAs, irrespective of whether $L$ is trace-closed. Our main algorithmic contributions are a \emph{fully polynomial-time randomized approximation scheme} (FPRAS) that, with high probability, approximates the desired count within a prescribed accuracy, and a \emph{fully polynomial-time almost uniform sampler} (FPAUS) that generates traces whose distribution is provably close to uniform.