LO1 semantics

Question

1. ∀t2.t0 ≤ t2 < t1 → a^t1

The above LO1 is interval((t0,1,t1,0), a), and it says between t0 and t1 a should hold excluding t1.

2. ∀t2. t1 ≤ t2 → b^t1

The second LO1 says b is true until t2 and t2 might be included. (if the last part of formula is b[t2], I know that it is Gb but for this I am unable to figure out)

For the above formula I explained what I understood so far, but I am still unable to understand it in proper way.

Q1. Could you please explain about how to read it properly ?

Q2. Could you please explain how can I interpret it interms of LTL ?

Answer 1

Well, you already explained the formulas as they are. If you want to rephrase them in LTL, that is possible for the second one which is G b, but the first one has two free numeric variables which has no meaning in LTL. Maybe that is what is bothering you.