# Emptiness of zero automata is decidable

## TL;DR

This paper proves that the emptiness problem for zero automata, a probabilistic automaton on infinite trees, is decidable by introducing nonzero automata and establishing their equivalence, impacting the decidability of related logical satisfiability.

## Contribution

It introduces nonzero automata, shows their equivalence to zero automata, and proves the emptiness problem is decidable and in NP and coNP, advancing automata theory and logic satisfiability.

## Key findings

- Emptiness problem for zero automata is decidable.
- Nonzero automata are equivalent to zero automata with quadratic size.
- Decidability results imply satisfiability of tmso + zero is decidable.

## Abstract

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of mso, called tmso + zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable and both in NP and in coNP. These results imply that tmso + zero has decidable satisfiability.