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.