A TLA Solution to the RPC-Memory Specification Problem

Since the problem posed in [114] was devised by both Broy and me, I felt it was reasonable for me to present a TLA solution. Martín Abadi, Stephan Merz, and I worked out a solution that Merz and I presented at the workshop. Afterwards, we worked some more on it and finally came up with a more elegant approach that is described in this paper. I believe that Abadi and I wrote most of the prose. Merz wrote the actual proofs, which he later checked using his embedding of TLA in Isabelle. We all contributed to the writing of the specifications.

This is the only example I’ve encountered in which the pictures of TLA formulas described in [113] were of some use. In fact, I discovered the error in [113] when I realized that one of the pictures in this paper provided a counterexample to its incorrect theorem.