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?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
