Microsoft tla

Meanwhile, Ernie Cohen had been working on reduction using Kleene algebra, obtaining elegant proofs of nice, general results for safety properties. I showed him the TLA version and my preliminary results on liveness, and we decided to collaborate. This paper is the result. We translated his more general results for safety into TLA and obtained new results for liveness properties.

The paper promises a complete proof and a more general result in a later paper. The result exists, but the later paper is unlikely ever to appear. Follow us:. Share this page:. Reduction in TLA. May View Publication. Download BibTex. View Publication Research Areas Algorithms. Back in the 50s and 60s, programmers used flowcharts.

Eventually, guided by people like Dijkstra and Hoare, we learned that pictures were a bad way to describe programs because they collapsed under the weight of complexity, producing an incomprehensible spaghetti of boxes and arrows.

In the great tradition of learning from our mistakes how to make the same mistake again, many people decided that drawing pictures was a wonderful way to specify systems. So, they devised graphical specification languages. Not wanting to be outdone, I wrote this paper to show that you can write TLA specifications by drawing pictures. It describes how to interpret as TLA formulas the typical circles and arrows with which people describe state transitions.

These diagrams represent safety properties. When I wrote the paper, I actually did think that pictures might be useful for explaining parts of specifications.