{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:23Z","timestamp":1725542963625},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_22","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"295-311","source":"Crossref","is-referenced-by-count":9,"title":["Regular Linear Temporal Logic with Past"],"prefix":"10.1007","author":[{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"first","affiliation":[]},{"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986 (1986)","DOI":"10.1145\/512644.512660"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11901433_41","volume-title":"Formal Methods and Software Engineering","author":"A. Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Streit, J.: SALT\u2014structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 757\u2013775. Springer, Heidelberg (2006)"},{"key":"22_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, p. 363. Springer, Heidelberg (2001)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 191\u2013206. Springer, Heidelberg (2005)"},{"key":"22_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-89439-1_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Dax","year":"2008","unstructured":"Dax, C., Klaedtke, F.: Alternation elimination by complementation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 214\u2013229. Springer, Heidelberg (2008)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"A. Emerson","year":"1980","unstructured":"Emerson, A., Clarke, E.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085. Springer, Heidelberg (1980)"},{"key":"22_CR7","unstructured":"Fisman, D., Eisner, C., Havlicek, J.: Formal syntax and Semantics of PSL: Appendix B of Accellera Property Language Reference Manual, Version 1.1. (2004)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: POPL 1980 (1980)","DOI":"10.1145\/567446.567462"},{"key":"22_CR9","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. TCS\u00a038, 307\u2013322 (1985)","journal-title":"TCS"},{"issue":"1-3","key":"22_CR10","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J. Henriksen","year":"1999","unstructured":"Henriksen, J., 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":"22_CR11","volume-title":"Introduction to automata theory, languages and computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Ullman, J.: Introduction to automata theory, languages and computation. Addison-Wesley, Reading (1979)"},{"key":"22_CR12","unstructured":"Kamp, H.: Tense Logic and the Theory of Linear Order. PhD thesis, UCLA (1968)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) ICALP 1982. LNCS, vol.\u00a0140. Springer, Heidelberg (1982)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/3-540-44685-0_35","volume-title":"CONCUR 2001 - Concurrency Theory","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Piterman, N., Vardi, M.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, p. 519. Springer, Heidelberg (2001)"},{"key":"22_CR15","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":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-74407-8_7","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"M. Lange","year":"2007","unstructured":"Lange, M.: Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 90\u2013104. Springer, Heidelberg (2007)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, Ph.: Temporal logic with forgettable past. In: LICS 2002 (2002)","DOI":"10.1109\/LICS.2002.1029846"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-75292-9_20","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"M. Leucker","year":"2007","unstructured":"Leucker, M., S\u00e1nchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 291\u2013305. Springer, Heidelberg (2007)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193. Springer, Heidelberg (1985)"},{"key":"22_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verif. of Reactive Systems","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verif. of Reactive Systems. Springer, Heidelberg (1995)"},{"key":"22_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. Muller","year":"1987","unstructured":"Muller, D., Schupp, P.: Altenating automata on infinite trees. TCS\u00a054, 267\u2013276 (1987)","journal-title":"TCS"},{"key":"22_CR22","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 99","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":"22_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"22_CR24","volume-title":"Logics and models of concurrent systems, NATO ASI F-13","author":"A. Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, NATO ASI F-13. Springer, Heidelberg (1985)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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\u2013a survey of current trends. In: Current Trends in Concurrency. LNCS, vol.\u00a0224. Springer, Heidelberg (1986)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A. Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 573\u2013586. Springer, Heidelberg (2006)"},{"key":"22_CR27","unstructured":"Schnoebelen, Ph.: The complexity of temporal logic model checking. In: AiML 2002 (2002)"},{"issue":"3","key":"22_CR28","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.: The complexity of propositional linear termporal logics. JACM\u00a032(3), 733\u2013749 (1985)","journal-title":"JACM"},{"key":"22_CR29","unstructured":"Stockmeyer, L.: The Computational Complexity of Word Problems. PhD thesis. MIT (1974)"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Logics for Concurrency","author":"M. Vardi","year":"1996","unstructured":"Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043. Springer, Heidelberg (1996)"},{"key":"22_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf.\u00a0Comp.\u00a0115, 1\u201337 (1994)","journal-title":"Inf.\u00a0Comp."},{"key":"22_CR32","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. Info.& Control\u00a056, 72\u201399 (1983)","journal-title":"Info.& Control"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:39:29Z","timestamp":1606185569000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}