A More Complete TLA

Stephan Merz

Abstract

This paper defines a generalization of Lamport's Temporal Logic of Actions. We prove that our logic is stuttering-invariant and give an axiomatization of its propositional fragment. We also show that standard TLA is as expressive as our extension once quantification over flexible propositions is added.

© Springer-Verlag

Available as:  gzip'ed Postscript  (full version with proofs)

Reference

@InProceedings{merz:complete-tla,
  author = 	 {Stephan Merz},
  title = 	 {A More Complete {TLA}},
  booktitle = 	 {FM'99: World Congress on Formal Methods},
  pages =	 {1226--1244},
  year =	 1999,
  editor =	 {J.M. Wing and J. Woodcock and J. Davies},
  volume =	 1709,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Toulouse, France},
  month =	 sep,
  publisher =	 {Springer-Verlag}
}