arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2511.12011

A Logspace Constructive Proof of L=SL

Sam Buss·Anant Dhayal·Valentine Kabanets·Antonina Kolokolova·Sasank Mouli
View original source ↗Read source document ↗Export metadata ↓

Abstract

We formalize the proof of Reingold's Theorem that SL=L [Rei05] in the theory of bounded arithmetic VL, which corresponds to ``logspace reasoning''. As a consequence, we get that VL=VSL, where VSL is the theory of bounded arithmetic for ``symmetric-logspace reasoning''. This resolves in the affirmative an old open question from Kolokolova [Kol05] (see also Cook-Nguyen [NC10]). Our proof relies on the Rozenman-Vadhan alternative proof of Reingold's Theorem ([RV05]). To formalize this proof in VL, we need to avoid reasoning about eigenvalues and eigenvectors (common in both original proofs of SL=L). We achieve this by using some results from Buss-Kabanets-Kolokolova-Koucký [Bus+20] that allow VL to reason about graph expansion in combinatorial terms.

Explore related subjects

cs.LOmath.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Sam Buss, Anant Dhayal, Valentine Kabanets, Antonina Kolokolova, Sasank Mouli. 2025-11-15. A Logspace Constructive Proof of L=SL. https://arxiv.org/abs/2511.12011

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation First-order Logic

We introduce and study UCPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL) with converse (CPDL) and universal modality (UCPDL). In terms of expressive power, UCPDL+ strictly contains PDL extended with intersection and converse (a.k.a. ICPDL), as well as Conjunctive Queries (CQ), Conjunctive Regular Path Queries (CRPQ), or some known extensions thereof (Regular Queries and CQPDL). Further, it is equivalent to the extension of the unary-negation fragment of first-order logic (UNFO) with unary transitive closure, denoted by UNTC, which in turn strictly contains a previously studied extension of UNFO with regular expressions known as UNFO$^{reg}$. We investigate the expressive power, indistinguishability via bisimulations, satisfiability, and model checking for UCPDL+ and CPDL+. We argue that natural subclasses of CPDL+ can be defined in terms of the tree-width of the underlying graphs of the formulas. We show that the class of CPDL+ formulas of tree-width 2 is equivalent to ICPDL, and that it also coincides with CPDL+ formulas of tree-width 1. However, beyond tree-width 2, incrementing the tree-width strictly increases the expressive power. We characterize the expressive power for every class of fixed tree-width formulas in terms of a bisimulation game with pebbles. Based on this characterization, we show that CPDL+ has a tree-like model property. We prove that the satisfiability problem for UCPDL+ is decidable in 2ExpTime, coinciding with the complexity of ICPDL. As a consequence, the satisfiability problem for UNTC is shown to be 2ExpTime-complete as well. We also exhibit classes for which satisfiability is reduced to ExpTime.

cs.LO↗
arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗
arXiv2026

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

cs.LO↗