效绵鼎 if3tET,(t)=s∧B(t)=s',we say s→s',we define the generalized transition relation S X A X S such that 0IfS→s',S》s' Ifss',s'-》s",we say s》s" ■ Let A=<S,So,T,a,B be a TS,we say s is reachable if s∈S,So∈So,SoS◼ 𝑖𝑓 ∃ 𝑡 ∈ 𝑇, 𝛼 𝑡 = 𝑠 ⋀𝛽 𝑡 = 𝑠 ′ ,we say s → 𝑠 ′ , we define the generalized transition relation ↠⊆ S × A × S such that  If s → 𝑠 ′ , s ↠ 𝑠 ′  If s ↠ 𝑠 ′ , s ′ ↠ 𝑠 ′′ , 𝑤𝑒 𝑠𝑎𝑦 𝑠 ↠ 𝑠 ′′ ◼ Let 𝒜 =< 𝑆, 𝑆0 ,𝑇, 𝛼, 𝛽 > be a TS, we say s is reachable if 𝑠 ∈ 𝑆, 𝑠0 ∈ 𝑆0 , 𝑠0 ↠ 𝑠