<p>When you evaulate until formulae on paths, you usually require that <strong>either</strong> $b$ is the case to begin with, <strong>or</strong> you have a number $a$'s until a $b$ is met.</p>

<p>$bbbb \ldots b$ therefore satisfies the formula.</p>

<p><strong>Example usage:</strong></p>

<p>If you want in a system to reach a state satisfying a <strong>goal</strong> property while ensuring that no intermediate states have a <strong>bad</strong> property you could verify the following formula:</p>

<p>$\lnot \text{bad } U \text{ goal }$</p>

<p>One way to satisfy this property is that the starting configuration satisfies the desired property i.e <strong>goal</strong> (the semantics may also require $\lnot$bad in this configuration)</p>

CC BY-SA 3.0
2015-02-07T12:42:59.543Z
2015-02-07T13:01:50.967Z
2015-02-07T13:01:50.967Z
User
<p>I have a doubt, in <em>Linear Temporal Logic LTL</em>, does the <strong>Until operator</strong> require that the first occurrence is the first term of the formula?<br></p>

<p>ex:  <code>a U b</code> does require that the first term is <code>a</code> ?<br>
Is the sequence <code>bbbbbb..bb</code> valid?</p>

CC BY-SA 3.0
2015-02-07T13:38:23.290Z
I am not sure whether this is a research-level question in theoretical computer science.
J.-E. Pin
CC BY-SA 3.0
2015-02-07T14:31:35.693Z
Is not LTL a theoretical computer science topic?
Nk SP
CC BY-SA 3.0
2015-02-07T17:30:01.100Z
Sure it is, but the question is quite basic :)
User
<lo.logic><model-checking><temporal-logic>
Temporal Logic - Until
Nk SP
# Temporal Logic - Until

(Asked by: username_0 on 2015-02-07)

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?

**Tags:** lo.logic, model-checking, temporal-logic

> **Comments:**
> **username_1**: I am not sure whether this is a research-level question in theoretical computer science.  
> **username_0**: Is not LTL a theoretical computer science topic?  
> **username_2**: Sure it is, but the question is quite basic :)  

---

## 1 answers

### Answer by username_2 on 2015-02-07. Score: 0 | Accepted answer

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)


---

