Just uploaded my seminar paper on PLTL Model Checking toghether with the slides. The paper and the slides are in german, and cover the basics of Model Checking using Propositional Linear Temporal Logic (PLTL).