Decomposing Properties into Safety and Liveness Using Predicate Logic.

Abstract

Two classes of properties are of particular interest when considering programs: safety properties and liveness properties. Informally, a safety property stipulates that 'bad things' do not happen during execution of a program and a liveness property stipulates that 'good things' do happen (eventually). Distinguishing between safety and liveness properties is useful because knowing whether a property is safety or liveness helps when deciding how to prove that the property holds for a program. A new proof is given that every property can be expressed as a conjunction of safety and liveness properties. The proof is in terms of first-order predicate logic. Keywords: Concurrency; Semantics.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 05, 1987
Accession Number
ADA187556

Entities

People

  • Fred B. Schneider

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Availability
  • Classification
  • Computer Science
  • Computers
  • Language
  • Military Research
  • Monitoring
  • New York
  • Security
  • Sequences
  • Specifications
  • Standards
  • Universities
  • Words (Language)

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Canadian European Scientific Immigration and Epilepsy Clearance Studies
  • Theoretical Analysis.