I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a deterministic Büchi automaton, then why not? Do you have examples for that case?

| cite | improve this question | | | | |

There are languages that are representable by an LTL formula but by no deterministic Büchi automaton (DBA). Thus a translation from LTL to DBA cannot exist. An example is the formula $\mathbf{F}\mathbf{G} a$, which states that from some moment on $a$ has to hold forever. A nondeterministic Büchi automaton can guess when this moment occurs.

No deterministic Büchi automaton can accept the corresponding language. To see this, assume that there is a DBA for the language and note that when reading only $a$ an accepting state must be visited at some point. After visiting the accepting state, let the next symbol of the input word be $b$, and then $a$ again until another accepting state is reached. Such a state must be reached again eventually, as $a^* b a^{\omega}$ is part of the language. By iterating this idea a word can be constructed that is not in the language but nevertheless is accepted by the automaton, which contradicts the assumption.

| cite | improve this answer | | | | |

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.