{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:05:48Z","timestamp":1737435948328,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432838"},{"type":"electronic","value":"9783540458418"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45841-7_37","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T08:11:17Z","timestamp":1186906277000},"page":"455-464","source":"Crossref","is-referenced-by-count":1,"title":["Nesting Until and Since in Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Denis","family":"Th\u00e9rien","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Wilke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,21]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"Jorge Almeida. Finite Semigroups and Universal Algebra, volume 3 of Series in Algebra. World Scientific, Singapore, 1995.","DOI":"10.1142\/2481"},{"issue":"2","key":"37_CR2","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1142\/S021819679600009X","volume":"6","author":"J. Almeida","year":"1996","unstructured":"Jorge Almeida. A syntactical proof of locality of DA. Internat. J. Algebra and Comput., 6(2):165\u2013177, 1996.","journal-title":"Internat. J. Algebra and Comput."},{"key":"37_CR3","unstructured":"Jo\u00eblle Cohen-Chesnot. Etude alg\u00e9brique de la logique temporelle. Doctoral thesis, Universit\u00e9 Paris 6, Paris, France, April 1989."},{"issue":"3","key":"37_CR4","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0022-0000(93)90005-H","volume":"46","author":"J. Cohen","year":"1993","unstructured":"Jo\u00eblle Cohen, Dominique Perrin, and Jean-Eric Pin. On the expressive power of temporal logic. J. Comput. System Sci., 46(3):271\u2013294, June 1993.","journal-title":"J. Comput. System Sci."},{"key":"37_CR5","volume-title":"Pure and Applied Mathematics","author":"S. Eilenberg","year":"1976","unstructured":"Samuel Eilenberg. Automata, Languages, and Machines, volume 59-B of Pure and Applied Mathematics. Academic Press, New York, 1976."},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"Allen E. Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, pages 995\u20131072. Elsevier Science Publishers B. V., Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. In Proceedings 12th Annual IEEE Symposium on Logic in Computer Science, pages 228\u2013235, Warsaw, Poland, 1997.","DOI":"10.1109\/LICS.1997.614950"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Kousha Etessami and Thomas Wilke. An until hierarchy for temporal logic. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 108\u2013117, New Brunswick, N. J., 1996.","DOI":"10.1109\/LICS.1996.561310"},{"key":"37_CR9","unstructured":"Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, Calif., 1968."},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"Fred Kr\u00f6ger. Temporal Logic of Programs. Springer, 1987.","DOI":"10.1007\/978-3-642-71549-5"},{"issue":"2","key":"37_CR11","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"Leslie Lamport. Specifying concurrent program modules. ACMT rans. Programming Lang. Sys., 5(2):190\u2013222, 1983.","journal-title":"ACMT rans. Programming Lang. Sys."},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"Zohar Manna, Anuchit Anuchitanukul, Nikolaj Bj\u00f8rner, Anca Browne, Edward Chang, Michael Col\u00f3n, Luca de Alfaro, Harish Devarajan, Henny Sipma, and Tomas Uribe. STeP: the Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Computer Science, Stanford University, Stanford, Calif., 1994.","DOI":"10.21236\/ADA324036"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, pages 46\u201357, Rhode Island, Providence, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"37_CR14","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0022-4049(98)00126-1","volume":"142","author":"B. Steinberg","year":"1999","unstructured":"Ben Steinberg. Semidirect products of categories and applications. Journal of Pure and Applied Algebra, 142:153\u2013182, 1999.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"37_CR15","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0022-4049(85)90062-3","volume":"36","author":"H. Straubing","year":"1985","unstructured":"Howard Straubing. Finite semigroup varieties of the form V.D. J. Pure Appl. Algebra, 36:53\u201394, 1985.","journal-title":"J. Pure Appl. Algebra"},{"key":"37_CR16","unstructured":"A. Prasad Sistla and Lenore D. Zuck. On the eventuality operator in temporal logic. In Proceedings, Symposium on Logic in Computer Science, pages 153\u2013166, Ithaca, New York, June 1987."},{"issue":"2","key":"37_CR17","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1993.1006","volume":"102","author":"A. P. Sistla","year":"1993","unstructured":"A. Prasad Sistla and Lenore D. Zuck. Reasoning in a restricted temporal logic. Inform. and Computation, 102(2):167\u2013195, February 1993.","journal-title":"Inform. and Computation"},{"key":"37_CR18","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0022-4049(91)90119-M","volume":"74","author":"D. Th\u00e9rien","year":"1991","unstructured":"Denis Th\u00e9rien. Two-sided wreath product of categories. Journal of Pure and Applied Algebra, 74:307\u2013315, 1991.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"Denis Th\u00e9rien and Thomas Wilke. Temporal logic and semidirect products: An effective characterization of the until hierarchy. In Proceedings of the 37th Annual Symposium on Foundations of Computer Science, pages 256\u2013263, Burlington, Vermont, 1996.","DOI":"10.1109\/SFCS.1996.548484"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Denis Th\u00e9rien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation: FO2 = \u22112\u2229\u220f2. In Proceedings of the Thirtieth Annual ACMSymp osium on Theory of Computing, pages 41\u201347, Dallas, Texas, May 1998.","DOI":"10.1145\/276698.276749"},{"key":"37_CR21","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0022-4049(87)90108-3","volume":"48","author":"B. Tilson","year":"1987","unstructured":"Brat Tilson. Categories as algebra. J. Pure Appl. Algebra, 48:83\u2013198, 1987.","journal-title":"J. Pure Appl. Algebra"}],"container-title":["Lecture Notes in Computer Science","STACS 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45841-7_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:55:48Z","timestamp":1737363348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45841-7_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432838","9783540458418"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45841-7_37","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}