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.