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?
-4
$\begingroup$
$\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$
$\endgroup$
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)
