Sooner Is Safer Than Later,

Abstract

It has been repeatedly observed that the standard safety-liveness classification of properties of reactive systems does not fit for real time properties. This is because the implicit 'liveness' of time shifts the spectrum towards the safety side. While, for example, response - that 'something good' will happen, eventually - is a classical liveness property, bounded response - that 'something good' will happen soon, within a certain amount of time - has many characteristics of safety. We account for this phenomenon formally by defining safety and liveness relative to a given condition, such as the progress of time.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 28, 1991
Accession Number
ADA325549

Entities

People

  • Thomas Henzinger

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Air Force
  • Automata
  • Classification
  • Commerce
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Information Processing
  • Information Systems
  • Language
  • Machines
  • Specifications
  • Standards
  • Theoretical Computer Science
  • Time Domain
  • United States

Readers

  • Educational Psychology
  • Mathematical Modeling and Probability Theory.