Reasoning about TLA Actions

Download: PDF.

“Reasoning about TLA Actions” by Carlos Pacheco. The University of Texas at Austin technical report TR01-16, May 2001. Undergraduate honors thesis.

Abstract

We use the ACL2 theorem prover to verify invariants of a distributed algorithm specified in TLA (Temporal Logic of Actions). The algorithm, Disk Synod, achieves consensus among a set of processors communicating through disks. We discuss the translation of TLA specifications into a finite set theory framework in ACL2, as well as the proof of two invariant properties of Disk Synod.

Download: PDF.

BibTeX entry:

@techreport{PachecoTh2001,
   author = {Carlos Pacheco},
   title = {Reasoning about TLA Actions},
   institution = {The University of Texas at Austin},
   number = {TR01-16},
   month = may,
   year = {2001},
   note = {Undergraduate honors thesis}
}