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?

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

1 Answer 1


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.

Example usage:

If you want in a system to reach a state satisfying a goal property while ensuring that no intermediate states have a bad property you could verify the following 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)


Not the answer you're looking for? Browse other questions tagged or ask your own question.