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

928 questions

1k answers

1.4k comments

441 users

0 votes

I was trying to convert LTL to LO2, i used the Algorithm mentioned on the slide. On the left side, the solution I got by doing the algorithm but on the right side, the answer is given in the question paper. Can you help me to figure out what went wrong? [I have abbreviated big formulas to A , B and C respectively ]  

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

1 Answer

+1 vote
 
Best answer
You have mixed up the weak and strong until operators. In the exam problem, it was a weak until, while your solution considers a strong until.
by (143k points)
selected by
okay. But I have a question. The given question was F[a WU b]. First I found the LO1 for F and the remaining part was [a WU b]. I used the below syntactic sugar.
[ϕ WU ψ] := [ϕ SU ψ] ∨ Gϕ.
And I proceeded with this. So it will be a case for disjunction and did split these. After that, I found LO1 for [a SU b] and then Ga. And finally combined everything together. So will it have any other impact?
I see that is fine also. Of course, you can generate many equivalent formulas in different ways. The one you had in mind is fine also.
Thanks for the advice. I will stick with this kind of reduction rule and work on the algorithm. Thank you, Professor.
You can go many ways: If the formula F[a WU b] is translated directly, you get
∃t1. t0≤t1 ∧ (∀t0. (t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2≤t0 → ¬b[t2])) → a[t0]))

If you replace it with the equivalent formula F([a SU b] | G a), you get
∃t1. (
        (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ b[t0]) ∨
        (∀t0. (t1≤t0 → a[t0]))) ∧ t0≤t1
Φ = F([a SU b] | G a)

Step 1: Tp2Od(t0, F([a SU b] | G a)), which is FΦ
             Ψ := ∃t1. t0≤t1 ∧ Φ ;
             ΨA := ∃t1. t1≤t0 ∧ ([a SU b] | G a) ;

Step 2: Tp2Od(t0, [a SU b] | G a), which is ϕ ∨ ψ
             Ψ := Tp2Od(t0, [a SU b]) ∨ Tp2Od(t0, G a);

Step 3: Tp2Od(t0, [a SU b]), which is [ϕ SU ψ]
            Ψ := ∃t1. t0 ≤ t1 ∧ Tp2Od(t1, b) ∧ interval((t0, 1,t1, 0), a)
                    Tp2Od(t1, b) = b(t1)
                    interval((t0, 1,t1, 0), a) = ∀t2. t0 ≤ t2 ∧ t2 < t1 → Tp2Od(t2, a);
                    Tp2Od(t2, a) = a(t2)
                  ΨB := ∃t1. t0 ≤ t1 ∧ b(t1)   ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2)

Step 4: Tp2Od(t0, G a), which is Gϕ
             Ψ :=  ∀t1. t0 ≤ t1  ∧ Φ
              ΨC:=  ∀t1. t0≤ t1  ∧ a(t0)

Step 5: Combining all :
            ΨA  ∧ (ΨB ∨ ΨC)(t0)

My final solution is :
∃t1. t0≤t1 ∧ ((∃t1. t0 ≤ t1 ∧ b(t1)  ∧ ∀t2. t0 ≤ t2 ∧ t2 < t1 →a(t2) )∨ (∀t1. t0≤ t1  ∧ a(t0)))
     
Is this formula in reduced form? Or are they different? I am not sure how to give the numbering for "t".
∃t1. (
        (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → a[t2])) ∧ b[t0]) ∨
        (∀t0. (t1≤t0 → a[t0]))) ∧ t0≤t1
Your formula is not correct; you have to use new variables since otherwise the free variables are bound which not not be the case.

Your formula is as follows

∃t1. t0≤t1 ∧ ((∃t1. t0≤t1 ∧ b(t1) ∧ ∀t2. t0≤t2 ∧ t2<t1 → a(t2) ) ∨ (∀t1. t0≤t1  ∧ a(t0)))

but should be rather

∃t1. t0≤t1 ∧ ((∃t3. t1≤t3 ∧ b(t3) ∧ ∀t2. t0≤t2 ∧ t2<t3 → a(t2) ) ∨ (∀t4. t1≤t4  ∧ a(t4)))

The above is then correct as far as I can see.
Are there any general rules for using new variables? [Is it okay to take t3<t2 like that?]
Can this be a valid one?
∃t1. t1≤t0 ∧ ((∃t2. t1 ≤ t2 ∧ b(t2)   ∧ ∀t3. t1 ≤ t3 ∧ t3 < t2 →a(t3)) ∨ (
∀t4. t1 ≤ t4  ∧ a(t4))
For any instance of Tp2Od that generates a formula with quantifiers, you need fresh variables in case that the body formula would have already that variable that would be used for quantification.
okay..I got it now..Thank you, professor.
Imprint | Privacy Policy
...