Search

We show that feasibility of the tth level of the Lasserre semidefinite programming hierarchy for graph isomorphism can be expressed as a homomorphism indistinguishability relation. In other words, we define a class Lt of graphs such that graphs G and H are not distinguished by the tth level of the Lasserre hierarchy if and only if they admit the same number of homomorphisms from any graph in Lt. By analysing the treewidth of graphs in Lt we prove that the 3tth level of Sherali–Adams linear programming hierarchy is as strong as the tth level of Lasserre. Moreover, we show that this is best possible in the sense that 3t cannot be lowered to 3t − 1 for any t. The same result holds for the Lasserre hierarchy with non-negativity constraints, which we similarly characterise in terms of homomorphism indistinguishability over a family L+t of graphs. Additionally, we give characterisations of level-t Lasserre with non-negativity constraints in terms of logical equivalence and via a graph colouring algorithm akin to the Weisfeiler–Leman algorithm. This provides a polynomial time algorithm for determining if two given graphs are distinguished by the tth level of the Lasserre hierarchy with non-negativity constraints.

LIPIcs, Volume 261, ICALP 2023, Complete Volume

Front Matter, Table of Contents, Preface, Conference Organization

Finite and algorithmic model theory (FAMT) studies the expressive power of logical languages on finite structures or, more generally, structures that can be finitely presented. These are the structures that serve as input to computation, and for this reason the study of FAMT is intimately connected with computer science. Over the last four decades, the subject has developed through a close interaction between theoretical computer science and related areas of mathematics, including logic and combinatorics. This report documents the program and the outcomes of Dagstuhl Seminar 22051 "Finite and Algorithmic Model Theory".

We give polynomial time algorithms for deciding almost-sure and limit-sure reachability in Branching Concurrent Stochastic Games (BCSGs). These are a class of infinite-state imperfect-information stochastic games that generalize both finite-state concurrent stochastic reachability games ([L. de Alfaro et al., 2007]) and branching simple stochastic reachability games ([K. Etessami et al., 2018]).

In recent years, a considerable amount of research has been devoted to understanding the computational complexity of basic analysis problems, and model checking problems, for finitely-presented countable infinite-state probabilistic systems. In particular, we have studied recursive Markov chains (RMCs), recursive Markov decision processes (RMDPs) and recursive stochastic games (RSGs). These arise by adding a natural recursion feature to finite-state Markov chains, MDPs, and stochastic games. RMCs and RMDPs provide natural abstract models of probabilistic procedural programs with recursion, and they are expressively equivalent to probabilistic and MDP extensions of pushdown automata. Moreover, a number of well-studied stochastic processes, including multi-type branching processes, (discrete-time) quasi-birth-death processes, and stochastic context-free grammars, can be suitably captured by subclasses of RMCs. A central computational problem for analyzing various classes of recursive probabilistic systems is the computation of their (optimal) termination probabilities. These form a key ingredient for many other analyses, including model checking. For RMCs, and for important subclasses of RMDPs and RSGs, computing their termination values is equivalent to computing the least fixed point (LFP) solution of a corresponding monotone system of polynomial (min/max) equations. The complexity of computing the LFP solution for such equation systems is a intriguing problem, with connections to several areas of research. The LFP solution may in general be irrational. So, one possible aim is to compute it to within a desired additive error epsilon > 0. For general RMCs, approximating their termination probability within any non-trivial constant additive error < 1/2, is at least as hard as long-standing open problems in the complexity of numerical computation which are not even known to be in NP. For several key subclasses of RMCs and RMDPs, computing their termination values turns

We study the computational complexity of basic decision problems for one-counter simple stochastic games (OC-SSGs), under various objectives. OC-SSGs are 2-player turn-based stochastic games played on the transition graph of classic one-counter automata. We study primarily the termination objective, where the goal of one player is to maximize the probability of reaching counter value 0, while the other player wishes to avoid this. Partly motivated by the goal of understanding termination objectives, we also study certain ``limit'' and ``long run average'' reward objectives that are closely related to some well-studied objectives for stochastic games with rewards. Examples of problems we address include: does player 1 have a strategy to ensure that the counter eventually hits 0, i.e., terminates, almost surely, regardless of what player 2 does? Or that the $liminf$ (or $limsup$) counter value equals $infty$ with a desired probability? Or that the long run average reward is $>0$ with desired probability? We show that the qualitative termination problem for OC-SSGs is in $NP$ intersect $coNP$, and is in P-time for 1-player OC-SSGs, or equivalently for one-counter Markov Decision Processes (OC-MDPs). Moreover, we show that quantitative limit problems for OC-SSGs are in $NP$ intersect $coNP$, and are in P-time for 1-player OC-MDPs. Both qualitative limit problems and qualitative termination problems for OC-SSGs are already at least as hard as Condon's quantitative decision problem for finite-state SSGs.