omega-automaton

Question

In this question its mentioned that we need to convert [a su b], i have converted to [a su b] to GF then got stuck in between. Do we have a formula to convert [a su b] directly to F automaton. Could you please help on this? 

Answer 1

Yes, there is an algorithm that does that translation. Unfortunately, most students stop reading the slides after the main translation up to page 91 in VRS-07-TemporalLogic. Pages  92-94 and the examples on pages 95-99 show first that some of the fairness constraints are not required.

Pages 100-102 motivate subclasses of temporal logic that correspond with safety, liveness, persistence and fairness properties. Pages 104-109 show then then we can use implications instead of equivalences for the transition relation, and this is the key to use weaker constraints than the fairness constraints which is then proved on pages 110-114.

The final translation to safety and liveness constraints is given on pages 115-116, and examples are shown on pages 117-127.

Have a look at these additional slides, they explain everything you need to solve the exercise.

Comments

Thanks, i have checked slides, i could see we have two formuals for SU in 115 and 116. I didn't fully understand how to check if [a SU b] is a positive occurrence or negative? My second doubt is , if its a positive occurrence we have acceptance state as FG!phi, if its a negative occurrence we have nothing, What does that mean, And i could find the acceptance state of F in that. Could you please clarify ?

---

So, if you have an omega-automaton without acceptance condition, you can add the acceptance condition G true to make it a safety automaton. If you determinize it, you get an acceptance condition G phi with some state set phi. The negation such an automaton is a F-automaton since for deterministic automata, you just have to negate the acceptance condition. Hence, to translation [a SU b] to a F-automaton, you may translate ![a SU b] to a G-automaton, determinize it, and negate it to obtain a deterministic F-automaton for [a SU b].

P.S.: Positive/negative occurrences means whether the occurrence is behind an even or odd number of negations.

---

I understood it, Thank you