On TLA as a logic

Martín Abadi, Stephan Merz

Abstract

We describe the Temporal Logic of Actions (TLA) from a logical perspective. After giving the syntax and semantics of TLA, we discuss some methods for representing reactive systems in TLA and study verification rules.

Available as:  gzip'ed Postscript 

Reference

@InCollection{abadi:marktoberdorf,
  author =    "Mart\'{\i}n Abadi and Stephan Merz",
  title =     "On {TLA} as a Logic",
  booktitle = "Deductive Program Design",
  publisher = "Springer-Verlag",
  year =      1996,
  editor =    "Manfred Broy",
  series =    "{NATO} {ASI} series {F}",
  address =   "Berlin",
  pages =     "235--272"
}