Animating TLA Specifications

Yassine Mokhtari, Stephan Merz

Abstract

TLA (the Temporal Logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, with the intent to facilitate the communication between domain and solution experts in the design of reactive systems.

© Springer-Verlag

Available as:  gzip'ed Postscript 

Reference

@inproceedings{mokhtari:animating,
  author="Yassine Mokhtari and Stephan Merz",
  title="Animating {TLA} Specifications",
  booktitle="6th International Conference on
             Logic for Programming and Automated Reasoning (LPAR'99)",
  editors = "Harald Ganzinger and David McAllester and Andrei Voronkov",
  publisher="Springer-Verlag",
  address="Tbilisi, Georgia",
  series="Lecture Notes in Computer Science",
  volume=1705,
  year=1999,
  pages="92--110"
}