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

769 questions

886 answers


424 users

0 votes
For this question we are meant to convert the omega automata

A∀({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp)

 to LO2, can we just use the formula that was given in slide 25 of the predicate logic slides so the answer in LO2 would be

∃q,p. ΘLO2(0, !p&!q )∧ (∀t. ΘLO2(t, ϕR)) ∧ (∀t1.∃t2.t1 < t2 ∧ ΘLO2(t2, GFp ))

where ϕR = (Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q))
in * TF "Emb. Sys. and Rob." by (790 points)

1 Answer

0 votes
Best answer

That formula is fine, but you need to negate it to get a universal quantification. The final answer should be 

    ¬q[0] ∧ ¬p[0] ∧ 
    ∀t. (q[t+1] ↔ (¬q[t] ∧ ¬a[t])) ∧ 
        (p[t+1] ↔ (¬p[t] → q[t]))
    → ∀t1.∃t2. t1<t2 ∧ p[t2]
by (117k points)
selected by
The negation only applies to the first existential quantifier right ? In your answer the negation was only applied to the quantifier ∃ in ∃q,p.
Don't know what you mean. What I wanted to say is that the given formula A∀({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp) may be first converted to ¬A∃({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), ¬GFp) so that you can apply the conversion to LO2 you mentioned. After that (it is not needed), you can drive in the negation and should get the formula I posted above.
when we had ΘLO2((Xq ↔ (¬q ∧ ¬a)), it was simplified to
(ΘLO2(Xq) ↔ ΘLO2((¬q ∧ ¬a)), is there a rule for this ?
Not really, but you can see that ΘLO2 leave propositional logic as it is, and just adds quantifiers, and applications to a time variable where needed.
oh okay, thanks
Imprint | Privacy Policy