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


546 users

+1 vote


I have a doubt regarding LO2 ,

F[a WU b] to LO2 formula. The answer for this is given :

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

But i got, 

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

I'm not sure how can we give the time. 

What i have is , 

we have: Fa = ∃t1. t0≤t1 ∧ a[t1] 

so F[a WU b] = ∃t1. t0≤t1 ∧ [a WU b][t1] 

[a WU b] = ∀t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2≤t1 → ¬b[t2])) → a[t1]), but we are starting from the time t1, so i replaced the time accordingly. 

And finally 

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

but timing are little bit different from tool and what i got. Could you please help on this, how can i give the time?

in # Study-Organisation (Master) by (2.7k points)

1 Answer

+1 vote
Best answer
The teaching tool uses as few variables as possible. Indeed, one can show that three variables are sufficient because of the special kind of predicate logic that corresponds with LTL. You have used other names to avoid the shadowing of existing variables, which is safer than what the tool does. So, yes, your solution is correct.
by (166k points)
selected by
Thank you professor

Related questions

Imprint | Privacy Policy