Prover-Adversary games for systems over (non-deterministic) branching programs

TL;DR

This paper introduces Prover-Adversary games to characterize proof systems over deterministic and non-deterministic branching programs, establishing polynomial equivalences and extending the Immerman-Szelepcsenyi theorem.

Contribution

It formalizes new game-based characterizations of proof systems over branching programs and extends key complexity theorems to non-uniform settings.

Findings

Proves polynomial equivalence between proof systems and new games.

Formalizes a non-uniform version of the Immerman-Szelepcsenyi theorem.

Shows eLNDT is equivalent to systems over boundedly alternating branching programs.

Abstract

We introduce Pudlak-Buss style Prover-Adversary games to characterise proof systems reasoning over deterministic branching programs (BPs) and non-deterministic branching programs (NBPs). Our starting points are the proof systems eLDT and eLNDT, for BPs and NBPs respectively, previously introduced by Buss, Das and Knop. We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsenyi theorem that coNL = NL. Thanks to the techniques developed, we further obtain a proof complexity theoretic version of Immerman-Szelepcsenyi, showing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.