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


524 users

0 votes

I have a doubt regarding LTL model checking. Why [a SU a] is neglected? I read that, we can neglect the positive occurrence of WU and the negative occurrence of SU. I am not sure about what it's meant by positive occurrence and negative occurrence. Could you please clarify?

As per the syntactic sugar,

q0<->[a SU a]

Φ[ϕ SU ψ]x ⇔ A∃ ({q}, 1, q ↔ ψ ∨ ϕ ∧ Xq, Φqx ∧ GF[q → ψ]) ,

but how did it become GF(¬q0 → a) instead of GF(q0 → a)?

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

1 Answer

0 votes
Positive and negative occurrences essentially means under an even and odd number of negations, i.e., in !a&b|!(!c&d) the variables a and d have negative occurrences while b and c have positive ones.
by (165k points) this [b SU Ga], can I write Ga to ![true SU !a] and it's a negative occurrence of SU. So that I'm ignoring it. Therefore remaining acceptance condition will be [b SU q0], which is a positive occurrence of SU. Then it will be GF[q2->q0] but in the slide, it is given as GF(q → p) ∧ GF(a → p). Is it valid?

Related questions

Imprint | Privacy Policy