Michael Fisher: An Introduction to Practical Formal Methods using Temporal Logic Michael Fisher: An Introduction to Practical Formal Methods using Temporal Logic An Introduction to Practical Formal Methods using Temporal Logic Michael Fisher Book Corrections Examples Systems Slides Videos Book The Wiley web page for the book is here. If you notice any mistakes, either in the book or in these pages, please email me. Thank you. Corrections Thanks to all those who have pointed our errors in the book: Page 273, Example A.3, missing negation. Should be ''A OR B is equivalent to NOT ((NOT A) AND (NOT B))'' Thanks to Ed Briggs for spotting this. Examples An ongoing project -- to populate this section with examples. Systems TSPASS: was developed by Michel Ludwig and is available here. A copy of the sources and binaries for version 0.94 of TSPASS is also available here. Spin: was developed at Bell Labs primarily by Gerard Holzmann and is freely available for general use from here. Concurrent MetateM: this Java implementation was developed by Anthony Hepple and is available here. A copy of the zip file for version 0.2.1 is also available here. When unzipped, this file provides the Concurrent MetateM interpreter (an archive of Java class files), documentation and a series of example agent systems. Slides Slides (in pdf form) are available below. Temporal Logic ORIGINALS NEW STYLE introduction: pdf; 4up-pdf pdf; 4up-pdf intuition: pdf; 4up-pdf pdf; 4up-pdf semantics: pdf; 4up-pdf pdf; 4up-pdf esoterica: pdf; 4up-pdf pdf; 4up-pdf Temporal Specification programs: pdf; 4up-pdf. semantics: pdf; 4up-pdf. concurrency: pdf; 4up-pdf. communication: pdf; 4up-pdf. case studies: pdf; 4up-pdf. exercises: pdf; 4up-pdf. esoterica: pdf; 4up-pdf. Temporal Resolution resolution: pdf; 4up-pdf. normal form: pdf; 4up-pdf. loop search: pdf; 4up-pdf. simplification: pdf; 4up-pdf. TSPASS: pdf; 4up-pdf. Model Checking -- not yet available. Executable Temporal Specification -- not yet available. implementation: pdf; 4up-pdf. METATEM: pdf; 4up-pdf. Concurrent METATEM: implementing the METATEM approach, bringing in deliberation, concurrency, and multi-agent systems Advanced: Videos An ongoing project -- to populate this page with videos. About this document ... An Introduction to Practical Formal Methods using Temporal Logic This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71) Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds. Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney. The command line arguments were: latex2html -no_subdir -no_navigation -split 1 -address MFisher@liverpool.ac.uk -t 'Michael Fisher: An Introduction to Practical Formal Methods using Temporal Logic' index.tex The translation was initiated by Michael Fisher on 2015-01-30 MFisher@liverpool.ac.uk
