Decidability of the Theory of the Totally Unbounded omega-Layered Structure Angelo Montanari and Gabriele Puppis   View Paper (PDF)   Return to Short Papers Abstract In this paper, we address the decision problem for a system of monadic second-order logic interpreted over an ù-layered temporal structure devoid of both a finest layer and a coarsest one (we call such a structure totally unbounded). We propose an automaton-theoretic method that solves the problem in two steps: first, we reduce the considered problem to the problem of determining, for any given Rabin tree automaton, whether it accepts a fixed vertex-colored tree; then, we exploit a suitable notion of tree equivalence to reduce the latter problem to the decidable case of regular trees. BIBTEX @inproceedings{DBLP:conf/time/MontanariP04,    author    = {Angelo Montanari and                 Gabriele Puppis},    title     = {Decidability of the Theory of the Totally Unbounded omega-Layered                 Structure.},    booktitle = {TIME},    year      = {2004},    pages     = {156-160},    ee        = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550156abs.htm},    crossref  = {conf/time/2004},    bibsource = {DBLP, http://dblp.uni-trier.de}  }  @proceedings{DBLP:conf/time/2004,    title     = {11th International Symposium on Temporal Representation                 and Reasoning (TIME 2004), 1-3 July 2004, Tatihou Island,                 Normandie, France},    booktitle = {TIME},    publisher = {IEEE Computer Society},    year      = {2004},    isbn      = {0-7695-2155-X},    bibsource = {DBLP, http://dblp.uni-trier.de}  } }, ©2005 Association for Computing Machinery