POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Fri 16 Jan 2026 16:10 - 16:35 at Nef - Automata 2 Chair(s): Umang Mathur

In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet $\Sigma$ and an independence relation $\mathbb{I} \subseteq \Sigma \times \Sigma$. The computational problems we address take as input a regular language $L$ over $\Sigma$, presented as a finite automaton with $m$ states, together with a natural number $n$ (presented in unary). For the counting problem, the output is the number of Mazurkiewicz \emph{traces} (induced by $\mathbb{I}$) that intersect the $n^\text{th}$ slice $L_n = L \cap \Sigma^n$ of $L$, i.e., traces that have at least one linearization in $L_n$. 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 \emph{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 $L$ 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 $L$ is trace-closed. Finally, our main contributions are a \emph{fully polynomial-time randomized approximation scheme} (FPRAS) that, with high probability, estimates the desired count within a specified accuracy parameter, and a \emph{fully polynomial-time almost uniform sampler} (FPAUS) that generates traces while ensuring that the distribution induced on them is approximately uniform with high probability.

Fri 16 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:10 - 17:25
Automata 2POPL at Nef
Chair(s): Umang Mathur National University of Singapore
16:10
25m
Talk
Counting and Sampling Traces in Regular Languages
POPL
Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore
DOI Pre-print
16:35
25m
Talk
Parametrised Verification of Intel-x86 Programs
POPL
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences
DOI
17:00
25m
Talk
General Decidability Results for Systems with Continuous Counters
POPL
A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
DOI