The Boundary Between Decidability and Undecidability for Transitive-Closure Logics

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 ∃ ∀ (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 that use decidable logics to reason about programs.