Recogizing safety and liveness

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. Th...

Full description

Bibliographic Details
Main Author: Alpern, Bowen
Other Authors: Schneider, Fred B.
Format: Electronic Article
Language:English
Subjects:
Online Access:Texto completo