Obtaining Statistical Properties by Simulating Specs with TLC - Jack Vanlightly and Markus A. Kuppe
Channel: Markus Kuppe
Date: 2022-10-24

In this talk, we describe how simulation can be used to obtain statistical properties of
algorithms and how we can apply this technique using TLA+ with TLC in simulation mode.

Understanding the statistical properties of an algorithm are often as important as verifying its correctness. These statistics can pertain to both liveness and correctness. An example of liveness statistics are the number of protocol rounds to achieve a steady state, or the time to detect some condition. Examples of correctness are calculating the probability of a data loss event given a correlated failure.

Jack Vanlightly (@vanlightly) and Markus A. Kuppe (@lemmster)