Over the last decades the theory of automata on infinite objects has been an important source of tools for the specification andthe verification of computer programs. Trees are more suitable than words to model nondeterminism and concurrency. In the literature, there are several examples of acceptance conditions that have been proposed for automata on infinite words and then have been fruitfully extended to infinite trees. The type of acceptance condition can influence both the succinctness of the language acceptors and the computational complexity of the decision problems. Here we consider, relatively to automata on infinite trees, two acceptance conditions that are obtained by relaxing Muller acceptance condition: the Landweber and the Muller-Superset conditions. We prove that Muller-Superset tree automata accept the same class of languages as Büchi tree automata. Also, we show that for such languages the minimal Muller-Superset acceptor is at least as succinct as the minimal Büchi acceptor and, in some cases, it can be exponentially more succinct. Landweber tree automata, instead, define a class of languages that is not comparable with that defined by Büchi tree automata. The main result we prove is that the emptiness problem for this class of automata is decidable in polynomial time, andthus we extendthe class of automata with a tractable emptiness problem.

Weak Muller acceptance conditions for tree automata

LA TORRE, Salvatore;NAPOLI, Margherita
2005-01-01

Abstract

Over the last decades the theory of automata on infinite objects has been an important source of tools for the specification andthe verification of computer programs. Trees are more suitable than words to model nondeterminism and concurrency. In the literature, there are several examples of acceptance conditions that have been proposed for automata on infinite words and then have been fruitfully extended to infinite trees. The type of acceptance condition can influence both the succinctness of the language acceptors and the computational complexity of the decision problems. Here we consider, relatively to automata on infinite trees, two acceptance conditions that are obtained by relaxing Muller acceptance condition: the Landweber and the Muller-Superset conditions. We prove that Muller-Superset tree automata accept the same class of languages as Büchi tree automata. Also, we show that for such languages the minimal Muller-Superset acceptor is at least as succinct as the minimal Büchi acceptor and, in some cases, it can be exponentially more succinct. Landweber tree automata, instead, define a class of languages that is not comparable with that defined by Büchi tree automata. The main result we prove is that the emptiness problem for this class of automata is decidable in polynomial time, andthus we extendthe class of automata with a tractable emptiness problem.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11386/1064784
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact