Temporal Logic - Until [closed]

I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula?

ex: a U b does require that the first term is a ?
Is the sequence bbbbbb..bb valid?

• I am not sure whether this is a research-level question in theoretical computer science. – J.-E. Pin Feb 7 '15 at 13:38
• Is not LTL a theoretical computer science topic? – Nk SP Feb 7 '15 at 14:31
• Sure it is, but the question is quite basic :) – User Feb 7 '15 at 17:30

When you evaulate until formulae on paths, you usually require that either $b$ is the case to begin with, or you have a number $a$'s until a $b$ is met.
$bbbb \ldots b$ therefore satisfies the formula.
$\lnot \text{bad } U \text{ goal }$
One way to satisfy this property is that the starting configuration satisfies the desired property i.e goal (the semantics may also require $\lnot$bad in this configuration)