I have doubt regarding LO2,
We know that :
Subset(p, q) :⇔ ∀t.p (t) → q (t)
Sing(p) :⇔ [∃t1.p (t1) ] ∧ [∀t1t2.p (t1) ∧ p (t2) → t1 .= t2]
PSUC(p, q) :⇔ Sing(p) ∧ Sing(q) ∧ ∀t.p (t) → q (t+1) .
How to derive the omega-automaton formula for Subset(p, q), Sing(p), and PSUC(p, q)?
We know these are the acceptance for :
Subset(p, q) : G¬s1
Sing(p): Fs1 ∧ G¬s2
PSUC(p, q): Fs2 ∧ G¬s3
Can we use these formulas as acceptance and get an omega automaton formula for them? Or is there any omega automaton already defined for them? Could you please give one example omega automaton formula for subset, sing and PSUC?
