ω-Automata Feb 2021

Question

How to write the transition(R) for (a SU b) and also which slides to refer for this?

Answer 1

Well. The transitions formula is already in the solutions. It's ¬q∧a∧¬b∧¬q′∨(q∨b)∧q'.

Actually, when I designed the solution. I first drew the automaton, and then extracted the transition relation from that. The transition formula is a formula over the state variables, the alphabet, and the primed variables. Precisely the formulas satisfying assignments are the transitions that are in the relation. I divided the transitions into two parts. The incoming transitions of {}, and the ones of {q}. The transition to {} comes from q itself, and goes to {}. That's why we have ¬q∧¬q'. The condition of that transition is a∧¬b. If we add that as a conjunction, we get ¬q∧a∧¬b∧¬q′. The transitions to {q} both come from {q} itself with no condition and from {} with the condition b. If we write down these cases explicitly, we get the two formulas ¬q∧b∧q' and q∧q'. I simplified that as (q∨b)∧q'.

Symbolic transition relations were our topic in the Transition Systems chapter starting from slide 55.

How did I obtain the automaton itself? It is an NDetF automaton. So once we reach an accepting state on any infinite path corresponding to the input, we accept this input word. Thus, the initial state should rather not be accepting and we need at least one accepting state. The paths described by [a SU b] have three parts. First, they can not satisfy b for arbitrarily (including zero) steps but they need to satisfy a in every of these steps. Then they satisfy b for at least one state. And in the third part, they may do whatever they want. The waiting for the second part is implemented by having a self-loop at the non-accepting initial state. The condition of this self-loop is a∧¬b. As that's how the first part looks like. If our path doesn't satisfy this condition at any step, there is just no run in the automaton, and thus we don't accept. That's just the magic of non-determinism. The second part is just checked by this singled transition with the condition b from the non-accepting to the accepting state. Pretty straight-forward. Any accepting run needs to cross this transition at least once. Thus, we ensure that our input path satisfies b at least once (that's the strong about the strong until). For the third part of our input, we have no requirements. It can be any infinite suffix. Thus, we have a self-loop with no condition.

Did that make it clearer?

The deterministic version of the automaton (task c and d) is obtained in a similar way. As I said, we used the magic of non-determinism by just not offering any transition if we want to reject the input. In a deterministic world, we have to provide precisely one infinite run for any input. It just may not contain an accepting state. Thus, we just add a non-accepting (and non-initial) state with a self-loop with no condition. This fail state is reached by the remaining transition from the initial state. Thus, the transition from the initial to the fail state has the condition ¬a∧¬b.

In order to label the new state, I needed to introduce the fresh variable r. This actually produces two states {q} and {q,r}. For the unreachable state {q,r}, I just added any transition I found easy to write down in the symbolic variant.

Comments

Thank you for the explanation.

---

Helped? Learned a lot?

Answer 2

It is not clear what you mean with a transition relation for [a SU b]; clearly, I understand that you want the transition relation of an omega-automaton for [a SU b]. However, the latter needs to be discussed with a little care since there is a slight difference between initial and global equivalence of LTL formulas that can be explained with Martin's answer which is initial, but not global equivalent.

Consider the omega-automaton Am that Martin constructed; it looks as shown above, and we can easily prove that [a SU b] <-> F q holds when we run the omega-automaton on some trace. That means the omega-automaton Am is initally equivalent to [a SU b], since for any path, we have at time 0 that Am<->[a SU b]. You find that automaton also on slide 59 of the temporal logic chapter.

However, the equivalence Am<->[a SU b] is not true for all paths and all points of time t, so that Am and [a SU b] are not globally equivalent. The latter is often required for translations from LTL to omega-automata, since the subformulas that are translated to an omega-automaton have to be equivalent to that omega-automata at any point of time, and not just the initial one.

For global equivalence, you may consider the automaton Au := Auto(exists,{q},true,q<->b|a&next(q), GF(q→b)) whose state transition shown below. It is globally equivalent, i.e., for all paths and all points of time t, Au and [a SU b] are globally equivalent. Why that is so, is discussed on the slides 61-71 by considering all cases.

Comments

Thank you for the explanation