LTL to automaton translation that can only read disjunctions of labels per transition

Question

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the automaton to read conjunction as well as disjunction of atomic propositions.

Answer 1

The models of an LTL formula $\varphi$, with atomic propositions $P$, are infinite words $w = \sigma_0\sigma_1\ldots$, where each $\sigma_i$ is a subset of $P$. To recognize such words, the edges of an automaton recognizing the language of $\varphi$ generally have to be labeled by symbols in $2^P$ (i.e. subsets of $P$).

Often multiple transitions are grouped by labeling edges in the automaton with boolean formulas over $P \cup \tilde{P}$, where $\tilde{P}$ is the set of negated atomic propositions. The edge label $f$ then stands for all models of $f$. In nondeterministic Büchi automata we can restrict $f$ to be a conjunction, as disjunction in the label can be modeled by introducing another transition.

Universal automata are the dual of nondeterministic automata, so to accept a word $aw, a \in \Sigma, w \in \Sigma^{\omega}$ from a state $q$, $w$ has to be accepted from all $a$-successors of $q$. Combining universal and nondeterministic branching one gets alternating automata. In universal automata for LTL formulas you can restrict the edge label to be a disjunction over $P \cup \tilde{P}$, as you can model conjunction in the label by introducing another transition.

With the right acceptance universal automata are as expressive as LTL, for example co-Büchi universal automata can recognize all $\omega$-regular languages.

Edit: I don't think this is a good answer after second thought. The reason is that grouping transitions in this way makes no sense for universal automata, unless the formulas on the labels have disjoint models. Example: Splitting $x \xrightarrow{a \land b} y$ into $x \xrightarrow{a} y$ and $x \xrightarrow{b} y$ adds the possibility to move to $y$ when only satisfying $a$, which was not possible before. I don't see any natural way of having an automata with only disjunctive boolean formulas as edge labels, however you can get rid of the formulas entirely on the edge labels by just using symbols in $2^P$.