0
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ Welcome to Computer Science, SimonJ! I like your answer, it is comprehensive but complete and 'thinks ahead'. If you'd like, there are plenty unanswered questions on automata or linear-temporal-logic that could use an answer like yours! $\endgroup$ – Discrete lizard Mar 30 '18 at 9:08
  • $\begingroup$ @SimonJ thank you for your answer. Can you please elaborate more on this: "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" $\endgroup$ – Perissiane Mar 30 '18 at 11:10
  • $\begingroup$ @Perissiane When thinking about this again, maybe the answer is wrong after all. Grouping transitions in this way probably does not make sense for universal automata at all, as we would have to require the labels to be disjoint to make it meaningful. The reason is that the grouping already is a sort of disjunctive choice. $\endgroup$ – SimonJ Apr 2 '18 at 11:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.