{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:34Z","timestamp":1783111474487,"version":"3.54.6"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,4,30]]},"abstract":"<jats:p>\n            We consider intuitionistic variants of linear temporal logic with \u201cnext,\u201d \u201cuntil,\u201d and \u201crelease\u201d based on\n            <jats:italic>expanding posets<\/jats:italic>\n            : partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic that we denote ITL\n            <jats:sup>e<\/jats:sup>\n            , and by imposing additional constraints, we obtain the logics ITL\n            <jats:sup>p<\/jats:sup>\n            of\n            <jats:italic>persistent posets<\/jats:italic>\n            and ITL\n            <jats:sup>ht<\/jats:sup>\n            of\n            <jats:italic>here-and-there temporal logic,<\/jats:italic>\n            both of which have been considered in the literature. We prove that ITL\n            <jats:sup>e<\/jats:sup>\n            has the effective finite model property and hence is decidable, while ITL\n            <jats:sup>p<\/jats:sup>\n            does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the \u201cuntil\u201d and \u201crelease\u201d operators are not definable in terms of each other, even over the class of persistent posets.\n          <\/jats:p>","DOI":"10.1145\/3365833","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T13:33:12Z","timestamp":1576848792000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Intuitionistic Linear Temporal Logics"],"prefix":"10.1145","volume":"21","author":[{"given":"Philippe","family":"Balbiani","sequence":"first","affiliation":[{"name":"IRIT, Toulouse University, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Boudou","sequence":"additional","affiliation":[{"name":"IRIT, Toulouse University, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mart\u00edn","family":"Di\u00e9guez","sequence":"additional","affiliation":[{"name":"LAB-STICC, ENIB, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8604-4183","authenticated-orcid":false,"given":"David","family":"Fern\u00e1ndez-Duque","sequence":"additional","affiliation":[{"name":"Department of Mathematics, Ghent University, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"4","article-title":"A denotational semantics for equilibrium logic","volume":"15","author":"Aguado F.","year":"2015","unstructured":"F. Aguado , P. Cabalar , D. Pearce , G. P\u00e9rez , and C. Vidal . 2015 . A denotational semantics for equilibrium logic . Theory Pract. Logic Program. 15 , 4 - 5 (2015), 620--634. F. Aguado, P. Cabalar, D. Pearce, G. P\u00e9rez, and C. Vidal. 2015. A denotational semantics for equilibrium logic. Theory Pract. Logic Program. 15, 4-5 (2015), 620--634.","journal-title":"Theory Pract. Logic Program."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.06.007"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA\u201916)","author":"Balbiani P.","unstructured":"P. Balbiani and M. Di\u00e9guez . 2016. Temporal here and there . In Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA\u201916) . Springer, Larnaca, Cyprus, 81--96. P. Balbiani and M. Di\u00e9guez. 2016. Temporal here and there. In Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA\u201916). Springer, Larnaca, Cyprus, 81--96."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press Cambridge UK.  P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_5_1","first-page":"1","article-title":"A decidable intuitionistic temporal logic. In Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL\u201917). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Stockholm","volume":"14","author":"Boudou J.","year":"2017","unstructured":"J. Boudou , M. Di\u00e9guez , and D. Fern\u00e1ndez-Duque . 2017 . A decidable intuitionistic temporal logic. In Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL\u201917). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Stockholm , Sweden , 14 : 1 -- 14 :17. J. Boudou, M. Di\u00e9guez, and D. Fern\u00e1ndez-Duque. 2017. A decidable intuitionistic temporal logic. In Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL\u201917). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Stockholm, Sweden, 14:1--14:17.","journal-title":"Sweden"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA\u201919)","author":"Boudou J.","unstructured":"J. Boudou , M. Di\u00e9guez , D. Fern\u00e1ndez-Duque , and F. Romero . 2019. Axiomatic systems and topological semantics for intuitionistic temporal logic . In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA\u201919) . Springer International Publishing, 763--777. J. Boudou, M. Di\u00e9guez, D. Fern\u00e1ndez-Duque, and F. Romero. 2019. Axiomatic systems and topological semantics for intuitionistic temporal logic. In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA\u201919). Springer International Publishing, 763--777."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043195"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 11th International Conference on Computer Aided Systems Theory (EUROCAST\u201907)","author":"Cabalar P.","unstructured":"P. Cabalar and G. P\u00e9rez . 2007. Temporal equilibrium logic: A first approach . In Proceedings of the 11th International Conference on Computer Aided Systems Theory (EUROCAST\u201907) . Springer, Berlin, 241--248. P. Cabalar and G. P\u00e9rez. 2007. Temporal equilibrium logic: A first approach. In Proceedings of the 11th International Conference on Computer Aided Systems Theory (EUROCAST\u201907). Springer, Berlin, 241--248."},{"key":"e_1_2_1_9_1","volume-title":"Handbook of Philosophical Logic.","author":"van Dalen D.","unstructured":"D. van Dalen . 1986. Intuitionistic logic . In Handbook of Philosophical Logic. Vol. 166 . Springer Netherlands , Dordrecht , 225--339. D. van Dalen. 1986. Intuitionistic logic. In Handbook of Philosophical Logic. Vol. 166. Springer Netherlands, Dordrecht, 225--339."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788825"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3011069"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.009"},{"key":"e_1_2_1_14_1","unstructured":"M. Di\u00e9guez and D. Fern\u00e1ndez-Duque. 2018. An intuitionistic axiomatization of \u201ceventually\u201d. In Advances in Modal Logic. College Publications Bern Switzerland 199--218.  M. Di\u00e9guez and D. Fern\u00e1ndez-Duque. 2018. An intuitionistic axiomatization of \u201ceventually\u201d. In Advances in Modal Logic. College Publications Bern Switzerland 199--218."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(77)90078-3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273953"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915)","author":"del Cerro L. Fari\u00f1as","unstructured":"L. Fari\u00f1as del Cerro , A. Herzig , and E. Iraz Su . 2015. Epistemic equilibrium logic . In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915) . AAAI Press, Buenos Aires, Argentina, 2964--2970. L. Fari\u00f1as del Cerro, A. Herzig, and E. Iraz Su. 2015. Epistemic equilibrium logic. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915). AAAI Press, Buenos Aires, Argentina, 2964--2970."},{"key":"e_1_2_1_18_1","first-page":"1","article-title":"The intuitionistic temporal logic of dynamical systems","volume":"14","author":"Fern\u00e1ndez-Duque D.","year":"2018","unstructured":"D. Fern\u00e1ndez-Duque . 2018 . The intuitionistic temporal logic of dynamical systems . Logic. Methods Comput. Sci. 14 , 3 (2018), 1 -- 35 . D. Fern\u00e1ndez-Duque. 2018. The intuitionistic temporal logic of dynamical systems. Logic. Methods Comput. Sci. 14, 3 (2018), 1--35.","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201980)","author":"Gabbay D.","unstructured":"D. Gabbay , A. Pnueli , S. Shelah , and J. Stavi . 1980. On the temporal analysis of fairness . In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201980) . ACM, New York, NY, 163--173. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. 1980. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201980). ACM, New York, NY, 163--173."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.01.001"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 5th International Conference on Logic Programming (ICLP\u201988)","author":"Gelfond M.","unstructured":"M. Gelfond and V. Lifschitz . 1988. The stable model semantics for logic programming . In Proceedings of the 5th International Conference on Logic Programming (ICLP\u201988) . MIT Press, Seattle, WA, 1070--1080. M. Gelfond and V. Lifschitz. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Conference on Logic Programming (ICLP\u201988). MIT Press, Seattle, WA, 1070--1080."},{"key":"e_1_2_1_22_1","volume-title":"Die formalen Regeln der intuitionistischen Logik. De\u00fctsche Akademie der Wissenschaften zu Berlin","author":"Heyting A.","unstructured":"A. Heyting . 1930. Die formalen Regeln der intuitionistischen Logik. De\u00fctsche Akademie der Wissenschaften zu Berlin , Mathematisch-Naturwissenschaftliche Klasse , Berlin, Germany . A. Heyting. 1930. Die formalen Regeln der intuitionistischen Logik. De\u00fctsche Akademie der Wissenschaften zu Berlin, Mathematisch-Naturwissenschaftliche Klasse, Berlin, Germany."},{"key":"e_1_2_1_23_1","first-page":"171","article-title":"Expressive completeness of Until and Since over dedekind complete linear time","volume":"53","author":"Hodkinson I.","year":"1995","unstructured":"I. Hodkinson . 1995 . Expressive completeness of Until and Since over dedekind complete linear time . Modal Logic Process Alg. 53 (1995), 171 -- 185 . I. Hodkinson. 1995. Expressive completeness of Until and Since over dedekind complete linear time. Modal Logic Process Alg. 53 (1995), 171--185.","journal-title":"Modal Logic Process Alg."},{"key":"e_1_2_1_24_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Howard W. A.","unstructured":"W. A. Howard . 1980. The formulas-as-types notion of construction . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism , J. P. Seldin and J. R. Hindley (Eds.). Academic Press , Boston, MA , 479--490. W. A. Howard. 1980. The formulas-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, Boston, MA, 479--490."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2009.06.001"},{"key":"e_1_2_1_27_1","first-page":"1491","article-title":"Constructive linear-time temporal logic: Proof systems and Kripke semantics. Info","volume":"209","author":"Kojima K.","year":"2011","unstructured":"K. Kojima and A. Igarashi . 2011 . Constructive linear-time temporal logic: Proof systems and Kripke semantics. Info . Comput. 209 , 12 (2011), 1491 -- 1503 . K. Kojima and A. Igarashi. 2011. Constructive linear-time temporal logic: Proof systems and Kripke semantics. Info. Comput. 209, 12 (2011), 1491--1503.","journal-title":"Comput."},{"key":"e_1_2_1_28_1","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture","volume":"95","author":"Kruskal J. B.","year":"1960","unstructured":"J. B. Kruskal . 1960 . Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture . Trans. Amer. Math. Soc. 95 , 2 (1960), 210 -- 225 . J. B. Kruskal. 1960. Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture. Trans. Amer. Math. Soc. 95, 2 (1960), 210--225.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008223921944"},{"key":"e_1_2_1_30_1","volume-title":"Gabbay","author":"Kurucz A.","year":"2003","unstructured":"A. Kurucz , F. Wolter , M. Zakharyaschev , and Dov M . Gabbay . 2003 . Many-Dimensional Modal Logics: Theory and Applications, Volume 148 (Studies in Logic and the Foundations of Mathematics) (1 ed.). North Holland, Amsterdam, The Netherlands . A. Kurucz, F. Wolter, M. Zakharyaschev, and Dov M. Gabbay. 2003. Many-Dimensional Modal Logics: Theory and Applications, Volume 148 (Studies in Logic and the Foundations of Mathematics) (1 ed.). North Holland, Amsterdam, The Netherlands."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer","author":"Lifschitz V.","unstructured":"V. Lifschitz , D. Pearce , and A. Valverde . 2007. A characterization of strong equivalence for logic programs with variables . In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer , Berlin, 188--200. V. Lifschitz, D. Pearce, and A. Valverde. 2007. A characterization of strong equivalence for logic programs with variables. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer, Berlin, 188--200."},{"key":"e_1_2_1_32_1","volume-title":"Die logik und das grundlagenproblem. Les Entreties de Z\u00fcrich sur les Fondaments et la M\u00e9thode des Sciences Math\u00e9matiques 12, 6-9","author":"Lukasiewicz J.","year":"1938","unstructured":"J. Lukasiewicz . 1938. Die logik und das grundlagenproblem. Les Entreties de Z\u00fcrich sur les Fondaments et la M\u00e9thode des Sciences Math\u00e9matiques 12, 6-9 ( 1938 ), 82--100. J. Lukasiewicz. 1938. Die logik und das grundlagenproblem. Les Entreties de Z\u00fcrich sur les Fondaments et la M\u00e9thode des Sciences Math\u00e9matiques 12, 6-9 (1938), 82--100."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_24"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"V. Marek and M. Truszczy\u0144ski. 1999. Stable Models and an Alternative Logic Programming Paradigm. Springer-Verlag Berlin 169--181.  V. Marek and M. Truszczy\u0144ski. 1999. Stable Models and an Alternative Logic Programming Paradigm. Springer-Verlag Berlin 169--181.","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"e_1_2_1_35_1","volume-title":"A Short Introduction to Intuitionistic Logic","author":"Mints G.","unstructured":"G. Mints . 2000. A Short Introduction to Intuitionistic Logic . Kluwer Academic Publishers , Norwell, MA . G. Mints. 2000. A Short Introduction to Intuitionistic Logic. Kluwer Academic Publishers, Norwell, MA."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.09.009"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_24"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the Non-Monotonic Extensions of Logic Programming (NMELP\u201996)","author":"Pearce D.","year":"1996","unstructured":"D. Pearce . 1996 . A new logical characterisation of stable models and answer sets . In Proceedings of the Non-Monotonic Extensions of Logic Programming (NMELP\u201996) . Springer, Bad Honnef, Germany, 57--70. D. Pearce. 1996. A new logical characterisation of stable models and answer sets. In Proceedings of the Non-Monotonic Extensions of Logic Programming (NMELP\u201996). Springer, Bad Honnef, Germany, 57--70."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-006-9028-z"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 1st Conference on Theoretical Aspects of Reasoning About Knowledge (TARK\u201986)","author":"Plotkin G.","unstructured":"G. Plotkin and C. Stirling . 1986. A framework for intuitionistic modal logics: Extended abstract . In Proceedings of the 1st Conference on Theoretical Aspects of Reasoning About Knowledge (TARK\u201986) . Morgan Kaufmann Publishers Inc., San Francisco, CA, 399--406. G. Plotkin and C. Stirling. 1986. A framework for intuitionistic modal logics: Extended abstract. In Proceedings of the 1st Conference on Theoretical Aspects of Reasoning About Knowledge (TARK\u201986). Morgan Kaufmann Publishers Inc., San Francisco, CA, 399--406."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_43_1","volume-title":"A proof of Kamp\u2019s theorem. Logic. Methods Comput. Sci. 10, 1","author":"Rabinovich A.","year":"2014","unstructured":"A. Rabinovich . 2014. A proof of Kamp\u2019s theorem. Logic. Methods Comput. Sci. 10, 1 ( 2014 ). A. Rabinovich. 2014. A proof of Kamp\u2019s theorem. Logic. Methods Comput. Sci. 10, 1 (2014)."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201906)","author":"Yuse Y.","unstructured":"Y. Yuse and A. Igarashi . 2006. A modal type system for multi-level generating extensions with persistent code . In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201906) . ACM, New York, NY, 201--212. Y. Yuse and A. Igarashi. 2006. A modal type system for multi-level generating extensions with persistent code. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201906). ACM, New York, NY, 201--212."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365833","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3365833","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:36Z","timestamp":1750202616000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3365833"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4,30]]}},"alternative-id":["10.1145\/3365833"],"URL":"https:\/\/doi.org\/10.1145\/3365833","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}