{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:08Z","timestamp":1776333488573,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540752905","type":"print"},{"value":"9783540752929","type":"electronic"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-75292-9_20","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"291-305","source":"Crossref","is-referenced-by-count":32,"title":["Regular Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Martin","family":"Leucker","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"IEEE P1850 - Standard for PSL - Property Specification Language (September 2005)"},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1145\/512644.512660","volume-title":"POPL 1986","author":"H. Barringer","year":"1986","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986. Procs. of the 13th Annual ACM Symp. on Principles of Programming Languages, pp. 173\u2013183. ACM Press, New York (1986)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"20_CR4","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the Int\u2019l Congress on Logic Methodology and Philosophy of Science, pp. 1\u201312. Stanford University Press (1962)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"20_CR6","unstructured":"Fisman, D., Eisner, C., Havlicek, J.: Formal syntax and Semantics of PSL: Appendix B of Accellera Property Language Reference Manual, Version 1.1 (March 2004)"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(85)90225-7","volume":"38","author":"D. Harel","year":"1985","unstructured":"Harel, D., Peleg, D.: Process logic with regular formulas. Theoretical Computer Science\u00a038, 307\u2013322 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"1-3","key":"20_CR8","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"Henriksen, J.G., Thiagarajan, P.S.: Dynamic linear time temporal logic. Annals of Pure and Applied Logic\u00a096(1-3), 187\u2013207 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"20_CR9","volume-title":"Introduction to automata theory, languages and computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages and computation. Addison-Wesley, Reading (1979)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/BFb0023448","volume-title":"STACS 1997","author":"J. Hromkovic","year":"1997","unstructured":"Hromkovic, J., Seibert, S., Wilke, T.: Translating regular expressions into small \u03b5-free nondeterministic finite automata. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 55\u201366. Springer, Heidelberg (1997)"},{"key":"20_CR11","first-page":"3","volume-title":"Automata Studies","author":"S.C. Kleene","year":"1956","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, vol.\u00a034, pp. 3\u201341. Princeton University Press, Princeton, New Jersey (1956)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/BFb0012782","volume-title":"Automata, Languages, and Programming","author":"D. Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages, and Programming. LNCS, vol.\u00a0140, pp. 348\u2013359. Springer, Heidelberg (1982)"},{"key":"20_CR13","first-page":"147","volume-title":"ISTCS 1997","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: ISTCS 1997. Proc. of the Fifth Israel Symposium on Theory of Computing and Systems, pp. 147\u2013158. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-540-30579-8_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Lange","year":"2005","unstructured":"Lange, M.: Weak automata for the linear time \u03bc-calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 267\u2013281. Springer, Heidelberg (2005)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_18","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Lange","year":"2002","unstructured":"Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol.\u00a02303, Springer, Heidelberg (2002)"},{"key":"20_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Heidelberg (1995)"},{"key":"20_CR17","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Altenating automata on infinite trees. Theoretical Computer Science\u00a054, 267\u2013276 (1987)","journal-title":"Theoretical Computer Science"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/3-540-49116-3_48","volume-title":"STACS 1999","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M\u00fcller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.\u00a01563, pp. 510\u2013520. Springer, Heidelberg (1999)"},{"key":"20_CR19","first-page":"46","volume-title":"FOCS 1977","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977. Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201367. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/BFb0027047","volume-title":"Current Trends in Concurrency","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems \u2013 a survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol.\u00a0224, pp. 510\u2013584. Springer, Heidelberg (1986)"},{"issue":"3","key":"20_CR21","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear termporal logics. Journal of the ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"key":"20_CR22","unstructured":"Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, Department of Electrical Engineering, MIT, Boston, Massachusetts (1974)"},{"key":"20_CR23","unstructured":"Vardi, M.Y.: Personal communication"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"20_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"20_CR26","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\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/3-540-44968-X_45","volume-title":"Computing and Combinatorics","author":"H. Yamamoto","year":"2000","unstructured":"Yamamoto, H.: On the power of input-synchronized alternating finite automata. In: Du, D.-Z., Eades, P., Sharma, A.K., Lin, X., Estivill-Castro, V. (eds.) COCOON 2000. LNCS, vol.\u00a01858, p. 457. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T02:02:05Z","timestamp":1558490525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540752905","9783540752929"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}