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


510 users

0 votes

Could you explain how you derived the formula here (Problem 7a. September 6, 2022 exams). The formula in the lecture slide seems different from this.

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

1 Answer

0 votes

For G[a WU b], we may simply apply the standard translation to LTL (pages 83-83), but we may also skip the GF-constraints for positive occurrences of weak and negative occurrences of strong temporal operators (page 94). In our case, both operators are weak and have positive occurrences, so that no GF-constraints are generated.

    G[a WU b]
        = AE({p},true,p<->b|a&Xp,Gp)
        = AE({p,q},true,(p<->b|a&Xp)&(q<->p&Xq),q)
        = AE({p,q},q,(p<->b|a&Xp)&(q<->p&Xq),true)

What is different to the lecture slides? Maybe I don't get what you mean?

Remark: It has already been pointed out that we may already take AE({p},true,p<->b|a&Xp,Gp) as a two-state safety automaton as the result. 

by (162k points)
My confusion is this part &(q<->p&Xq),q
What is wrong with it? As explained on slides 95-99, we apply the abbreviations step by step which generates a conjunction of transition equations and a conjunction of fairness constraints, right?
Got it. Thank you

Related questions

Imprint | Privacy Policy