Defining liveness

A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that 'something good' eventually happens during execution. A topological characterization of safety and liveness is given. Every property is...

Full description

Bibliographic Details
Main Author: Alpern, Bowen
Other Authors: Schneider, Fred B.
Format: Electronic Article
Language:English
Subjects:
Online Access:Texto completo
Description
Summary:A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that 'something good' eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.
Physical Description:1 recurso en línea (p. 181-185)