Pepperdine Papers on Linear Temporal Logic

This book Pepperdine Papers on Linear Temporal Logic documents the research conducted over many years at Pepperdine University culminating in the recent publication of: J. Stanley Warford David Vega and Scott M. Staley. 2020. A Calculational Deductive System for Linear Temporal Logic. ACM Comput. Surv. 53 3 Article 53 (June 2020) 38 pages https: //doi.org/10.1145/3387109 which is freely available for download from the link given above. This book was written with three goals in mind. First to make the complete documentation of this work widely accessible to engineers and scientists working in this and related fields. Due to publication page limitations only a small sample of the results of this work could be published in the ACM Computing Surveys article. Second to update the reader on additional new results that were completed subsequent to the submission of the article to the peer-review process. And third to report on related supporting work that was conducted using the automated theorem proving software ACL2 to confirm a significant number of the calculational proofs. Our hope is that together the ACM article and this book can be a significant resource for students and researchers working on LTL specification of reactive and concurrent systems. The audience for this book Pepperdine Papers on Linear Temporal Logic includes university students at the undergraduate and graduate levels in computer science mathematics software engineering and systems design. This book may also be of interest to practicing professionals and educators in both industry and academia.