Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

543 users

0 votes

1. ∀t2.t0 ≤ t2 < t1 → at1

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 → bt1

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 ?

in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

0 votes
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.
by (166k points)

Related questions

0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...