On the Logic of TLA+

Stephan Merz
TLA+ is a language intended for the high-level specification of reactive, distributed, and in particular asynchronous systems. Combining the linear-time temporal logic TLA and classical set-theory, it provides an expressive specification formalism and supports assertional verification.
© Computers and Informatics
Available as: PDF
The definition of stuttering invariance given in section 2.4 (p.11) is erroneous, since it does not identify two sequences that differ in infinitely many stuttering steps. Please refer to the article The Specification Language TLA+, which supersedes this paper.
  author = 	 {Stephan Merz},
  title = 	 {On the Logic of TLA{\textsuperscript{+}}},
  journal = 	 {Computers and Informatics},
  year = 	 2003,
  volume =       22,
  pages =	 {351--379}

Stephan Merz