I`m having difficulties at understanding how we modelled these automata by using Linear Temporal Logic. Can someone, please please, explain this to me, on the cases which are on the picture in this link, or point me to a source that explains this on examples.
I thank you in advance for your help.
LTL formula are defined over an alphabet (which is usually referred to as "atomic propositions", and in your examples the alphabet is the set
{x,y}). An LTL formula splits the infinite sequences of subsets of the alphabet into (infinite-)words that satisfy the formula and those that don't. For example, the word{x}, {x,y}, {}, {}...satisfies the formulaF not x and not y, but does not satisfy the formulaGy.A Buchi automaton does the same. It reads an infinite word over some alphabet and either accepts or rejects the word. Vardi and Wolper showed that it is possible, given an LTL formula, to construct a Buchi automaton that accepts exactly the infinite words that satisfy the formula. You can see the construction here.