Relative liveness and behavior abstraction (extended abstract)
Ulrich Ultes‐Nitsche, Pierre Wolper · 1997
This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used.It shows that using a more abstract notion than truth under fairness, specifically the concept of relative liveness property can lead to interesting possibilities.Technically, it is first established that deciding relative liveness is a PSPACE-complete problem and it is shown that relative liveness properties ca aiways be satisfied by some fair implementation.Thereafter, the interaction between behavior abstraction and relative Iiveness properties is studied and it is proved that relative liveness properties can be verified on behavior abstractions, if the abstracting homomorphism is simple in the sense of Ochsenschlager.