Proving Nondeterministically Specified Safety Properties Using Progress Measures

Information and Computation - United States
doi 10.1006/inco.1993.1064