Dear Daniel Leivant, My experience shows that it is best to use Leslie’s hyperbook as the primary starting source and add (more!) theoretical background as appropriate for a possibly required understanding of related notations and/or concepts. Students tend to appreciate machine support for “thinking” quite a bit! Another issue is the application background. The level of the “informal” understanding of the concepts of e. g. distributed systems is key before entering “formal” descriptions of it. All the best Fritz Von: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx] Im Auftrag von Stephan Merz Dear Daniel Leivant, Leslie's hyperbook is an obvious source for many ideas for such a course, it is essentially a tutorial: http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html. I have occasionally given TLA courses at summer schools, and I'll send you a set of slides off-list. For a description that focuses more on the logic of TLA, you may find some material in http://www.loria.fr/~merz/papers/tla+logic2008.html. The TLA+ distribution comes with a set of a few examples for the use of the model checker. I'm not sure if these are part of the TLA+ Toolbox distribution of TLC, but they are (or at least used to be) part of the standalone (command-line) tools available from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html#downloading. Best regards, Stephan On 16 Dec 2013, at 18:04, Daniel Leivant <lei...@xxxxxxxxxxxxxx> wrote: I plan to incorporate next semester an introduction to TLA (and temporal logic) into a graduate introductory course on formal logic and program verification. -- -- |