+1 vote

in paper Feb,2017 

problem 5,b 

construct a deterministic liveness automaton that accept L1 can we use future operator instead of past one if yes we get the answer directly like prob 5,c  third equation  or we have to convert something .

while I read a question about future and past and the answer was

"The advantage of using past operators is that a translation to an equivalent ω-automaton will give us directly a deterministic one, and deterministic automata are easier to deal with when it comes to boolean combinations, in particular, negations."

can we use future operators to construct both Det and NondDet automaton directly from the LTL to ω-automaton equations.

in TUK (TU Kaiserslautern) by (130 points)

1 Answer

+2 votes

That problem asks for a deterministic liveness automaton for the language. Here are three ways you could follow:

  1. Construct such an automaton directly and explain why it should be correct. I don't recommend this, since you may easily forget transitions etc. 
  2. Construct an equivalent LTL formula for the language (which is typically simple an F, G, FG, GF with some X operators for the single letters). If you use future operators, the translation of the LTL formula to automata gives you a nondeterministic automaton. If that one uses a GF-constraint, you are lost since you don't know how to determinize this. Otherwise, you will have to apply the breakpoint construction, and to that end, you have to make the automaton first explicit. I also cannot recommend this way. 
  3. Construct an equivalent LTL formula for the language using some F, G, FG, GF followed by past operators only. If you do the standard translation from here, you directly obtain a deterministic automaton. This is the simple and very efficient solution I definitely would prefer. 
Future operators translate to nondeterministic automata that have to be determined in a second step. Past operators directly give you a deterministic automaton. You can see that with the transition relations introduced for the past operators which are of the form q' <-> Phi(q,i) that defines the next value q' of q by the current values of q (states) and i (inputs). This is not the case for the automata for future LTL operators. 
by (15k points)
Even if the question would not ask directly for a deterministic automaton, and the next question would ask for further steps like the complement of the automaton, a deterministic automaton will give you many advantages.

Related questions

+1 vote
1 answer
+1 vote
1 answer
asked Aug 17, 2018 in * TF "Emb. Sys. and Rob." by KS (15k points)
Imprint | Privacy Policy
...