Completing the Temporal Picture,

Abstract

The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves on previous temporal systems, such as (MP83a) and (MP83b), in that it reduces the validity of program properties into pure assertional reasoning, not involving additional temporal reasoning. The proof system is based on the classification of temporal properties according to the Borel hierarchy, providing an appropriate proof rule for each of the main classes, such as safety, response, and progress properties.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1989
Accession Number
ADA328579

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Applied Mathematics
  • Automata
  • Classification
  • Computations
  • Computer Program Verification
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Hierarchies
  • Invariance
  • Language
  • Mathematics
  • Sequences
  • Symbols
  • Verification

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.