Visibly pushdown automata on trees: universality and u-universality

TL;DR

This paper investigates the computational complexity of universality and u-universality in visibly pushdown automata on trees, proposing antichain-based algorithms to efficiently decide these properties, including for hedge automata.

Contribution

It introduces antichain-based techniques for deciding universality and u-universality in visibly pushdown automata on trees, addressing their EXPTIME-hardness.

Findings

Algorithms for universality and u-universality of hedge automata.

Antichain-based methods improve decision procedures.

Complexity results for non-deterministic tree automata.

Abstract

An automaton is universal if it accepts every possible input. We study the notion of u-universality, which asserts that the automaton accepts every input starting with u. Universality and u-universality are both EXPTIME-hard for non-deterministic tree automata. We propose efficient antichain-based techniques to address these problems for visibly pushdown automata operating on trees. One of our approaches yields algorithms for the universality and u-universality of hedge automata.