{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:13:17Z","timestamp":1760202797799,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T00:00:00Z","timestamp":1545264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"GNCS project Formal Methods for Verification and Synthesis of Discrete and Hybrid Systems"},{"name":"(PRID) ENCASE - Efforts in the uNderstanding of Complex interActing SystEms"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted \u201cpoint-wise\u201d describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted \u201cinterval-wise\u201d express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste?<\/jats:p>\n          <jats:p>In this article, we study the expressiveness of Halpern and Shoham\u2019s interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL*. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL*, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL*).<\/jats:p>","DOI":"10.1145\/3281028","type":"journal-article","created":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T13:35:46Z","timestamp":1545312946000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Interval vs. Point Temporal Logic Model Checking"],"prefix":"10.1145","volume":"20","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[{"name":"University of Napoli \u201cFederico II\u201d, Napoli, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7792-2105","authenticated-orcid":false,"given":"Alberto","family":"Molinari","sequence":"additional","affiliation":[{"name":"University of Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[{"name":"University of Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[{"name":"University of Napoli \u201cFederico II\u201d, Napoli, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Sala","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,12,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_10"},{"key":"e_1_2_1_3_1","unstructured":"C. Baier and J. P. Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.   C. Baier and J. P. Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press."},{"key":"e_1_2_1_4_1","unstructured":"P. Blackburn and J. Seligman. 1998. What are hybrid languages? In AiML. CSLI Publications 41--62.  P. Blackburn and J. Seligman. 1998. What are hybrid languages? In AiML. CSLI Publications 41--62."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"L.\n      Bozzelli A.\n      Molinari A.\n      Montanari and \n      A.\n      Peron\n  . \n  2017\n  . An in-depth investigation of interval temporal logic model checking with regular expressions. In SEFM Lecture Notes in Computer Science Vol. \n  10469\n  . \n  Springer 104--119.  L. Bozzelli A. Molinari A. Montanari and A. Peron. 2017. An in-depth investigation of interval temporal logic model checking with regular expressions. In SEFM Lecture Notes in Computer Science Vol. 10469. Springer 104--119.","DOI":"10.1007\/978-3-319-66197-1_7"},{"key":"e_1_2_1_6_1","volume-title":"Electronic Proceedings in Theoretical Computer Science","volume":"256","author":"Bozzelli L.","unstructured":"L. Bozzelli , A. Molinari , A. Montanari , and A. Peron . 2017. On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In GandALF , Electronic Proceedings in Theoretical Computer Science , Vol. 256 . EPTCS, 31--45. L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. 2017. On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In GandALF, Electronic Proceedings in Theoretical Computer Science, Vol. 256. EPTCS, 31--45."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_27"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"Interval vs. point temporal logic model checking: An expressiveness comparison","volume":"26","author":"Bozzelli L.","year":"2016","unstructured":"L. Bozzelli , A. Molinari , A. Montanari , A. Peron , and P. Sala . 2016 . Interval vs. point temporal logic model checking: An expressiveness comparison . In FSTTCS. LIPIcs , 26 : 1 -- 26 :14. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2016. Interval vs. point temporal logic model checking: An expressiveness comparison. In FSTTCS. LIPIcs, 26:1--26:14.","journal-title":"FSTTCS. LIPIcs"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"L. Bozzelli A. Molinari A. Montanari A. Peron and P. Sala. 2016. Model checking the logic of Allen\u2019s relations meets and started-by is P<sup>NP<\/sup>-complete. In GandALF. EPTCS 76--90.  L. Bozzelli A. Molinari A. Montanari A. Peron and P. Sala. 2016. Model checking the logic of Allen\u2019s relations meets and started-by is P<sup>NP<\/sup>-complete. In GandALF. EPTCS 76--90.","DOI":"10.4204\/EPTCS.226.6"},{"key":"e_1_2_1_10_1","volume-title":"ICALP (LIPIcs)","volume":"80","author":"Bozzelli L.","unstructured":"L. Bozzelli , A. Molinari , A. Montanari , A. Peron , and P. Sala . 2017. Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption . In ICALP (LIPIcs) , Vol. 80 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 120:1--120:14. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2017. Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption. In ICALP (LIPIcs), Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 120:1--120:14."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-013-9376-4"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn063"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.003"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"D.\n      Bresolin A.\n      Montanari P.\n      Sala and \n      G.\n      Sciavicco\n  . \n  2011\n  . Optimal tableau systems for propositional neighborhood logic over all dense and discrete linear orders. In TABLEAUX Lecture Notes in Computer Science Vol. \n  6973\n  . \n  Springer 73--87.   D. Bresolin A. Montanari P. Sala and G. Sciavicco. 2011. Optimal tableau systems for propositional neighborhood logic over all dense and discrete linear orders. In TABLEAUX Lecture Notes in Computer Science Vol. 6973. Springer 73--87.","DOI":"10.1007\/978-3-642-22119-4_8"},{"key":"e_1_2_1_15_1","unstructured":"G. De Giacomo and M. Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI. IJCAI\/AAAI 854--860.   G. De Giacomo and M. Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI. IJCAI\/AAAI 854--860."},{"key":"e_1_2_1_16_1","volume-title":"Computer Science: Finite-State Systems","author":"Demri S.","year":"2016","unstructured":"S. Demri , V. Goranko , and M. Lange . 2016 . Temporal Logics in Computer Science: Finite-State Systems . Cambridge University Press . S. Demri, V. Goranko, and M. Lange. 2016. Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318620"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Temporal Logic in Specification","author":"Gabbay D. M.","unstructured":"D. M. Gabbay . 1987. The declarative past and imperative future: Executable temporal logic for interactive systems . In Temporal Logic in Specification , Lecture Notes in Computer Science , Vol. 398 . Springer , 409--448. D. M. Gabbay. 1987. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification, Lecture Notes in Computer Science, Vol. 398. Springer, 409--448."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/115234.115351"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.006"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00035-U"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/646067.676812"},{"key":"e_1_2_1_26_1","unstructured":"A. Lomuscio and J. Michaliszyn. 2013. An epistemic Halpern-Shoham logic. In IJCAI. IJCAI\/AAAI 1010--1016.   A. Lomuscio and J. Michaliszyn. 2013. An epistemic Halpern-Shoham logic. In IJCAI. IJCAI\/AAAI 1010--1016."},{"key":"e_1_2_1_27_1","unstructured":"A. Lomuscio and J. Michaliszyn. 2014. Decidability of model checking multi-agent systems against a class of EHS specifications. In ECAI. IOS Press 543--548.   A. Lomuscio and J. Michaliszyn. 2014. Decidability of model checking multi-agent systems against a class of EHS specifications. In ECAI. IOS Press 543--548."},{"key":"e_1_2_1_28_1","unstructured":"A. Lomuscio and J. Michaliszyn. 2016. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In KR. AAAI Press 298--308.   A. Lomuscio and J. Michaliszyn. 2016. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In KR. AAAI Press 298--308."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2608462.2608466"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0250-1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2015.12"},{"key":"e_1_2_1_32_1","unstructured":"A. Molinari A. Montanari and A. Peron. 2015. A model checking procedure for interval temporal logics based on track representatives. In CSL. LIPIcs 193--210.  A. Molinari A. Montanari and A. Peron. 2015. A model checking procedure for interval temporal logics based on track representatives. In CSL. LIPIcs 193--210."},{"key":"e_1_2_1_33_1","unstructured":"A. Molinari A. Montanari A. Peron and P. Sala. 2016. Model checking well-behaved fragments of HS: The (almost) final picture. In KR. AAAI Press 473--483.   A. Molinari A. Montanari A. Peron and P. Sala. 2016. Model checking well-behaved fragments of HS: The (almost) final picture. In KR. AAAI Press 473--483."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"A. Montanari A. Murano G. Perelli and A. Peron. 2014. Checking interval properties of computations. In TIME. IEEE Computer Society 59--68.  A. Montanari A. Murano G. Perelli and A. Peron. 2014. Checking interval properties of computations. In TIME. IEEE Computer Society 59--68.","DOI":"10.1109\/TIME.2014.24"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:7)2015"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_38_1","volume-title":"Temporal prepositions and their logic. Artificial Intelligence 166(1--2)","author":"Pratt-Hartmann I.","year":"2005","unstructured":"I. Pratt-Hartmann . 2005. Temporal prepositions and their logic. Artificial Intelligence 166(1--2) ( 2005 ), 1--36. I. Pratt-Hartmann. 2005. Temporal prepositions and their logic. Artificial Intelligence 166(1--2) (2005), 1--36."},{"key":"e_1_2_1_39_1","first-page":"451","article-title":"Intervals and tenses","volume":"9","author":"Roeper P.","year":"1980","unstructured":"P. Roeper . 1980 . Intervals and tenses . Journal of Philosophical Logic 9 (1980), 451 -- 469 . P. Roeper. 1980. Intervals and tenses. Journal of Philosophical Logic 9 (1980), 451--469.","journal-title":"Journal of Philosophical Logic"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"volume-title":"Logics for Concurrency","author":"Vardi M. Y.","key":"e_1_2_1_41_1","unstructured":"M. Y. Vardi . 1996. An automata-theoretic approach to linear temporal logic . In Logics for Concurrency . Springer , 238--266. M. Y. Vardi. 1996. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency. Springer, 238--266."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635589"},{"volume-title":"STACS, (Lecture Notes in Computer Science","author":"Wilke T.","key":"e_1_2_1_43_1","unstructured":"T. Wilke . 1999. Classifying discrete temporal properties . In STACS, (Lecture Notes in Computer Science , Vol. 1563). Springer, 32-- 46 . T. Wilke. 1999. Classifying discrete temporal properties. In STACS, (Lecture Notes in Computer Science, Vol. 1563). Springer, 32--46."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3281028","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3281028","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:17Z","timestamp":1750208237000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3281028"}},"subtitle":["An Expressiveness Comparison"],"short-title":[],"issued":{"date-parts":[[2018,12,20]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3281028"],"URL":"https:\/\/doi.org\/10.1145\/3281028","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,12,20]]},"assertion":[{"value":"2017-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}