{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:49Z","timestamp":1760202709487},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"6-8","license":[{"start":{"date-parts":[[2015,11,19]],"date-time":"2015-11-19T00:00:00Z","timestamp":1447891200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s00236-015-0250-1","type":"journal-article","created":{"date-parts":[[2015,11,19]],"date-time":"2015-11-19T07:29:34Z","timestamp":1447918174000},"page":"587-619","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Checking interval properties of computations"],"prefix":"10.1007","volume":"53","author":[{"given":"Alberto","family":"Molinari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,19]]},"reference":[{"issue":"11","key":"250_CR1","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"JF Allen","year":"1983","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832\u2013843 (1983)","journal-title":"Commun. ACM"},{"issue":"1\u20133","key":"250_CR2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/s10472-013-9376-4","volume":"71","author":"D Bresolin","year":"2014","unstructured":"Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: The dark side of interval temporal logic: marking the undecidability border. Ann. Math. Artif. Intell. 71(1\u20133), 41\u201383 (2014)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"250_CR3","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1093\/logcom\/exn063","volume":"20","author":"D Bresolin","year":"2010","unstructured":"Bresolin, D., Goranko, V., Montanari, A., Sala, P.: Tableau-based decision procedures for the logics of subinterval structures over dense orderings. J. Log. Comput. 20(1), 133\u2013166 (2010)","journal-title":"J. Log. Comput."},{"issue":"3","key":"250_CR4","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/j.apal.2009.07.003","volume":"161","author":"D Bresolin","year":"2009","unstructured":"Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Ann. Pure Appl. Log. 161(3), 289\u2013304 (2009)","journal-title":"Ann. Pure Appl. Log."},{"key":"250_CR5","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What\u2019s decidable about Halpern and Shoham\u2019s interval logic? The maximal fragment $${\\sf AB}{\\overline{\\sf BL}}$$ AB BL \u00af . In: Proceedings of the 26th LICS. IEEE Comp. Society Press, pp. 387\u2013396 (2011)","DOI":"10.1109\/LICS.2011.35"},{"key":"250_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of the Workshop on Logic of Programs, LNCS, vol. 131. Springer, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"250_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"2002","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2002)"},{"key":"250_CR8","first-page":"73","volume":"105","author":"D Della Monica","year":"2011","unstructured":"Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Interval temporal logics: a journey. Bull. EATCS 105, 73\u201399 (2011)","journal-title":"Bull. EATCS"},{"key":"250_CR9","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M.: The declarative past and imperative future: executable temporal logic for interactive systems. In: Proceedings of Temporal Logic in Specification, LNCS, vol. 398. Springer, pp. 409\u2013448 (1987)","DOI":"10.1007\/3-540-51803-7_36"},{"issue":"1\u20132","key":"250_CR10","doi-asserted-by":"crossref","first-page":"9","DOI":"10.3166\/jancl.14.9-54","volume":"14","author":"V Goranko","year":"2004","unstructured":"Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. J. Appl. Non-Classical Log. 14(1\u20132), 9\u201354 (2004)","journal-title":"J. Appl. Non-Classical Log."},{"issue":"4","key":"250_CR11","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1145\/115234.115351","volume":"38","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935\u2013962 (1991)","journal-title":"J. ACM"},{"issue":"1","key":"250_CR12","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.jal.2005.08.002","volume":"4","author":"M Lange","year":"2006","unstructured":"Lange, M.: Model checking propositional dynamic logic with all extras. J. Appl. Log. 4(1), 39\u201349 (2006)","journal-title":"J. Appl. Log."},{"key":"250_CR13","doi-asserted-by":"crossref","unstructured":"Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Proceedings of the 6th ASIAN, LNCS, vol. 1961, pp. 290\u2013298 (2000)","DOI":"10.1007\/3-540-44464-5_21"},{"key":"250_CR14","unstructured":"Lomuscio, A.R., Michaliszyn, J.: An epistemic Halpern\u2013Shoham logic. In: Proceedings of the 23rd IJCAI. AAAI Press\/International Joint Conferences on Artificial Intelligence (2013)"},{"key":"250_CR15","unstructured":"Lomuscio, A.R., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: Proceedings of the 21st ECAI, pp. 543\u2013548 (2014)"},{"issue":"2","key":"250_CR16","doi-asserted-by":"crossref","first-page":"217","DOI":"10.3233\/FI-2014-1011","volume":"131","author":"J Marcinkowski","year":"2014","unstructured":"Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundam. Inf. 131(2), 217\u2013240 (2014)","journal-title":"Fundam. Inf."},{"key":"250_CR17","doi-asserted-by":"crossref","unstructured":"Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. In: Proceedings of the 21st TIME, pp. 59\u201368 (2014)","DOI":"10.1109\/TIME.2014.24"},{"key":"250_CR18","doi-asserted-by":"crossref","unstructured":"Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of Halpern and Shoham\u2019s modal logic of intervals. In: Proceedings of the 37th ICALP, LNCS, vol. 6199, pp. 345\u2013356 (2010)","DOI":"10.1007\/978-3-642-14162-1_29"},{"key":"250_CR19","unstructured":"Moszkowski, B.: Reasoning About Digital Circuits. PhD thesis, Department of Computer Science, Stanford University, Stanford, CA (1983)"},{"key":"250_CR20","volume-title":"Computational Complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"250_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"250_CR22","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: The Temporal Semantics of Concurrent Programs. Theor. Comput. Sci. 13, 45\u201360 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"250_CR23","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.:Specification and verification of concurrent programs in CESAR. In: Proceedings of the 6th SP, LNCS, vol. 137. Springer, pp. 337\u2013351 (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"250_CR24","first-page":"451","volume":"9","author":"P Roeper","year":"1980","unstructured":"Roeper, P.: Intervals and tenses. J. Philos. Log. 9, 451\u2013469 (1980)","journal-title":"J. Philos. Log."},{"key":"250_CR25","volume-title":"Introduction to the Theory of Computation","author":"M Sipser","year":"2012","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 3rd edn. International Thomson Publishing, New York (2012)","edition":"3"},{"issue":"3","key":"250_CR26","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"250_CR27","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st LICS. IEEE Comp. Society Press, pp. 332\u2013344 (1986)"},{"issue":"4","key":"250_CR28","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1093\/logcom\/1.4.453","volume":"1","author":"Y Venema","year":"1991","unstructured":"Venema, Y.: A modal logic for chopping intervals. J. Log. Comput. 1(4), 453\u2013476 (1991)","journal-title":"J. Log. Comput."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0250-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0250-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0250-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0250-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T15:26:43Z","timestamp":1599838003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0250-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,19]]},"references-count":28,"journal-issue":{"issue":"6-8","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["250"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0250-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11,19]]}}}