The Long Reach of Reachability
Workshop on Infinite State Systems at the Bellairs Institute on Barbados
|
|
Cropped from source |
Joel Ouaknine is a Professor of Computer Science at Oxford University and a Fellow of St. John’s College there. He was previously a doctoral student at Oxford and made a critical contribution in 1998 of a kind I enjoyed as a student in the 1980s. This was contributing a win in the annual Oxford-Cambridge Varsity Chess Match, which in 1998 was won by Oxford, 5-3.
Today I’d like to report on some of the wonderful things that happened at a workshop on “Infinite-State Systems” hosted by Joel at the Bellairs Institute of McGill University last March 13–20 in Barbados, before we finally opened a chess set and played two games on the last evening.
The workshop was one of two happening concurrently at Bellairs, which has been my pleasure to visit twice before in 1995 and 2009. The other was on “Co-Algebras in Quantum Physics” and was co-organized by Prakash Panangaden, whom I used to know on Cornell’s faculty when I was a postdoc there. I often wished I could be in a quantum superposition between the workshops. My own talk for Joel’s workshop was on analyzing quantum circuits, and that anchored stimulating discussions I had with both workshops’ members during meals and excursions and other free time.
The other participants in ours were Dmitry Chistikov, Thomas Colcombet, Amelie Gheerbrant, Stefan Göller, Martin Grohe, Radu Iosif, Marcin Jurdzinski, Stefan Kiefer, Stephan Kreutzer, Ranko Lazic, Jerome Leroux, Richard Mayr, Peter Bro Miltersen, Nicole Schweikardt, and James Worrell. Göller and Grohe joined Joel and me for soccer in a nearby park on two lunch breaks—we didn’t just play chess.
Reachability
The basic reachability problem is: Given a graph , a starting node
, and a set
of target nodes, is there a path from
to some node in
? When
is undirected the problem is solvable in logarithmic space. This is a deep result—for a long time randomized logspace was known—but a simple statement. When
is directed the problem is complete for nondeterministic log space (
). But
is in
so it’s still solvable in polynomial time.
Enough said about reachability? The meta-problem—really the problem—comes from other ways to present besides listing finitely many nodes and edges. If
is presented by a circuit
with
inputs that recognizes its edge relation on
, then reachability for
jumps up to being
-complete. Not all graphs
have
of poly size, but those that do include the transition graphs for polynomial space-bounded Turing machines with start state
and accepting configurations
.
As the workshop’s name implies, we can consider “machines” that give rise to infinitely many states, and then things really get interesting. We just blogged about such a machine and its halting problem. Described in another way, the “machine” is a matrix
which takes a vector
to
where
The target states in are those with last component
. Are any of them reached in the sequence
? This is a deterministic and discrete and simple linear system, yet nobody knows how to decide it. Allowing more general integer matrices
does not change the nature of the problem, and equivalent forms include whether the lower-left (or upper-right) entry of
ever becomes zero.
So the complexity range of reachability runs from easy to (maybe-) undecidable. There are further questions one can ask after allowing to consider computations that are actually infinite: Are some states in reached infinitely often? Does the system stay always within
upon entry? When there is branching one can put probabilities on the transitions and ask questions about probabilities of reaching
being nonzero or
or
and so on. In a sense my own talk was about those questions when the transitions have amplitudes instead of probabilities. One can also associate infinitely many states to a finite graph by having one or more “budget counters” and giving each edge a label for how much it increments or debits a given counter when traversed. Finally one can partition the nodes among adversarial players who can vie to reach certain nodes and/or bankrupt some counters.
Overall the workshop impressed me with the wide range of interesting problems in this thread and the variety of their application areas. I’ll mention a few of the 16 talks now and intend more later. Here is a photo of our participants:
Some Talks
Nicole Schweikardt led off with the words,
“As a warmup to infinite State Systems, everything in my talk will be finite.”
She actually led off with a great introductory problem to her 2014 paper with Kreutzer: Define the -number of a graph
to be the number of ways of choosing three edges that don’t have any edges between them. Equivalently, their edge-neighborhoods are disjoint; they are an independent set in the edge graph of
; the subgraph induced by their six vertices is the graph of three disjoint edges. Now for any
consider:
-
the cycle on
nodes;
-
the graph of two disjoint
-cycles.
Do they have the same -number? I felt knowledgeable about these graphs since Dick and I were interested long ago in the problem of distinguishing these graphs via constant-depth circuits with various fancy gates. So I put some confidence in my reaction, “of course not.” But the answer is yes when
.
The reason “why ?” can be explained in a hand-waving manner by saying that if you number the edges in one half of
and choose edges
and
, you can equally well choose
or
for a third edge in that component. One choice “attaches to” the end with
, the other to
, so the choices have the same degrees of freedom as in the bigger cycle
. Well that is far from a proof, and what was beautiful in the rest of the talk and the paper is the connection between Hanf equivalence and logic that makes this rigorous. This leads to an open problem about extending the equivalence for order-invariant logics, which relates to what we covered two posts ago.
Richard Mayr led off the third talk by saying his contents were
“…partly known, partly nice observations, and partly half-baked.”
We raised a cheer recently for observations. Mayr began with a setup like Christos Papadimitriou’s games against Nature: a finite graph with some node choices controlled by the Player and the others random and one budget counter. His first example was the following graph:
The player begins at node with a balance of
but can raise it as much as desired by choosing the edge with
. To reach the goal
, however, the player must eventually go to the random node
. This carries some risk of the
loop being taken more times than the
arc was chosen at
, thus bankrupting the player. But the risk can be made arbitrarily small. The key distinction is between the properties:
-
There exists a strategy for
that gives success probability
.
-
The supremum over all strategies of their probability of success is
.
When the total state space is finite these conditions are equivalent, but here where the counter creates an infinite space only the second holds.
The next issue is whether players are allowed to remember the game history so as to know the values of their counters, or at least test them for zero. The latter power suffices to emulate Marvin Minsky’s multiple-counter machines so many problems on arbitrary graphs become undecidable. In restricted cases this leads to further interesting distinctions and questions. Let us add to the above graph an arrow from back to
. Can the player reach
infinitely often? There is no single strategy that assures this, but in case bad luck at node
depleted the counter on the last go-round,
can use the memory to replenish it.
Mayr then went into energy games where nature is replaced by a second player who tries to bankrupt a counter. In a recent paper he and others carved out a decidable case of the problem of who wins. This is when there is just one energy counter and the game-graph itself is induced by a one-counter automaton.
Stefan Göller talked about
-dimensional vector addition systems with states (VASS). The standard definition without states is that you have a non-negative start vector
and a set
of vectors with positive and negative integer entries. The transitions allow adding a vector
to your current vector
, provided u+v is non-negative. Thus it is a solitaire version of the energy games we just mentioned with
counters, where
is the dimension of the vectors. In Göller’s case you also change state—and this may affect the subset of
available to use at the next state.
Göller led off by quoting Dick’s lower bound for the simple case, which Dick covered near the start of this blog. In his talk he covered his recent joint paper showing that for
the problem is
-complete. The real surprise here is the
upper bound, since only a double-exponential time upper bound was known dating from almost 30 years ago. The proof is a deep classification and analysis of three basic types of computational flow patterns. I don’t have time to reproduce the pretty pictures and the sketch of his proof from my notes, but the pictures appear in the paper.
Indeed, I have only gone through three of the first four talks on the first day—there was much great material in the rest and I will have to pick it up another time.
Open Problems
As our last post hinted with its discussion of possible connections between the Skolem Problem and Fermat’s Last Theorem, we suspect that number-theory issues are governing the complexity levels. Can this be brought out in a bird’s-eye view of the various reachability problems?




Gregory Chaitin has a proof of the infinity of the primes which uses Kolmogorov complexity. The idea is that a set of bounded entropy can’t generate a set of unbounded entropy. I wish it were possible to reason similarly to prove that a single polynomial SAT solver could not generate, modulo the polynomial reductions, every possible polynomial Turing machine. But numbers are simpler objects than programs… or at least, they interfere less with our own mental processes!