Proving Precedence Properties: The Temporal Way,

Abstract

The paper explores the three important classes of temporal properties of concurrent programs: invariance, liveness and procedence. It presents the first methodological approach to the precedence properties, while providing a review of the invariance and liveness properties. The approach is based on the unless operator 'U', which is a weak version of the until operator 'U'. For each class of properties, we present a single complete proof principle. Finally, we show that the properties of each class are decidable over finite state programs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1983
Accession Number
ADA128148

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Air Platforms
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Applied Mathematics
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Families (Human)
  • Hierarchies
  • Information Processing
  • Invariance
  • Language
  • Mathematics
  • Programming Languages
  • Sequences
  • Specifications

Readers

  • Mathematical Modeling and Probability Theory.