{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171544,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627814"},{"type":"electronic","value":"9783540685173"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0030596","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:10:41Z","timestamp":1133417441000},"page":"189-200","source":"Crossref","is-referenced-by-count":13,"title":["Generalized quantitative temporal reasoning: An automata-theoretic approach"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"key":"15_CR1","first-page":"164","volume-title":"A Really Temporal Logic","author":"R. Alur","year":"1989","unstructured":"Alur, R., and Henzinger, T. A., A Really Temporal Logic. In Proceedings of the 30th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, New York, pp. 164\u2013169, 1989."},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science, Vol. 600","first-page":"74","volume-title":"Real Time: Theory in Practice","author":"R. Alur","year":"1982","unstructured":"Alur, R. and Henzinger, T. A., Logics and Models of Real Time: A Survey. In Real Time: Theory in Practice. J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds. Lecture Notes in Computer Science, Vol. 600. Springer-Verlag, New York, pp. 74\u2013106, 1982."},{"issue":"No.1","key":"15_CR3","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R. and Henzinger, T. A., A Really Temporal Logic. In Journal of the Association for Computing Machinery. Vol. 41, No. 1, January 1994, pp. 181\u2013204, 1994.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"15_CR4","unstructured":"Arnold, A., Finite Transition Systems: Semantics of Communicating Systems. Translated by John Plaice, Prentice Hall, 1994."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R. and Habermehl, P., Verifying Infinite State Processes with Sequential and Parallel Composition. In ACM POPL95 pp 95\u2013106.","DOI":"10.1145\/199448.199470"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R. and Habermehl, P., On The Verification Problem of Nonregular Properties for Nonregular Processes. In IEEE LICS95 pp 123\u2013133.","DOI":"10.1109\/LICS.1995.523250"},{"key":"15_CR7","unstructured":"Buchi, J. R., On a Decision Method in restricted Second Order Arithmetic, Proc. 1960 Inter. Congress on Logic, Methodology, and Philosophy of Science, pp. 1\u201311."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic, Logics of Programs Workshop, IBM Yorktown Heights, New York, Springer LNCS no. 131, pp. 52\u201371, May 1981.","DOI":"10.1007\/BFb0025774"},{"key":"15_CR9","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60915-6_3","volume-title":"Logics for Concurrency","author":"E. A. Emerson","year":"1996","unstructured":"Emerson, E. A., Automated Temporal Reasoning about Reactive Systems. In Logics for Concurrency, Faron Moller and Graham Birtwistle, Eds., Springer Verlag, Berlin, 1996, pp. 41\u2013101."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science, Vol. 531","first-page":"136","volume-title":"CAV 90: Computer-aided Verification","author":"E. A. Emerson","year":"1990","unstructured":"Emerson, E. A., Mok, A. K., Sistla, A. P., and Srinivasan, J., Quantitative Temporal Reasoning. In CAV 90: Computer-aided Verification. E. M. Clarke and R.P. Kurshan Eds. Lecture Notes in Computer Science, Vol. 531. Springer-Verlag, New York, pp. 136\u2013145, 1990."},{"key":"15_CR11","unstructured":"Emerson, E. A. and Trefler, Richard J., Generalized Quantitative Temporal Reasoning. Dept. of Computer Sciences, University of Texas at Austin, technical report TR-96-20, 1996."},{"key":"15_CR12","unstructured":"Heitmeyer, C. L., Jeffords, R.D., Labaw, B.G., A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems. In Proc. 10th Intern. Workshop on Real-Time Operating Systems and Software, May, 1993."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D. and Pnueli, A., On the Development of Reactive Systems. In Logics and Models of Concurrent Systems. K. Apt Ed. NATO Advanced Summer Institutes, Vol. F-13. Springer-Verlag, pp. 477\u2013498, 1985.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97\u2013107, Jan. 85.","DOI":"10.1145\/318593.318622"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Symbolic Model Checking: An approach to the state explosion problem. Ph.D. Thesis, Department of Computer Science, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"volume-title":"Automata on Infinite Words","year":"1985","key":"15_CR16","unstructured":"Nivat, M., and Perrin, D., Eds. Automata on Infinite Words. Springer-Verlag, Berlin, 1985."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., The Temporal Logic of Programs, 18th annual IEEE-CS Symp. on Foundations of Computer Science, pp. 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends, in Current Trends in Concurrency: Overviews and Tutorials, ed. J. W. de Bakker, W.P. de Roever, and G. Rozenberg, Springer LNCS no. 224, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"15_CR19","first-page":"195","volume":"no. 137","author":"J. P. Queille","year":"1982","unstructured":"Queille, J. P., and Sifakis, J., Specification and verification of concurrent programs in CESAR, Proc. 5th Int. Symp. Prog., Springer LNCS no. 137, pp. 195\u2013220, 1982.","journal-title":"Springer LNCS"},{"key":"15_CR20","unstructured":"Vardi, M., and Wolper, P., An Automata-theoretic Approach to Automatic Program Verification, Proc. IEEE LICS, pp. 332\u2013344, 1986."},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P., Temporal Logic Can Be More Expressive Information and Control, Vol. 56, 1983, pp. 72\u201399.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '97: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:41:32Z","timestamp":1736127692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030596"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627814","9783540685173"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0030596","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}