The Temporal Logic of Actions I

Wolfgang Schreiner
Research Institute for Symbolic Computation
Johannes Kepler University, 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
  • References

  • Wolfgang.Schreiner@risc.uni-linz.ac.at
    Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine