Abstract: 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. On the other hand, with a few notable exceptions, adding transitive closure to even very tame logics makes them undecidable.
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 language called EA(TC+[E]) that goes beyond trees, includes a version of transitive closure, and is decidable. We show that satisfiability of EA(TC+[E]) is NEXPTIME complete. We furthermore show that essentially any reasonable extension of EA(TC+[E]) is undecidable.
Our main contribution is to demonstrate these sharp divisions between decidable and undecidable. We also compare the complexity and expressibility of EA(TC+[E]) with related decidable languages including MSO(trees) and guarded fixed point logics.
We mention possible applications to systems some of us are building that use decidable logics to reason about programs.
Recent Publications of Neil Immerman