C.5 Safety Properties

C.5 Safety Properties

A safety property Q in FSP is represented by an image of the LTS of the process expression that defines the property. The image LTS has each state of the original LTS and has a transition from each state for every action in the alphabet of the original. Transitions added to the image LTS are to the error state.

 property Q = E:          lts(Q) =def image(lts(E)),          for an LTS P =< S, A, Δ, p >, image(P) = < S ∪ {π}, A, Δ′, q >,          where Δ′ = Δ ∪ {(s, a, π)|s ∈ S, a ∈ A, and  ∈ S: (s, a, s′) ∈ Δ}.