Alternating Nonzero Automata
Paulin Fournier, Hugo Gimbert

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*.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
