{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T01:42:38Z","timestamp":1706146958802},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,5,15]],"date-time":"2010-05-15T00:00:00Z","timestamp":1273881600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2010,6]]},"DOI":"10.1007\/s00236-010-0118-3","type":"journal-article","created":{"date-parts":[[2010,5,13]],"date-time":"2010-05-13T18:28:05Z","timestamp":1273775285000},"page":"251-277","source":"Crossref","is-referenced-by-count":8,"title":["On regular temporal logics with past"],"prefix":"10.1007","volume":"47","author":[{"given":"Christian","family":"Dax","sequence":"first","affiliation":[]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Lange","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,5,15]]},"reference":[{"key":"118_CR1","unstructured":"IEEE standard for Property Specification Language (PSL). IEEE Std 1850TM, Oct (2005). http:\/\/ieeexplore.ieee.org\/xpls\/abs_all.jsp?arnumber=1524461"},{"key":"118_CR2","unstructured":"IEEE standard for SystemVerilog\u2014unified hardware design, specification, and verification language. IEEE Std 1800TM, Nov (2005). http:\/\/ieeexplore.ieee.org\/xpls\/abs_all.jsp?tp=&isnumber=33132&arnumber=1560791"},{"key":"118_CR3","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: a new temporal property-specification language. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2280, pp. 296\u2013211. Springer (2002)","DOI":"10.1007\/3-540-46002-0_21"},{"key":"118_CR4","doi-asserted-by":"crossref","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Proceedings of Temporal Logic in Specification 1987. Lecture Notes in Computer Science, vol. 398, pp. 62\u201374. Springer (1989)","DOI":"10.1007\/3-540-51803-7_22"},{"key":"118_CR5","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL. Technical Report, The Prosyd Project, http:\/\/www.prosyd.org (2005)"},{"issue":"4","key":"118_CR6","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1142\/S0129054107004942","volume":"18","author":"R. Bloem","year":"2007","unstructured":"Bloem R., Cimatti A., Pill I. and Roveri M. (2007). Symbolic implementation of alternating automata. Int. J. Found. Comput. Sci. 18(4): 727\u2013743","journal-title":"Int. J. Found. Comput. Sci."},{"key":"118_CR7","doi-asserted-by":"crossref","unstructured":"Bustan, D., Havlicek, J.: Some complexity results for SystemVerilog assertions. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4144, pp. 205\u2013218. Springer (2006)","DOI":"10.1007\/11817963_21"},{"key":"118_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2404, pp. 359\u2013364. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"118_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: a modular symbolic encoding. In: Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 125\u2013133. IEEE Computer Society Press (2006)","DOI":"10.1109\/FMCAD.2006.19"},{"key":"118_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of Past LTL. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD). Lecture Notes in Computer Science, vol. 3312, pp. 245\u2013259. Springer (2004)","DOI":"10.1007\/978-3-540-30494-4_18"},{"issue":"1","key":"118_CR11","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E.M. Clarke","year":"1997","unstructured":"Clarke E.M., Grumberg O. and Hamaguchi K. (1997). Another look at LTL model checking. Form. Method Syst. Des. 10(1): 47\u201371","journal-title":"Form. Method Syst. Des."},{"key":"118_CR12","doi-asserted-by":"crossref","unstructured":"Dax, C., Klaedtke, F.: Alternation elimination by complementation. In: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Lecture Notes in Computer Science, vol. 5530, pp. 214\u2013229. Springer (2008)","DOI":"10.1007\/978-3-540-89439-1_16"},{"issue":"1","key":"118_CR13","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1006\/inco.2001.3094","volume":"174","author":"S. Demri","year":"2002","unstructured":"Demri S. and Schnoebelen P. (2002). The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1): 84\u2013103","journal-title":"Inf. Comput."},{"key":"118_CR14","first-page":"261","volume-title":"Logic and Automata: History and Perspectives, Texts in Logic and Games, vol. 2","author":"V. Diekert","year":"2007","unstructured":"Diekert V. and Gastin P. (2007). First-order definable languages. In: Flum, J., Gr\u00e4del, E. and Wilke, T. (eds) Logic and Automata: History and Perspectives, Texts in Logic and Games, vol. 2, pp 261\u2013306. Amsterdam University Press, Amsterdam"},{"key":"118_CR15","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, vol. 2747, pp. 439\u2013448. Springer (2003)","DOI":"10.1007\/978-3-540-45138-9_38"},{"key":"118_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel D., Kozen D. and Tiuryn J. (2000). Dynamic Logic. MIT Press, Cambridge"},{"issue":"1\u20133","key":"118_CR17","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"Henriksen J.G. and Thiagarajan P.S. (1999). Dynamic linear time temporal logic. Ann. Pure Appl. Logic 96(1\u20133): 187\u2013207","journal-title":"Ann. Pure Appl. Logic"},{"key":"118_CR18","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"2006","unstructured":"Hopcroft J.E., Motwani R. and Ullman J.D. (2006). Introduction to Automata Theory, Languages, and Computation. 3rd edn. Addison-Wesley, Reading","edition":"3"},{"key":"118_CR19","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Extended temporal logic revisited. In: Proceedings of the 12th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 2154, pp. 519\u2013535. Springer (2001)","DOI":"10.1007\/3-540-44685-0_35"},{"key":"118_CR20","doi-asserted-by":"crossref","unstructured":"Lange, M.: Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness. In: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 4703, pp. 90\u2013104. Springer (2007)","DOI":"10.1007\/978-3-540-74407-8_7"},{"issue":"5","key":"118_CR21","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1016\/j.ipl.2008.06.003","volume":"108","author":"M. Lange","year":"2008","unstructured":"Lange M. (2008). A purely model-theoretic proof of the exponential succinctness gap between CTL+ and CTL. Inf. Process. Lett. 108(5): 308\u2013312","journal-title":"Inf. Process. Lett."},{"key":"118_CR22","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 383\u2013392. IEEE Computer Society Press (2002)","DOI":"10.1109\/LICS.2002.1029846"},{"key":"118_CR23","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Proceedings of the Conference on Logics of Programs 1985. Lecture Notes in Computer Science, vol. 193, pp. 196\u2013218. Springer (1985)","DOI":"10.1007\/3-540-15648-8_16"},{"key":"118_CR24","first-page":"122","volume":"79","author":"N. Markey","year":"2003","unstructured":"Markey N. (2003). Temporal logic with past is exponentially more succinct. Bull. EATCS 79: 122\u2013128","journal-title":"Bull. EATCS"},{"issue":"3","key":"118_CR25","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano S. and Hayashi T. (1984). Alternating finite automata on \u03c9-words. Theor. Comput. Sci. 32(3): 321\u2013330","journal-title":"Theor. Comput. Sci."},{"key":"118_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"118_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Proceedings of the 14th International Symposium on Formal Methods (FM). Lecture Notes in Computer Science, vol. 4085, pp. 573\u2013586. Springer (2006)","DOI":"10.1007\/11813040_38"},{"key":"118_CR28","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS), pp. 319\u2013327. IEEE Computer Society Press (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"118_CR29","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez C., Leucker, M.: Regular linear temporal logic with past. In: Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 5944, pp. 295\u2013311. Springer (2010)","DOI":"10.1007\/978-3-642-11319-2_22"},{"issue":"2","key":"118_CR30","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch W.J. (1970). Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2): 177\u2013192","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"118_CR31","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0020-0190(89)90205-6","volume":"30","author":"M.Y. Vardi","year":"1989","unstructured":"Vardi M.Y. (1989). A note on the reduction of two-way automata to one-way automata. Inf. Process. Lett. 30(5): 261\u2013264","journal-title":"Inf. Process. Lett."},{"key":"118_CR32","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Proceedings of the 8th Banff Higher Order Workshop on Logics for Concurrency 1995. Lecture Notes in Computer Science, vol. 1043, pp. 238\u2013266. Springer (1996)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"118_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS), pp. 332\u2013344. IEEE Computer Society Press (1986)"},{"issue":"1\/2","key":"118_CR34","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper P. (1983). Temporal logic can be more expressive. Inf. Control 56(1\/2): 72\u201399","journal-title":"Inf. Control"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-010-0118-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-010-0118-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-010-0118-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T01:05:33Z","timestamp":1559091933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-010-0118-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,15]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["118"],"URL":"https:\/\/doi.org\/10.1007\/s00236-010-0118-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,15]]}}}