Accession Number:

ADA128148

Title:

Proving Precedence Properties: The Temporal Way,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1983-04-01

Pagination or Media Count:

39.0

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.

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE