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

529 users

0 votes

As I see that Weak Until is not used in the algorithm in lecture slides, how do we come to the answer shown below 

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

1 Answer

0 votes

You can ask the teaching tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html that knows all the cases. For instance:

G a ==> ∀t1. (t0≤t1 → a[t1])

F a ==> ∃t1. t0≤t1 ∧ a[t1]

[a WU b] ==> ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1])

[a WB b] ==> ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2])) → ¬b[t1])

[a SU b] ==> ∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → a[t2])) ∧ b[t1]

[a SB b] ==> ∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) ∧ a[t1]

All of these cases, however, just follow the given semantics of the temporal operators and describe that in LO1.
by (166k points)
Thank you very much for the answer.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...