College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||Recognizing Safety and Liveness|
|Authors: ||Alpern, Bowen|
Schneider, Fred B.
|Keywords: ||computer science|
|Issue Date: ||Jan-1986|
|Publisher: ||Cornell University|
|Abstract: ||Formal characterizations for safety properties and liveness properties are 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.|
|Appears in Collections:||Computer Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.