Alternating Nonzero Automata

TL;DR

This paper introduces alternating nonzero automata, extending non-deterministic nonzero automata, and provides decidability results for their emptiness problem, leading to algorithms for probabilistic temporal logic satisfiability.

Contribution

It defines a new class of automata on infinite trees and reduces their emptiness problem to known cases, enabling new decision procedures.

Findings

Decidability of the emptiness problem for alternating nonzero automata

Reduction of the problem to non-deterministic automata cases

Algorithms for probabilistic temporal logic satisfiability

Abstract

We introduce a new class of automata on infinite trees called \emph{alternating nonzero automata}, which extends the class of non-deterministic nonzero automata. We reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain as a corollary algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.