The Temporal Logic of Actions I

RISC-Linz logo

Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC-Linz)
Johannes Kepler University, A-4040 Linz, Austria
  • Introduction
  • Logic Versus Programming
  • Goals of a Programming Logic
  • The Logic of Actions
  • State Functions and Predicates
  • Actions
  • Predicates as Actions
  • Validity and Provability
  • Rigid Variables and Quantifiers
  • The Enabled Predicate
  • Simple Temporal Logic
  • Temporal Formulas
  • Some Useful Temporal Formulas
  • Validity and Provability
  • The Raw Logic
  • Describing Programs with RTLA
  • Describing Programs with RTLA
  • TLA
  • Adding Liveness
  • Liveness as TLA Formulas
  • Fairness
  • Fairness
  • Rewriting the Fairness Requirement
  • Examining Formula Phi
  • Syntax of Simple TLA
  • Semantics of Simple TLA
  • Additional Notation
  • The Rules of Simple Temporal Logic
  • The Basic Rules of TLA
  • Additional Rules

  • Author: Wolfgang Schreiner
    Last Modification: May 14, 1998

    [Up] [RISC-Linz] [University] [Search]