In this paper we provide an automaton-based solution to the decision problem for a large set of monadic second-order theories of deterministic tree structures. We achieve it in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of ) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. We conclude the paper with a short discussion of related work.

Decidability of MSO Theories of Tree Structures

MONTANARI, Angelo
;
PUPPIS, Gabriele
2004-01-01

Abstract

In this paper we provide an automaton-based solution to the decision problem for a large set of monadic second-order theories of deterministic tree structures. We achieve it in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of ) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. We conclude the paper with a short discussion of related work.
2004
3540240586
File in questo prodotto:
File Dimensione Formato  
FSTTCS 2004.pdf

non disponibili

Licenza: Non pubblico
Dimensione 222.06 kB
Formato Adobe PDF
222.06 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/856753
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact