161 / 1971-01-01 00:00:00

A Case Study In The Use Of Model Checking To Solve A Mathematical Problem

5275

TLA is a specification language for describing and reasoning about asynchronous, nondeterministic, concurrent systems. It is based on standard set theory and temporal logic. In this paper, we present how to write TLA language to specify a mathematical problem and extend it to the generalization, then use the Toolbox to check the property we want, and from the counter example of the results to get the solution.