{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:57:22Z","timestamp":1759147042847},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_5","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:28:09Z","timestamp":1184588889000},"page":"62-76","source":"Crossref","is-referenced-by-count":10,"title":["First Order Linear Temporal Logic over Finite Time Structures"],"prefix":"10.1007","author":[{"given":"Serenella","family":"Cerrito","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta Cialdea","family":"Mayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Praud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"65","author":"M. Abadi","year":"1989","unstructured":"M. Abadi. The power of temporal proofs. Theoretical Computer Science, 65:35\u201383, 1989.","journal-title":"Theoretical Computer Science"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M. Abadi","year":"1990","unstructured":"M. Abadi and Z. Manna. Nonclausal deduction in first-order temporal logic. Journal of the Association for Computing Machinery, 37:279\u2013317, 1990.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"S. Abiteboul, L. Herr, and J. Van den Bussche. Temporal versus first-order logic to query temporal databases. In Proc. of the 15th Int. Conf. on Principles of Databases (PODS\u201996), 1996.","DOI":"10.1145\/237661.237674"},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness","author":"H. Barringer","year":"1989","unstructured":"H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens. MetateM: a framework for programming in temporal logic. In Proc. of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS. Springer, 1989."},{"key":"5_CR5","unstructured":"V. Benzaken, S. Cerrito, and S. Praud. V\u00e9rification statique de contraintes d\u2019int\u00e9grit\u00e9 dynamiques. In Proc. of 15\u00e8mes Journ\u00e9es Bases de Donn\u00e9es Avanc\u00e9es (BDA99), Bordeaux, France, October 1999. To appear."},{"issue":"190","key":"5_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/S0304-3975(97)00088-1","volume":"2","author":"N. Bidoit","year":"1998","unstructured":"N Bidoit and S. De Amo. A first step towards implementing dynamic algebraic dependencies. Theoretical Computer Science, 2(190):115\u2013149, january 1998.","journal-title":"Theoretical Computer Science"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"S. Cerrito and M. Cialdea Mayer. Bounded model search in linear temporal logic and its application to planning. In H. De Swart, editor, International Conference on Automated Reasoning with Analytical Tableaux and Related Methods, pages 124\u2013140. Springer, 1998.","DOI":"10.1007\/3-540-69778-0_18"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"S. Cerrito and M. Cialdea Mayer. Using linear temporal logic to model and solve planning problems. In F. Giunghiglia, editor, Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA\u2019 98), pages 141\u2013152. Springer Verlag, 1998.","DOI":"10.1007\/BFb0057441"},{"key":"5_CR9","unstructured":"S. Cerrito, M. Cialdea Mayer, and S. Praud. First order linear temporal logic over finite time structures is not semi-decidable. Tecnical Report LRI n. 1208, available at \n                    http:\/\/www.dia.uniroma3.it\/~cialdea\/papers\/nonre.ps\n                    \n                  . Presented at the Workshop Methods for Modalities 1 (M4M) (Amsterdam, May 1999)."},{"key":"5_CR10","unstructured":"S. Cerrito, M. Cialdea Mayer, and S. Praud. A tableau calculus for first order linear temporal logic over bounded time structures. Technical Report LRI n. 1207, available at \n                    http:\/\/www.dia.uniroma3.it\/~cialdea\/papers\/foltl.ps\n                    \n                  ."},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/BFb0014006","volume-title":"Temporal Logic: ICTL\u201994","author":"J. Chomicki","year":"1994","unstructured":"J. Chomicki. Temporal query languages: a survey. In D.M. Gabbay and H.J. Ohlbach, editors, Temporal Logic: ICTL\u201994, volume 827 of Lecture Notes in Computer Science, pages 506\u2013534. Springer-Verlag, 1994."},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Proc. of Colloquium on Temporal Logic in Specification","author":"D. Gabbay","year":"1989","unstructured":"D. Gabbay. Declarative past and imperative future: Executable temporal logic for interactive systems. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. of Colloquium on Temporal Logic in Specification, number 398 in LNCS, pages 409\u2013448. Sprinber-Verlag, 1989."},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1007\/BFb0014007","volume-title":"Proceedings of the First International Conference on Temporal Logic (ICTL 94)","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle and O. Ibens. Improving temporal logic tableaux using integer constraints. In D. M. Gabbay and H. J. Ohlbach, editors, Proceedings of the First International Conference on Temporal Logic (ICTL 94), volume 827 of LNCS, pages 535\u2013539. Springer, 1994."},{"key":"5_CR14","first-page":"51","volume":"24","author":"D. Harel","year":"1985","unstructured":"D. Harel. Recurring dominoes: Making the higly undecidable higly understandable. Annals of Discrete Mathematics, 24:51\u201372, 1985.","journal-title":"Annals of Discrete Mathematics"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"M Kaminski and C.K. Wong. The power of the \u201calways\u201d operator in first-order temporal logic. Theoretical Computer Science, pages 271\u2013281, 1996.","DOI":"10.1016\/0304-3975(95)00108-5"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(90)90161-A","volume":"73","author":"F. Kr\u00f6ger","year":"1990","unstructured":"F. Kr\u00f6ger. On the interpretability of arithmetic in temporal logic. Theoretical Computer Science, 73:47\u201361, 1990.","journal-title":"Theoretical Computer Science"},{"key":"5_CR17","unstructured":"P.H. Schmitt and J. Goubault-Larrecq. A tableau system for full linear temporal logic. Draft, available at: \n                    http:\/\/www.dyade.fr\/fr\/actions\/vip\/jgl\/ltl2.ps.gz\n                    \n                  ."},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","volume-title":"3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997)","author":"P.H. Schmitt","year":"1997","unstructured":"P.H. Schmitt and J. Goubault-Larrecq. A tableau system for linear-time temporal logic. In E. Brinksma, editor, 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997), LNCS. Springer Verlag, 1997."},{"key":"5_CR19","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"P. Wolper. The tableau method for temporal logic: an overview. Logique et Analyse, 28:119\u2013152, 1985.","journal-title":"Logique et Analyse"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T20:20:52Z","timestamp":1550434852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}