{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:28Z","timestamp":1750219828578,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"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":[[2023,7,31]]},"abstract":"<jats:p>\n            In this article, we introduce and investigate an extension of Halpern and Shoham\u2019s interval temporal logic\n            <jats:sans-serif>HS<\/jats:sans-serif>\n            for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures enforcing visibility of the pushdown operations. The proposed logic, called nested\n            <jats:sans-serif>BHS<\/jats:sans-serif>\n            , supports branching-time both in the past and in the future and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of\n            <jats:sans-serif>LTL<\/jats:sans-serif>\n            such as\n            <jats:sans-serif>CaRet<\/jats:sans-serif>\n            \u00a0[\n            <jats:xref ref-type=\"bibr\">4<\/jats:xref>\n            ] and\n            <jats:sans-serif>NWTL<\/jats:sans-serif>\n            \u00a0[\n            <jats:xref ref-type=\"bibr\">2<\/jats:xref>\n            ]. The main result is the decidability of the visibly pushdown model-checking problem against nested\n            <jats:sans-serif>BHS<\/jats:sans-serif>\n            . The proof exploits a non-trivial automata-theoretic construction.\n          <\/jats:p>\n          <jats:p\/>","DOI":"10.1145\/3583756","type":"journal-article","created":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T23:49:46Z","timestamp":1676504986000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Interval Temporal Logic for Visibly Pushdown Systems"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0963-8169","authenticated-orcid":false,"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli \u201cFederico II,\u201d Napoli, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4322-769X","authenticated-orcid":false,"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7111-3171","authenticated-orcid":false,"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Trieste, Trieste, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.19"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111051"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516518"},{"key":"e_1_3_1_8_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J. P. Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104498"},{"key":"e_1_3_1_11_2","first-page":"120:1\u2013120:14","volume-title":"Proceedings of the 44th ICALP (LIPIcs)","volume":"80","author":"Bozzelli L.","year":"2017","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 Proceedings of the 44th ICALP (LIPIcs), Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 120:1\u2013120:14."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.09.006"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3281028"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0093-x"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9410-z"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-013-9376-4"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn063"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.03.033"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.02.002"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22119-4_8"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_7"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v30i1.10124"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/115234.115351"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36078-6_18"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44464-5_21"},{"key":"e_1_3_1_27_2","first-page":"1010","volume-title":"Proceedings of the 23rd IJCAI","author":"Lomuscio A.","year":"2013","unstructured":"A. Lomuscio and J. Michaliszyn. 2013. An epistemic Halpern-Shoham logic. In Proceedings of the 23rd IJCAI. IJCAI\/AAAI, 1010\u20131016."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-419-0-543"},{"key":"e_1_3_1_29_2","first-page":"298","volume-title":"Proceedings of the 15th KR","author":"Lomuscio A.","year":"2016","unstructured":"A. Lomuscio and J. Michaliszyn. 2016. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In Proceedings of the 15th KR. AAAI Press, 298\u2013308. Retrieved from http:\/\/www.aaai.org\/ocs\/index.php\/KR\/KR16\/paper\/view\/12823."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2014-1011"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0250-1"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.08.011"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:7)2015"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/911281"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2005.04.003"},{"key":"e_1_3_1_37_2","first-page":"451","article-title":"Intervals and Tenses","volume":"9","author":"Roeper P.","year":"1980","unstructured":"P. Roeper. 1980. Intervals and Tenses. J. Philos. Logic 9 (1980), 451\u2013469.","journal-title":"J. Philos. Logic"},{"key":"e_1_3_1_38_2","article-title":"The complexity of decision problems in automata theory and logic","author":"Stockmeyer L. J.","year":"1974","unstructured":"L. J. Stockmeyer. 1974. The complexity of decision problems in automata theory and logic. PhD thesis, MIT.","journal-title":"PhD thesis, MIT"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635589"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_58"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583756","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3583756","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:29Z","timestamp":1750178789000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583756"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,17]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,7,31]]}},"alternative-id":["10.1145\/3583756"],"URL":"https:\/\/doi.org\/10.1145\/3583756","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,4,17]]},"assertion":[{"value":"2022-06-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-02-06","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}