-4
$\begingroup$

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?

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

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)

$\endgroup$

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