SRC Technical Note 1998-005

Reduction in TLA

Ernie Cohen and Leslie Lamport

Reduction theorems allow one to deduce properties of a concurrent system specification from properties of a simpler, coarser-grained version called the reduced specification. We present reduction theorems based upon a more precise relation between the original and reduced specifications than earlier ones, permitting the use of reduction to reason about a larger class of properties. In particular, we present reduction theorems that handle general liveness properties.

Back to the SRC Technical Notes main page.

• PostScript compressed with UNIX compress -- 296 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 272 Kbytes
  
• PostScript compressed with ZIP -- 280 Kbytes
  
• PostScript -- 528 Kbytes
  
• Portable Document Format (PDF) -- 99 Kbytes