A Temporal Proof Methodology for Reactive Systems,

Abstract

The paper presents a minimal proof theory which is adequate for proving the main important temporal properties of reactive programs. The properties we consider consist of the classes of invariance, response, and precedence properties. For each of these classes we present a small set of rules that is complete for verifying properties belonging to this class. We illustrate the application of these rules on several examples. We discuss concise presentations of complex proofs using the devices of transition tables and proof diagrams.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1993
Accession Number
ADA262848

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Automata
  • Complex Systems
  • Composite Materials
  • Computations
  • Computer Science
  • Computers
  • Electronic Mail
  • Encapsulation
  • Formal Languages
  • Guarantees
  • Language
  • Specifications
  • Standards
  • United States
  • Universities

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.