2026-07-22T03:53:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23972 2025-11-12T13:25:10Z ddc:004 open_access

Partial-Order Reduction Is Hard Herbreteau, Frédéric Larroze-Jardiné, Sarah Walukiewicz, Igor Formal verification Concurrent systems Partial-order reduction Complexity The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Frédéric Herbreteau and Sarah Larroze-Jardiné and Igor Walukiewicz 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.22 urn:nbn:de:0030-drops-239727 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22 eng https://creativecommons.org/licenses/by/4.0/legalcode