Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
A Formalised Lower Bound on Undirected Graph Reachability
verfasst von : Ulrich Schöpp
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We study the expressivity of Jumping Automata on Graphs (
jag
s), an idealised model of computation with logarithmic space.
jag
s operate on graphs by using finite control and a constant number of pebbles. In this paper we revisit the proof of Cook & Rackoff that
jag
s cannot decide
s
-
t
-reachability in undirected graphs. Cook & Rackoff prove this result by constructing, for any given
jag
, a finite graph that cannot be traversed exhaustively by the
jag
. We generalise this result from the graphs constructed by Cook & Rackoff to a general class of group action graphs. We establish a bound on the number of nodes that a
jag
can visit on such action graphs. This generalisation allows us to strengthen the result of Cook & Rackoff to the existence of a graph of small degree whose diameter (rather than its number of nodes) is larger than the number of nodes the
jag
can visit. The main result has been formalised in the theorem prover Coq, using Gonthier’s tactic language
SSReflect
.