The Boundary Between Decidability and Undecidability for Transitive Closure Logics
N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh
To reason effectively about programs it is important to
have some version of a transitive closure operator so that
we can describe such notions as the set of nodes reachable
from a program's variables.
In this paper we explore the boundary between decidability
and undecidability for transitive closure logics. Rabin
proved that the monadic second order theory of trees
is decidable although the complexity of the decision procedure
is not elementary. If we go beyond trees, however,
undecidability comes immediately.
We have identified a rather weak first-order language
called "$(DTC[E]) that goes beyond trees, includes a version
of transitive closure, and is decidable. We show that
satisfiability of "$(DTC[E]) is NEXPTIME complete. We
furthermore show that essentially any reasonable extension
of "$(DTC[E]) is undecidable.
Our main contribution is to demonstrate these sharp
divisions between decidable and undecidable. We also
compare the complexity and expressibility of "$(DTC[E])
with related decidable languages including MSO(trees) and
guarded fixed point logics.
We mention possible applications to systems some of us
are building which use decidable logics to reason about pro-grams.
(Click here to access the paper:
PostScript,
PDF.)