{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T08:22:33Z","timestamp":1761294153329,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,7,4]],"date-time":"2020-07-04T00:00:00Z","timestamp":1593820800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010939","name":"Pepperdine University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100010939","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Tooma Undergraduate Research Fellowship Program"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2021,5,31]]},"abstract":"<jats:p>This article surveys the linear temporal logic (LTL) literature and presents all the LTL theorems from the survey, plus many new ones, in a calculational deductive system. Calculational deductive systems, developed by Dijkstra and Scholten and extended by Gries and Schneider, are based on only four inference rules\u2014Substitution, Leibniz, Equanimity, and Transitivity. Inference rules in the older Hilbert-style systems, notably modus ponens, appear as theorems in this calculational deductive system. This article extends the calculational deductive system of Gries and Schneider to LTL, using only the same four inference rules. Although space limitations preclude giving a proof of every theorem in this article, every theorem has been proved with calculational logic.<\/jats:p>","DOI":"10.1145\/3387109","type":"journal-article","created":{"date-parts":[[2020,7,4]],"date-time":"2020-07-04T22:24:24Z","timestamp":1593901464000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A Calculational Deductive System for Linear Temporal Logic"],"prefix":"10.1145","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7493-8577","authenticated-orcid":false,"given":"J. Stanley","family":"Warford","sequence":"first","affiliation":[{"name":"Pepperdine University, Malibu, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Vega","sequence":"additional","affiliation":[{"name":"The Aerospace Corporation, El Segundo, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott M.","family":"Staley","sequence":"additional","affiliation":[{"name":"Ford Motor Company Research Labs (retired), Dearborn, MI, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,4]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00212-H"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_2_2_1","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . The MIT Press , Cambridge, MA . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press, Cambridge, MA."},{"key":"e_1_2_2_3_1","volume-title":"Principles of Concurrent and Distributed Programming","author":"Ben-Ari Mordechai","unstructured":"Mordechai Ben-Ari . 2006. Principles of Concurrent and Distributed Programming ( 2 nd ed.). Addison-Wesley Pearson , Harlow, England . Mordechai Ben-Ari. 2006. Principles of Concurrent and Distributed Programming (2nd ed.). Addison-Wesley Pearson, Harlow, England.","edition":"2"},{"key":"e_1_2_2_4_1","volume-title":"Mathematical Logic for Computer Science","author":"Ben-Ari Mordechai","unstructured":"Mordechai Ben-Ari . 2012. Mathematical Logic for Computer Science ( 3 rd ed.). Springer-Verlag , London . Mordechai Ben-Ari. 2012. Mathematical Logic for Computer Science (3rd ed.). Springer-Verlag, London.","edition":"3"},{"volume-title":"Programming in the 1990\u2019s: An Introduction to the Calculation of Programs","author":"Cohen Edward","key":"e_1_2_2_5_1","unstructured":"Edward Cohen . 1990. Programming in the 1990\u2019s: An Introduction to the Calculation of Programs . Springer-Verlag , New York . Edward Cohen. 1990. Programming in the 1990\u2019s: An Introduction to the Calculation of Programs. Springer-Verlag, New York."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/362851.362858"},{"key":"e_1_2_2_7_1","volume-title":"Scholten","author":"Dijkstra Edsger W.","year":"1990","unstructured":"Edsger W. Dijkstra and Carel S . Scholten . 1990 . Predicate Calculus and Program Semantics. Springer-Verlag , New York. Edsger W. Dijkstra and Carel S. Scholten. 1990. Predicate Calculus and Program Semantics. Springer-Verlag, New York."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19590051405"},{"volume-title":"Truth and Other Enigmas","author":"Dummett Michael A. E.","key":"e_1_2_2_9_1","unstructured":"Michael A. E. Dummett . 1978. Truth and Other Enigmas . Harvard University Press , Cambridge, MA . Michael A. E. Dummett. 1978. Truth and Other Enigmas. Harvard University Press, Cambridge, MA."},{"volume-title":"Handbook of Theoretical Computer Science (Vol. B)","author":"Emerson E. Allen","key":"e_1_2_2_10_1","unstructured":"E. Allen Emerson . 1990. Handbook of Theoretical Computer Science (Vol. B) . The MIT Press , Cambridge, MA , Chapter: \u201cTemporal and Modal Logic,\u201d 995--1072. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=114891.114907. E. Allen Emerson. 1990. Handbook of Theoretical Computer Science (Vol. B). The MIT Press, Cambridge, MA, Chapter: \u201cTemporal and Modal Logic,\u201d 995--1072. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=114891.114907."},{"volume-title":"Formal Development of Programs","author":"Feijen Wim H. H.","key":"e_1_2_2_11_1","unstructured":"Wim H. H. Feijen . 1990. Exercises in formula manipulation . In Formal Development of Programs , E. W. Dijkstra (Ed.). Addison-Wesley , Menlo Park, NJ , 139--158. Wim H. H. Feijen. 1990. Exercises in formula manipulation. In Formal Development of Programs, E. W. Dijkstra (Ed.). Addison-Wesley, Menlo Park, NJ, 139--158."},{"volume-title":"Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of His Retirement from His Professorship at the University of Kiel)","author":"Gries David","key":"e_1_2_2_12_1","unstructured":"David Gries . 1999. Monotonicity in calculational proofs . In Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of His Retirement from His Professorship at the University of Kiel) . Springer-Verlag , Berlin , 79--85. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=646005.673872. David Gries. 1999. Monotonicity in calculational proofs. In Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the Occasion of His Retirement from His Professorship at the University of Kiel). Springer-Verlag, Berlin, 79--85. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=646005.673872."},{"key":"e_1_2_2_13_1","volume-title":"Schneider","author":"Gries David","year":"1994","unstructured":"David Gries and Fred B . Schneider . 1994 . A Logical Approach to Discrete Math. Springer-Verlag , New York. David Gries and Fred B. Schneider. 1994. A Logical Approach to Discrete Math. Springer-Verlag, New York."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00198-8"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1080\/10511979508965779"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1995.12004644"},{"key":"e_1_2_2_17_1","volume-title":"Schneider","author":"Gries David","year":"1998","unstructured":"David Gries and Fred B . Schneider . 1998 . Adding the everywhere operator to propositional logic. J. Logic Comput . 8 (12 1998). David Gries and Fred B. Schneider. 1998. Adding the everywhere operator to propositional logic. J. Logic Comput. 8 (12 1998)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"G. E. Hughes and M. J. Cresswell. 1996. A New Introduction to Modal Logic. Routledge New York.  G. E. Hughes and M. J. Cresswell. 1996. A New Introduction to Modal Logic. Routledge New York.","DOI":"10.4324\/9780203290644"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/98158"},{"volume-title":"Temporal Logic and State Systems","author":"Kr\u00f6ger Fred","key":"e_1_2_2_20_1","unstructured":"Fred Kr\u00f6ger and Stephan Merz . 2008. Temporal Logic and State Systems . Springer-Verlag , Berlin . Fred Kr\u00f6ger and Stephan Merz. 2008. Temporal Logic and State Systems. Springer-Verlag, Berlin."},{"volume-title":"Specification","author":"Manna Zohar","key":"e_1_2_2_21_1","unstructured":"Zohar Manna and Amir Pnueli . 1992. The Temporal Logic of Reactive and Concurrent Systems: v. 1 , Specification . Springer-Verlag , New York . Zohar Manna and Amir Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems: v. 1, Specification. Springer-Verlag, New York."},{"volume-title":"Present and Future","author":"Prior Arthur N.","key":"e_1_2_2_22_1","unstructured":"Arthur N. Prior . 1967. Past , Present and Future . Oxford University Press . Arthur N. Prior. 1967. Past, Present and Future. Oxford University Press."},{"key":"e_1_2_2_23_1","volume-title":"Discrete Mathematics and Its Applications","author":"Rosen Kenneth H.","unstructured":"Kenneth H. Rosen . 2007. Discrete Mathematics and Its Applications ( 6 th ed.). McGraw-Hill , New York . Kenneth H. Rosen. 2007. Discrete Mathematics and Its Applications (6th ed.). McGraw-Hill, New York.","edition":"6"},{"volume-title":"On Concurrent Programming","author":"Schneider Fred B.","key":"e_1_2_2_24_1","unstructured":"Fred B. Schneider . 1997. On Concurrent Programming . Springer-Verlag , New York . Fred B. Schneider. 1997. On Concurrent Programming. Springer-Verlag, New York."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.4.623"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387109","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387109","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:33:26Z","timestamp":1750199606000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,4]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,5,31]]}},"alternative-id":["10.1145\/3387109"],"URL":"https:\/\/doi.org\/10.1145\/3387109","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"type":"print","value":"0360-0300"},{"type":"electronic","value":"1557-7341"}],"subject":[],"published":{"date-parts":[[2020,7,4]]},"assertion":[{"value":"2019-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-07-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}