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 demo...

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh
• Keywords: CSL 2004, Monadic Second-order Theory, Tame Logics, Transitive Closure