# 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?

## closed as off-topic by Emil Jeřábek, Martin Berger, Kaveh, R B, Mohammad Al-TurkistanyFeb 8 '15 at 10:13

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Emil Jeřábek, Martin Berger, Kaveh, R B, Mohammad Al-Turkistany
If this question can be reworded to fit the rules in the help center, please edit the question.

• 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)