Bowen Alpern, Alan Carle, et al.
ACM SIGPLAN Notices
A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjunction is the original. The characterizations also give insight into techniques required to prove a large class of safety and liveness properties. © 1987 Springer-Verlag.
Bowen Alpern, Alan Carle, et al.
ACM SIGPLAN Notices
Martín Abadi, Bowen Alpern, et al.
Information Processing Letters
Bowen Alpern, Mark N. Wegman, et al.
POPL 1988
Bowen Alpern, Joshua Auerbach, et al.
VEe 2005