{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T04:50:17Z","timestamp":1648788617655},"publisher-location":"Berlin, Heidelberg","reference-count":60,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540518037","type":"print"},{"value":"9783540468110","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51803-7_23","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:16:08Z","timestamp":1330204568000},"page":"75-123","source":"Crossref","is-referenced-by-count":30,"title":["On the relation of programs and computations to models of temporal logic"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Wolper","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,25]]},"reference":[{"key":"5_CR1","unstructured":"S. Aggarwal, C. Courcoubetis, P. Wolper, \u201cAdding Liveness Properties to Coupled Finite-State Machines\u201d, to appear."},{"key":"5_CR2","unstructured":"B. Alpern, F. Schneider, \u201cVerifying Temporal Properties Without Using Temporal Logic\u201d, Technical Report TR 85-723, Dept. of Computer Science, Cornell University, December 1985."},{"key":"5_CR3","unstructured":"B. Alpern, F. Schneider, \u201cProving Boolean Combinations of Deterministic Properties\u201d, Proc. Symp. on Logic in Computer Science, Ithaca, June 1987, pp. 131\u2013137."},{"key":"5_CR4","unstructured":"M. Ben-Ari, Z. Manna, A. Pnueli, \u201cThe Logic of Nexttime\u201d, Eighth ACM Symposium on Principles of Programming Languages, Williamsburg, January 1981, pp. 164\u2013176."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, A. Pnueli, \u201cNow You May Compose Temporal Logic Specifications\u201d, Proc. 16th ACM Symp. on Theory of Computing, Washington, April 1984, pp. 51\u201363.","DOI":"10.1145\/800057.808665"},{"key":"5_CR6","first-page":"207","volume-title":"Proceedings of the IFIP Working Conference \u201cThe Role of Abstract Models in Information Processing","author":"H. Barringer","year":"1985","unstructured":"H. Barringer, R. Kuiper, A. Pnueli. \u201cA Compositional Temporal Approach to a CSP-like Language\u201d, Proceedings of the IFIP Working Conference \u201cThe Role of Abstract Models in Information Processing\u201d, E.J. Neuhold and G. Chroust, editors, North Holland, Vienna, 1985, pp. 207\u2013227."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, A. Pnueli, \u201cA Really Abstract Concurrent Model and its Temporal Logic\u201d, Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, St. Petersberg Beach, Florida, January 1986, pp. 173\u2013183.","DOI":"10.1145\/512644.512660"},{"key":"5_CR8","unstructured":"J. R. B\u00fcchi, \u201cOn a Decision Method in Restricted Second Order Arithmetic\u201d, Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, Stanford University Press, 1962, pp. 1\u201312."},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Synthesis of Synchronization Skeletons from Branching Time Temporal Logic","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke, E. A. Emerson, \u201cSynthesis of Synchronization Skeletons from Branching Time Temporal Logic\u201d, Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, NY, Lecture Notes in Computer Science vol. 131, Springer-Verlag, Berlin, 1982, pp. 52\u201371."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, A. P. Sistla, \u201cAutomatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications: A Practical Approach\u201d, Proc. of the 10th ACM Symposium on Principles of Programming Languages, Austin, January 1984, pp. 117\u2013126.","DOI":"10.1145\/567067.567080"},{"issue":"2","key":"5_CR11","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, A. P. Sistla, \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications\u201d, ACM Transactions on Programming Languages and Systems, vol. 8, no. 2 (1986), pp. 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, M.C. Browne, \u201cReasoning about Networks with Many Identical Finite-State Processes\u201d, Proc. 5th ACM Symp. on Principles of Distributed Computing, Minaki, Ontario, August 1985, pp. 240\u2013248.","DOI":"10.1145\/10590.10611"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, M. Y. Vardi, P. Wolper, \u201cReasoning about Fair Concurrent Programs\u201d, Proc. 18th Symp. on Theory of Computing, Berkeley, May 1986, pp. 283\u2013294.","DOI":"10.1145\/12130.12159"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"E. A. Emerson, E. M. Clarke, \u201cUsing Banching Time Logic to Synthesize Synchronization Skeletons\u201d, Science of Computer Programming, 2 (1982), pp. 241\u2013266.","journal-title":"Science of Computer Programming"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E. A. Emerson","year":"1985","unstructured":"E. A. Emerson, J. Y. Halpern, \u201cDecision Procedures and Expressiveness in the Temporal Logic of Branching Time\u201d, Journal of Computer and System Sciences, 30 (1985), pp. 1\u201324.","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"5_CR16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E.A. Emerson, J.Y. Halpern, \u201c\u201cSometimes\u201d and \u201cNot Never\u201d Revisited: On Branching versus Linear Time Temporal Logic\u201d, Journal of the ACM, vol. 33, no. 1 (1986), pp. 151\u2013178.","journal-title":"Journal of the ACM"},{"key":"5_CR17","unstructured":"E. A. Emerson, Ching-Laung Lei, \u201cTemporal Model Checking under Generalized Fairness Constraints\u201d, Proc. 18th Hawaii International Conference on System Sciences, 1985."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, Ching-Laung Lei, \u201cModalities for Model Checking: Branching Time Strikes Back\u201d, Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985, pp. 84\u201396.","DOI":"10.1145\/318593.318620"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, \u201cAutomata, Tableaux and Temporal Logics\u201d, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 79\u201388.","DOI":"10.1007\/3-540-15648-8_7"},{"key":"5_CR20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E. A. Emerson","year":"1984","unstructured":"E. A. Emerson, A. P. Sistla, \u201cDeciding Branching Time Logic\u201d, Information and Control, 61 (1984), pp. 175\u2013201.","journal-title":"Information and Control"},{"key":"5_CR21","doi-asserted-by":"crossref","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"N. Francez, Fairness, Springer-Verlag, Berlin, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, \u201cThe Temporal Analysis of Fairness\u201d, Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, January 1980, pp. 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. 10th International Colloquium on Automata Languages and Programming","author":"J. Halpern","year":"1983","unstructured":"J. Halpern, Z. Manna, B. Moszkowski, \u201cA Hardware Semantics Based on Temporal Intervals\u201d, Proc. 10th International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 154, Springer-Verlag, Berlin, 1983."},{"key":"5_CR24","unstructured":"Y. Kornatsky, S. S. Pinter, \u201cA Model Checker for Partial Order Temporal Logic\u201d, EE PUB no. 597, Department of Electrical Enginering, Technion-Israel Institute of Technology, June 1986."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"S. Katz, D. Peled, \u201cInterleaving Set Temporal Logic\u201d, Proc. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, August 1987, pp. 178\u2013190.","DOI":"10.1145\/41840.41855"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"L. Lamport, \u201cSometimes is Sometimes Not Never\u201d, Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV, January 1980, pp. 174\u2013185.","DOI":"10.1145\/567446.567463"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, \u201cChecking that Finite State Concurrent Programs Satisfy their Linear Specifications\u201d, Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, L. Zuck, \u201cThe Glory of the Past\u201d, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 196\u2013218.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner, \u201cA Calculus of Communicating Systems\u201d, Lecture Notes in Computer Science, vol. 92, Springer-Verlag, Berlin, 1980."},{"key":"5_CR30","unstructured":"B. Moszkowski, \u201cReasoning about Digital Circuits\u201d, Ph.D. Thesis, Department of Computer Science, Stanford University, July 1983."},{"key":"5_CR31","series-title":"International Lecture Series in Computer Science","first-page":"215","volume-title":"The Correctness Problem in Computer Science","author":"Z. Manna","year":"1981","unstructured":"Z. Manna, A. Pnueli, \u201cVerification of Concurrent Programs: the Temporal Framework\u201d, The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, eds., International Lecture Series in Computer Science, Academic Press, London, 1981, pp. 215\u2013273."},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, \u201cHow to Cook a Temporal Proof System for your Pet Language, Proc. of the 10th ACM Symposium on Principles of Programming Languages, Austin, January 1984, pp. 141\u2013154.","DOI":"10.1145\/567067.567082"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/BFb0036932","volume-title":"Proc. 10th International Colloquium on Automata Languages and Programming","author":"Z. Manna","year":"1983","unstructured":"Z. Manna, A. Pnueli, \u201cProving Properties: the Temporal Way\u201d, Proc. 10th International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 154, Springer-Verlag, Berlin, 1983, pp. 491\u2013512."},{"key":"5_CR34","unstructured":"Z. Manna, A. Pnueli, \u201cVerification of Concurrent Programs: A Temporal Proof System\u201d, Foundations of Computer Science IV, J. W. deBakker, J. Van Leeuwen, Eds., Mathematical Center Tracts, vol. 159, Amsterdam, 1983, pp. 163\u2013225."},{"key":"5_CR35","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna, A. Pnueli, \u201cAdequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs\u201d, Science of Computer Programming, 4 (1984), pp. 257\u2013289.","journal-title":"Science of Computer Programming"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, \u201cSpecification and Verification of Concurrent Programs by \u2200-Automata\u201d, Proc. 14th ACM Symp. on Principles of Programming Languages, Munich, January 1987, pp. 1\u201312.","DOI":"10.1145\/41625.41626"},{"issue":"1","key":"5_CR37","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna, P. Wolper, \u201cSynthesis of Communicating Processes from Temporal Logic Specifications\u201d, ACM Transactions on Programming Languages and Systems, vol. 6, no. 1, January 1984, pp. 68\u201393.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"V. Nguyen, D. Gries, S. Owicki, \u201cA Model and Temporal Proof System for Networks of Processes\u201d, Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, January 1985, pp. 121\u2013131.","DOI":"10.1145\/318593.318624"},{"issue":"3","key":"5_CR39","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki, L. Lamport, \u201cProving Liveness Properties of Concurrent Programs\u201d, ACM Transactions on Programming Languages and Systems, vol. 4, no. 3, 1982, pp. 455\u2013496.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cThe Temporal Logic of Programs\u201d, Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, November 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR41","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, \u201cThe Temporal Logic of Concurrent Programs\u201d, Theoretical Computer Science, 13(1981), pp. 45\u201360.","journal-title":"Theoretical Computer Science"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"V. R. Pratt, \u201cOn the Composition of Processes\u201d, Ninth Symposium on Principles of Programming Languages, Albuquerque, January 1982, pp. 213\u2013223.","DOI":"10.1145\/582153.582177"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"S.S. Pinter, P. Wolper, \u201cA Temporal Logic for Reasoning about Partially Ordered Computations\u201d, Proc. 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, August 1984, pp. 28\u201337.","DOI":"10.1145\/800222.806733"},{"key":"5_CR44","unstructured":"A. Pnueli, L. Zuck, \u201cProbabilistic Verification by Tableaux\u201d, Proc. Symp. on Logic in computer Science, Cambridge, June 1986, pp. 322\u2013331."},{"key":"5_CR45","first-page":"1","volume":"141","author":"M. O. Rabin","year":"1969","unstructured":"M. O. Rabin, \u201cDecidability of Second Order Theories and Automata on Infinite Trees\u201d, Transactions of American Mathematical Society, vol. 141, July 1969, pp. 1\u201335.","journal-title":"Transactions of American Mathematical Society"},{"key":"5_CR46","first-page":"1","volume-title":"Proc. Symp. on Mathematical Logic and Foundations of Set Theory","author":"M. O. Rabin","year":"1970","unstructured":"M. O. Rabin, \u201cWeakly Definable Relations and Special Automata\u201d, Proc. Symp. on Mathematical Logic and Foundations of Set Theory, Y. Bar-Hillel, ed., North Holland, Amsterdam, 1970, pp. 1\u201323."},{"key":"5_CR47","volume-title":"Theoretical Issues in the Design and Verification of Distributed Systems","author":"A. P. Sistla","year":"1983","unstructured":"A.P. Sistla, \u201cTheoretical Issues in the Design and Verification of Distributed Systems\u201d, PhD thesis, Harvard University, Harvard, 1983."},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"A. P. Sistla, E. M. Clarke, \u201cThe Complexity of Propositional Linear Temporal Logic\u201d, Proceedings of the 14th ACM Symposium on Theory of Computing, San Francisco, CA, May 1982, pp. 159\u2013168.","DOI":"10.1145\/800070.802189"},{"issue":"3","key":"5_CR49","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla, E. M. Clarke, \u201cThe Complexity of Propositional Linear Temporal Logics\u201d, Journal of the ACM, vol. 32, no. 3, July 1985, pp. 733\u2013749.","journal-title":"Journal of the ACM"},{"key":"5_CR50","doi-asserted-by":"crossref","unstructured":"R. L. Schwartz, P. M. Melliar-Smith, F. H. Vogt, \u201cAn Interval Logic for Higher-Level Temporal Reasoning\u201d, Proc. 2nd ACM Symposium on Principles of Distributed Computing, Montreal, Canada, August 1983, pp. 173\u2013186.","DOI":"10.1145\/800221.806720"},{"key":"5_CR51","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. P. Sistla","year":"1987","unstructured":"A. P. Sistla, M. Y. Vardi, P. Wolper, \u201cThe Complementation Problem for B\u00fcchi Automata with Applications to Temporal Logic\u201d, Theoretical Computer Science, 49 (1987), pp. 217\u2013237.","journal-title":"Theoretical Computer Science"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"M. Vardi, \u201cAutomatic Verification of Probabilistic Concurrent Finite-State Programs\u201d, Proc. 26th Symp. on Foundations of Computer Science, Portland, October 1985, pp. 327\u2013338.","DOI":"10.1109\/SFCS.1985.12"},{"key":"5_CR53","doi-asserted-by":"crossref","unstructured":"M. Vardi, The Taming of Converse: Reasoning about Two-Way Computations\u201d, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 413\u2013424.","DOI":"10.1007\/3-540-15648-8_31"},{"key":"5_CR54","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi, L. Stockmeyer, \u201cImproved Upper and Lower Bounds for Modal Logics of Programs\u201d, Proc. 17th ACM Symp. on Theory of Computing, Providence, May 1985, pp. 240\u2013251.","DOI":"10.1145\/22145.22173"},{"issue":"2","key":"5_CR55","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"M. Y. Vardi, P. Wolper, \u201cAutomata-Theoretic Techniques for Modal Logics of Programs\u201d, Journal of Computer and System Science, vol. 32, no. 2 (April 1986), pp. 183\u201321.","journal-title":"Journal of Computer and System Science"},{"key":"5_CR56","unstructured":"M. Y. Vardi, P. Wolper, \u201cAn Automata-Theoretic Approach To Automatic Program Verification\u201d, Proc. Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 322\u2013331."},{"key":"5_CR57","unstructured":"M. Y. Vardi, P. Wolper, \u201cReasoning about Infinite Computation Paths\u201d, to appear."},{"key":"5_CR58","unstructured":"P. Wolper, \u201cSynthesis of Communicating Processes from Temporal Logic Specifications\u201d, Ph.D. Thesis, Stanford University, August 1982."},{"issue":"1\u20132","key":"5_CR59","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper, \u201cTemporal Logic Can Be More Expressive\u201d, Information and Control, vol. 56, nos. 1\u20132, 1983, pp. 72\u201399.","journal-title":"Information and Control"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"P. Wolper, M. Y. Vardi, A. P. Sistla, \u201cReasoning about Infinite Computation Paths\u201d, Proc. 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983, pp. 185\u2013194.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Temporal Logic in Specification","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51803-7_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:22:50Z","timestamp":1605648170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51803-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540518037","9783540468110"],"references-count":60,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-51803-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1989]]}}}